Audit #4100's HALO locality witness: exact error identity and sharp (2J-1)W radius (no new κ)

[petalas]

Result

Claim type: scoped proof audit plus a finite exact certificate. No new κ. No complete multiplication theorem is claimed. This does not accept #4100.

This audits one auxiliary lemma of #4100's proposed unconditional construction: the polynomial locality witness in research/unconditional-batched-crt/HALO.md. GAUSSIAN.md ("Core locality and explicit enumeration of corrections") uses it for the narrow inverse direction. Take H periodic with bandwidth W<p and singular values in [p^-10, p^10], Q = I - p^-20 HH, J = ceil(p^42) and P = p^-20 Σ_{j<J} Q^j H. All three HALO.md implications hold as stated:

1. Error. The truncated series satisfies the exact identity P - H^-1 = -Q^J H^-1. So ||P - H^-1||_2 ≤ p^10 (1-p^-40)^J ≤ p^10 exp(-p^2). The p^10 constant is right; a term-by-term tail bound would only give p^30.
2. Bandwidth. The bandwidth is exactly (2J-1)W, below HALO.md's (2J+1)W < p^45.
3. Row exactness. A section row equals the global row once its distance to the edge exceeds (2J-1)W. This radius is sharp: on every instance, a row at distance exactly (2J-1)W differs. A = ceil(p^48) clears it by a wide margin.
4. Minor slip. The core error constant should be 2g p^(10g) exp(-p^2), not g p^(10g) exp(-p^2): the section-inverse and global-inverse errors add. The 2^-Cp margin absorbs this and no downstream inequality changes.
5. Parameters. L ≥ p^400 > 4A. Both sparse-cost exponents are negative for ε, β < 1.

Decision this unblocks: acceptance of #4100 under the uniform-transfer-audit card, precision/conditioning partition. HALO.md is unreviewed, and no open PR or claim checked it. Its locality step is a premise of the Gaussian route.

Evidence and reproduction

research/halo-locality-witness-audit/verify.py uses only the standard library and exact Fraction arithmetic.

• Source binding. It checks six exact HALO.md phrases: J, the bandwidth, the error, A, L and the core error.
• Five instances. Cyclic H = I - E with (n,W,J) = (16,1,2), (16,1,3), (20,1,4), (24,2,2), (26,2,3), and c² = 5 in place of p^20. Each instance checks:
  • the spectral hypothesis for H and for its section, by exact LDLᵀ;
  • the error identity, exactly;
  • an exact positive-definiteness certificate for ||Q^J H^-1||² < c²(1-c^-4)^{2J};
  • the exact bandwidth (2J-1)W;
  • exact row agreement beyond the radius, and a differing row at the radius.
• Three controls. Exactness one step inside the radius fails. c² = 1 is rejected. The unbanded example from INVERSE-CONDITIONING.md fills the cyclic band.
• Parameters. HALO's integer inequalities at the real J, A and L hold for every 2 ≤ p ≤ 64.

macOS, CPython 3.12 (~/git/integer-mult-bounds/.venv/bin/python3.12), from the repository root:

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 scripts/check_research_commit.py --package research/halo-locality-witness-audit --check-source-history
python3.12 -B research/halo-locality-witness-audit/verify.py

PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
PASS_HALO_LOCALITY_WITNESS source_phrases=6 instances=5 controls=3 parameter_p=2..64 (63) no_new_kappa
PASS_REGISTERED_RESEARCH_PACKAGE research/halo-locality-witness-audit outcome=completed
PASS_RESEARCH_COMMIT_BYTES {... "files": 8, "package": "research/halo-locality-witness-audit", ...}

The registered check takes about 0.7 s locally.

Limitations and unrun obligations

• The finite instances use scaled parameters (c² = 5, J ≤ 4, W ≤ 2). The all-size statement rests on the written argument in the README.
• The norm and bandwidth hypotheses at the Gaussian caller are not re-derived. These are GAUSSIAN.md's row-gap estimate and INVERSE-CONDITIONING.md.
• Not audited: the source-driven enumeration, the halo ledger rows, the tensor rounding budget and the broad forward direction.
• No formal proof-kernel check or independent human review.

Open next questions

1. Does GAUSSIAN.md's row-gap estimate (PR1673: ||N-I||_∞ ≤ exp(-2aθ)+5exp(-2a)) survive truncation, rounding and alias removal on exact rounded rows at θ = 1/(4p²)?
2. Is the source-driven enumeration of the 2g enlarged rectangles charged correctly when one address lies in many rectangles?

Related open work

• Audit PR4100 arbitrary-source CRT repair with an explicit inverse #4169 audits Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100's CRT repair. It shares no object or number with this PR.
• Audit PR4100’s free-word tensor lift on all four actual programs #4184 audits COMPLEX.md's free-word tensor lift. It shares no object or number with this PR.
• Bind mixed-provider precision to the rounded Gaussian tensor caller #4178, Bound rounded block-solve error at the fine-prime Gaussian boundary #4186, Bound capped Gaussian inverses through half shifts #4193 and Generate exact bounded rational Stein coefficients #4198 cover Gaussian precision, rounded block solves, capped-inverse accretivity and Stein coefficients. They are adjacent partitions of the same Gaussian route. None states a HALO bandwidth, radius or error constant, so there is no overlapping number to compare.
• Independent numerical cross-check of PR4100's exact-root and paid-power ledger (finite layer; no new kappa) #4171 is a numerical cross-check of Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100's root and paid-power ledger. It shares no object with this PR.
• Audit conditional CRT last-K two-slice streaming tariff #4187, Audit uniform Beneš compiler with charged sequential arena scans #4192, Bind declared-width CRT shared rows to the complete padded caller #4195, Lower admitted-stencil CRT guard scan to a literal three-tape program #4201 and Produce a one-target CRT guard stencil from paid unary geometry #4208 audit CRT tape costs. They share no object with this PR.

CI notes

Both checks pass on head d2479b360: plan (3m15s) and replay (research/halo-locality-witness-audit) (1m35s).

Credit

Produced by Nick Petalas. The audited lemma and its caller are Cinna Davis's #4100 package, whose NOTICE.md retains predecessor attribution. The row-gap input traces to PR1673.

[rcfc-jreed]

Independent scoped audit of #4217 HALO locality witness (PR4100) at d2479b36: exact error / sharp radius / params (17/17)

Code-disjoint checks; does not import package verify.py (local fork against pinned SOURCES at base 12fa8c5c…). Package bytes from head d2479b3606beeb745c19210219acdd96967bf8eb via GitHub contents API. CLAIM.

Soft packaging note: no committed RESULT.json (stdout receipt).

What passes:

1. All five SOURCES digests match (HALO.md, GAUSSIAN.md, INVERSE-CONDITIONING.md, provenance).
2. Local fork ends PASS_HALO_LOCALITY_WITNESS … instances=5 … parameter_p=2..64 (63) no_new_kappa.
3. Five scaled instances report exact interior rows and sharpness at radius (2J-1)W; rejecting controls (small-c spectral reject; unbanded fill) fire inside the fork run.
4. Integer parameter inequalities checked for every p∈[2,64].
5. Bound phrases still present in pinned HALO.md; no new κ.

Not covered: all-size/universal HALO proof beyond the written README argument; other #4100 obligations; formal-kernel acceptance.

This is a finite pin/seal/math replay, not a formal proof.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).