diff --git a/research/halo-locality-witness-audit/README.md b/research/halo-locality-witness-audit/README.md new file mode 100644 index 0000000000..03b244baf6 --- /dev/null +++ b/research/halo-locality-witness-audit/README.md @@ -0,0 +1,135 @@ +# Audit of the HALO.md polynomial locality witness (#4100) + +**Scoped proof audit plus a finite exact certificate. No new κ.** This checks +one auxiliary lemma of the proposed unconditional construction in +[#4100](../unconditional-batched-crt/README.md). It does not accept the +construction, recertify its cost ledger, or check the Gaussian matrix itself. + +## The proposition and its caller + +[HALO.md](../unconditional-batched-crt/HALO.md) supplies the locality step that +[GAUSSIAN.md](../unconditional-batched-crt/GAUSSIAN.md), "Core locality and +explicit enumeration of corrections", uses for the narrow inverse direction. +Its hypotheses: H is a periodic matrix of physical bandwidth W= p^400 > 4A. The two sparse exponents are + epsilon+beta+144-400 and epsilon+50-400. Both are negative for epsilon, + beta<1. The cost expression is the per-group bound + (gA/L)V(gA^2+p^2) summed over d/g groups. + +Nothing in this lemma needs the Gaussian structure beyond the stated norm and +bandwidth bounds, so the audit applies at its GAUSSIAN.md caller exactly when +those hypotheses hold there. This package does not re-derive them. + +## Executable evidence + +[verify.py](verify.py) uses only the standard library and exact rationals. + +- **Source binding.** It checks that HALO.md still states six exact phrases: + J, the bandwidth, the error, A, L and the core error. +- **Five instances.** These are cyclic H=I-E, with E having band W and entries + ±1/(8W), for (n,W,J) = (16,1,2), (16,1,3), (20,1,4), (24,2,2) and (26,2,3), + with c^2=5 standing in for p^20. Each instance checks: + - c^-2 I < H^T H < c^2 I exactly, for H and for its section, by an LDL^T + positive-definiteness test; + - the identity P-H^-1 = -Q^J H^-1 exactly; + - ||Q^J H^-1||_2^2 < c^2 (1-c^-4)^(2J), by an exact positive-definiteness + certificate; + - the bandwidth of P is exactly (2J-1)W; + - section rows agree exactly beyond the radius (2J-1)W, and at least one + row at distance exactly (2J-1)W differs. +- **Three controls.** Exactness one step inside the radius fails on every + instance. c^2=1 is rejected by the spectral check. The unbanded + INVERSE-CONDITIONING example E[i,0]=1/4 gives P full cyclic bandwidth. +- **Parameters.** For every integer 2<=p<=64, it checks (2J+1)(p-1) < p^45 and + < A, and L >= p^400 > 4A, at the real J, A and L. It also checks the + sparse exponents. + +```text +PASS_HALO_LOCALITY_WITNESS source_phrases=6 instances=5 controls=3 parameter_p=2..64 (63) no_new_kappa +``` + +## Reproduce + +From the repository root (CPython 3.12, standard library only): + +```sh +python3.12 -B scripts/research_package.py --package research/halo-locality-witness-audit --check-only +python3.12 -B scripts/research_package.py --package research/halo-locality-witness-audit +python3.12 -B research/halo-locality-witness-audit/verify.py +``` + +The verifier runs in under one second. + +## Limitations + +- The instances use scaled parameters (c^2=5, J<=4, W<=2), not c=p^10 and + J=ceil(p^42). The all-size statement rests on the written argument above. + The finite instances test the argument's exact identities and the sharp + radius; they do not replace it. +- The norm and bandwidth hypotheses at the Gaussian caller are not + re-derived here. These are GAUSSIAN.md's row-gap estimate and + INVERSE-CONDITIONING.md. +- The source-driven enumeration, the halo cost ledger rows, the tensor + rounding budget and the broad forward direction are not audited. +- This is not a formal proof-kernel check, and it is not an independent + human review. + +## Open next questions + +1. **Does GAUSSIAN.md's row-gap estimate survive truncation, rounding and + alias removal at the narrow reference matrix?** HALO's hypotheses depend on + it. A first step is to evaluate the sharp PR1673 row estimate + ||N-I||_inf <= exp(-2a theta)+5exp(-2a) on exact rounded rows for a + moderate p and theta=1/(4p^2). +2. **Is GAUSSIAN.md's source-driven enumeration of the 2g enlarged + rectangles charged correctly when one address lies in many rectangles?** + This is the remaining cost obligation in the same correction step. + +## Credit + +Produced by Nick Petalas. The audited lemma and its caller are Cinna Davis's +#4100 package, which retains its own predecessor attribution in +[NOTICE.md](../unconditional-batched-crt/NOTICE.md). The row-gap input traces +to PR1673's capped-phase audit. New work is Apache-2.0. diff --git a/research/halo-locality-witness-audit/SOURCES.json b/research/halo-locality-witness-audit/SOURCES.json new file mode 100644 index 0000000000..d70fbe5abf --- /dev/null +++ b/research/halo-locality-witness-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + }, + { + "path": "research/unconditional-batched-crt/INVERSE-CONDITIONING.md", + "usage": "input", + "git_blob": "3853ffac91dfed5421b05533eb274a8646741071", + "sha256": "be3e4b729481b15a5ccc286b297908e4f9cef94c0c9144a28ee1cf58950d142a" + } + ] +} diff --git a/research/halo-locality-witness-audit/TASK.json b/research/halo-locality-witness-audit/TASK.json new file mode 100644 index 0000000000..95e84a91df --- /dev/null +++ b/research/halo-locality-witness-audit/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Audit HALO.md's polynomial locality witness (Neumann polynomial bandwidth, error and exact row agreement, core error constant, sparse exponents) at its GAUSSIAN.md core-correction caller, precision/conditioning partition.", + "scope_change_reason": "The card asks for one quantified #4100 proposition; CRT repair, free-algebra lift, rounded Gaussian precision and several tape costs already have open audits, while HALO.md had none.", + "bottleneck_link": "#4100's proposed all-size proof is the main open acceptance decision; HALO.md is the locality input to its narrow Gaussian inverse step, so a defect here would break the Gaussian route.", + "budget_minutes": 60, + "stop_rule": "Stop at a written check of each HALO implication with an exact finite certificate, or at the first implication that fails.", + "outcome": "completed", + "evidence": "Written proof of the three HALO implications (exact identity P-H^-1=-Q^J H^-1, sharp bandwidth and exactness radius (2J-1)W) and the parameter inequalities; minor factor-2 slip in the core error constant, absorbed downstream. Exact-rational verifier: five scaled instances, three rejecting controls, parameter checks for 2<=p<=64.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does GAUSSIAN.md's row-gap estimate survive truncation, rounding and alias removal at the narrow reference matrix?", + "why_it_matters": "HALO's norm hypotheses at its caller rest on that row gap.", + "first_step": "Evaluate the PR1673 row estimate on exact rounded rows for a moderate p with theta=1/(4p^2).", + "blocked_by": "None." + }, + { + "question": "Is GAUSSIAN.md's source-driven enumeration of the 2g enlarged rectangles charged correctly when an address lies in many rectangles?", + "why_it_matters": "It is the remaining cost obligation in the same correction step.", + "first_step": "Write the enumeration as an explicit odometer and count internal nodes against emitted leaves on a small g.", + "blocked_by": "None." + } + ] +} diff --git a/research/halo-locality-witness-audit/VERIFY.json b/research/halo-locality-witness-audit/VERIFY.json new file mode 100644 index 0000000000..412cebd6e8 --- /dev/null +++ b/research/halo-locality-witness-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/INVERSE-CONDITIONING.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source phrases, exact error identity and bound, sharp bandwidth and exactness radius on five instances, three rejecting controls, parameter inequalities for 2<=p<=64." + } + ] +} diff --git a/research/halo-locality-witness-audit/verify.py b/research/halo-locality-witness-audit/verify.py new file mode 100644 index 0000000000..894463acb3 --- /dev/null +++ b/research/halo-locality-witness-audit/verify.py @@ -0,0 +1,258 @@ +"""Exact audit of the HALO.md polynomial locality witness (PR4100). + +HALO.md, used by GAUSSIAN.md "Core locality and explicit enumeration of +corrections", states for a periodic banded H with spectrum of H*H in +[c^-2, c^2] (c = p^10 there) and bandwidth W: + + P = c^-2 sum_{j= A > bandwidth from a section edge equals the + corresponding row of the global P exactly. + +This script checks those statements in exact rational arithmetic on +scaled instances (small c, J, W), with two rejecting controls, and checks +the integer parameter inequalities HALO.md uses at its real parameters +for every p in a bounded range. It is a finite certificate for the stated +instances; the all-size argument is the written proof in README.md. + +Author: Nick Petalas. Apache-2.0. +""" +from fractions import Fraction +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / "research/unconditional-batched-crt/HALO.md" +# Exact HALO.md phrases whose parameters this script checks. +BOUND_PHRASES = ( + "Put Q_i=I-p^-20 H_i^* H_i and J=ceil(p^42).", + "has physical bandwidth <=(2J+1)W 0.""" + n = len(a) + m = [list(r) for r in a] + for k in range(n): + if m[k][k] <= 0: + return False + for i in range(k + 1, n): + if m[i][k]: + f = m[i][k] / m[k][k] + for j in range(k, n): + m[i][j] -= f * m[k][j] + return True + + +def cyclic_distance(i, j, n): + d = abs(i - j) % n + return min(d, n - d) + + +def bandwidth(a, n): + return max((cyclic_distance(i, j, n) for i in range(n) for j in range(n) if a[i][j]), default=0) + + +def banded_h(n, w, rng): + """H = I - E, E cyclic band w, entries k/(8w) with |k| <= 1: row sum of |E| <= 1/4.""" + h = eye(n) + for i in range(n): + for d in range(-w, w + 1): + if d: + h[i][(i + d) % n] -= Fraction(rng.choice((-1, 1)), 8 * w) + return h + + +def spectrum_inside(h, c2): + """c^-2 I < H^T H < c^2 I, strictly, decided exactly.""" + g = matmul(transpose(h), h) + n = len(h) + upper = sub(scale(eye(n), c2), g) + lower = sub(g, scale(eye(n), 1 / c2)) + return positive_definite(upper) and positive_definite(lower) + + +def witness(h, c2, j_terms): + """Return P, Q^J for the Neumann polynomial of HALO.md.""" + n = len(h) + ht = transpose(h) + q = sub(eye(n), scale(matmul(ht, h), 1 / c2)) + term = ht + total = zeros(n) + for _ in range(j_terms): + total = [[x + y for x, y in zip(r, s)] for r, s in zip(total, term)] + term = matmul(q, term) + qj = eye(n) + for _ in range(j_terms): + qj = matmul(q, qj) + return scale(total, 1 / c2), qj + + +def section(a, idx): + return [[a[i][j] for j in idx] for i in idx] + + +def check_instance(n, w, j_terms, seed, c2): + need(n <= MAX_N, "instance size bound") + rng = random.Random(seed) + h = banded_h(n, w, rng) + need(spectrum_inside(h, c2), "global spectral hypothesis") + p, qj = witness(h, c2, j_terms) + hinv = inverse(h) + # Exact error identity P - H^-1 = -Q^J H^-1. + err = sub(p, hinv) + need(err == scale(matmul(qj, hinv), -1), "error identity") + # ||Q^J H^-1||_2^2 < c^2 (1 - c^-4)^(2J): exact PD certificate. + m = matmul(qj, hinv) + bound = c2 * (1 - 1 / (c2 * c2)) ** (2 * j_terms) + need(positive_definite(sub(scale(eye(n), bound), matmul(transpose(m), m))), "error bound") + # Bandwidth: exactly (2J-1)W, within HALO.md's (2J+1)W. + bw = bandwidth(p, n) + need(bw == (2 * j_terms - 1) * w, f"bandwidth {bw}") + # Section rows. The section omits two adjacent cyclic positions. + idx = list(range(n - 2)) + hs = section(h, idx) + need(spectrum_inside(hs, c2), "section spectral hypothesis") + ps, _ = witness(hs, c2, j_terms) + radius = (2 * j_terms - 1) * w + exact_rows = differing_at_radius = 0 + for a, r in enumerate(idx): + dist = min(cyclic_distance(r, o, n) for o in (n - 2, n - 1)) + same = ps[a] == [p[r][c] for c in idx] and all(p[r][o] == 0 for o in (n - 2, n - 1)) + if dist > radius: + need(same, f"row {r} at distance {dist} differs") + exact_rows += 1 + elif dist == radius and not same: + differing_at_radius += 1 + need(exact_rows > 0, "no interior rows tested") + # Sharpness control: one step closer, exactness fails. + need(differing_at_radius > 0, "radius not sharp on this instance") + return {"n": n, "W": w, "J": j_terms, "seed": seed, "bandwidth": bw, + "exact_rows": exact_rows, "rows_differing_at_radius": differing_at_radius} + + +def control_small_c(n, w, j_terms, seed): + """Control: with c^2 = 1 the spectral hypothesis is rejected.""" + h = banded_h(n, w, random.Random(seed)) + need(not spectrum_inside(h, Fraction(1)), "c^2 = 1 must be rejected") + + +def control_unbanded(n): + """Control: E[i,0] = 1/4 (INVERSE-CONDITIONING.md's example) gives a full-width P.""" + h = eye(n) + for i in range(1, n): + h[i][0] -= Fraction(1, 4) + p, _ = witness(h, Fraction(5), 2) + need(bandwidth(p, n) == n // 2, "unbanded control should fill the cyclic band") + + +def check_parameters(p_max): + """HALO.md integer inequalities at J=ceil(p^42), W<=p-1, A=ceil(p^48), L=2^ceil(400 log2 p).""" + checked = 0 + for p in range(2, p_max + 1): + j_terms = p ** 42 + w = p - 1 + a_halo = p ** 48 + log2_ceil = (p - 1).bit_length() + need(2 ** (log2_ceil - 1) < p <= 2 ** log2_ceil, "ceil log2") + l_core = 2 ** (400 * log2_ceil) + need((2 * j_terms + 1) * w < p ** 45, "bandwidth below p^45") + need((2 * j_terms + 1) * w < a_halo, "halo radius exceeds bandwidth") + need(l_core > 4 * a_halo and l_core >= p ** 400, "core side") + checked += 1 + # Sparse exponents: epsilon + beta + 3*48 - 400 and epsilon + 48 + 2 - 400 for epsilon, beta < 1. + need(1 + 1 + 3 * 48 - 400 < 0 and 1 + 48 + 2 - 400 < 0, "sparse exponents") + return checked + + +def check_source(): + text = SOURCE.read_text(encoding="utf-8") + for phrase in BOUND_PHRASES: + need(phrase in text, f"HALO.md no longer states: {phrase}") + return len(BOUND_PHRASES) + + +def main(): + phrases = check_source() + c2 = Fraction(5) + cases = [(16, 1, 2, 1), (16, 1, 3, 2), (20, 1, 4, 3), (24, 2, 2, 4), (26, 2, 3, 5)] + results = [check_instance(n, w, j, s, c2) for n, w, j, s in cases] + for r in results: + print("INSTANCE", r) + control_small_c(16, 1, 2, 1) + control_unbanded(12) + checked = check_parameters(64) + print(f"PASS_HALO_LOCALITY_WITNESS source_phrases={phrases} instances={len(results)} controls=3 parameter_p=2..64 ({checked}) no_new_kappa") + return 0 + + +if __name__ == "__main__": + sys.exit(main())