[pinterbanget]

Summary

This adds research/pr4100-proof-composition-audit/. It is an independent audit of the identities that Cinna Davis's #4100 PROOF.md composes into its outer algorithm, from the CRT address map through to exact integer recovery. The #4311 coverage map listed this as gap 2: no audit existed.

Claim type: a scoped proof audit (written re-derivation) with finite exact and 60-digit corroboration. No new κ. It does not accept #4100 and changes no #4100 file, priority or selected record.

Result

Every audited identity holds exactly with PROOF.md's own conventions (1/n-normalized DFTs, negative-exponent forward transforms):

1. Address isomorphism. y_i = k P_i^-1 mod s_i is a group isomorphism Z_S → Π Z_(s_i). It equals CRT.md's root map Φ_G, so PROOF.md and CRT.md agree.
2. Synthetic convolution. M F+((F- f)(F- g)/r) = (f*g)/(rM), and the ζ_(2r) twist turns the negacyclic product into a cyclic one. The y^(2r/t) twiddles are principal roots in C[y]/(y^r+1) when r is a power of two. The normalized H0/2 butterflies equal F- after bit reversal.
3. Chirp identity. It holds for all x, z if and only if s·t is even. PROOF.md's "each t_i even" is the right sufficient condition for odd primes s_i.
4. Gaussian source-transform identity. T_gauss P_s F_s = P_t F_t S_gauss holds by Poisson summation for every pair of positive integers s, t and every α > 0. Coprimality is needed only so the index maps are permutations. N = C T_gauss D has principal diagonal term exactly 1, and P_s F_s = D N^-1 C P_t F_t S_gauss follows whenever N is invertible.
5. Exact recovery.
   • F^+ R = R^-1 F^+.
   • T < 2^b holds exactly from b ≥ 8, which is what PROOF.md's "eventually" means.
   • T/2 ≥ 2n/b > 2Ndigits − 2.
   • Carries satisfy the sharper k_j ≤ Ndigits(2^b−1).
   • The final scale S² 2^(2b+4) turns an error C·2^(−4p) into one < 1/2 once b > (log2 C + 5)/20.

One minor presentational note. With only S ≥ 2Ndigits − 1, the product's top digit can land in the carry left after the last coefficient. This happens in 3 of the 8 toy products. The carry scan must flush it; it is at most one b-bit digit. At the real parameters S/T → 1, so this never matters there. No bound changes.

Evidence

verify.py uses only the standard library and takes about 9 seconds:

• Address map: 6,280 points checked against the source's own check_batched_crt.direct().
• Synthetic convolution: checked exactly in Q(ζ_(2r))[y]/(y^r+1) with rational arithmetic, for four shapes.
• Chirp: 195 even-t pairs checked exactly. All 18 coprime odd-t controls fail, as they should.
• Gaussian identity: 51 basis rows of the Poisson identity and the factorization, at five (s,t,α) up to (31,32,3), with worst residual 2.1e−58. Three controls are detected on every row where they can be: 1/s normalization (51/51), missing α^−1 (51/51) and +sk (46/46; the e_0 row is real and symmetric, so this control is blind there).
• End to end: 8 toy multiplications run through the full composed chain and recover the exact products. Scaling by S instead of S² fails, as it should.
• Recovery inequalities: checked exactly for 4 ≤ n < 2^14, plus 234 worst-case carry sequences.

Commands run locally (macOS, CPython 3.12):

python3.12 -B scripts/research_package.py --package research/pr4100-proof-composition-audit --check-only
  PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
python3.12 -B scripts/research_package.py --package research/pr4100-proof-composition-audit
  PASS_REGISTERED_RESEARCH_PACKAGE research/pr4100-proof-composition-audit outcome=completed
python3.12 -B scripts/check_research_commit.py --package research/pr4100-proof-composition-audit --check-source-history
  PASS_RESEARCH_COMMIT_BYTES {... "files": 8, ...}

Not covered

• The 2^−4p precision claim, which item 5's error bound assumes.
• Invertibility of N at θ = Θ(p^−2). This is GAUSSIAN.md's row gap; see Audit #4100's HALO locality witness: exact error identity and sharp (2J-1)W radius (no new κ) #4217's open question 1 and A centred prime-scale chirp keeps both corners positive, with a row sum above 1 (no new κ) #4304–The translated Schur diagonals are positive and at most 1 (no new κ) #4309.
• All costs (chirp head travel, the transforms, the Kronecker products, CRT).
• Prime existence, and the upstream Section 06/07 equivalences.
• The finite checks corroborate the written proofs; there is no proof-kernel check.

Task and overlap

• Card: uniform-transfer-audit, refined to PROOF.md's composition chain (recorded in TASK.json), priority revision 7.
• Base: canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244. Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 is pinned at 337d04939571a637aeab54a0f58f54fde811663a.
• Advance claim.
• Overlap was refreshed at 07:29 and 07:42 UTC. No other open PR or claim audits PROOF.md.

Open next questions

Both are in the README and TASK.json:

1. Bind the 2^−4p error to explicit constants. This is blocked by the all-size row gap.
2. Give the chirp odometer a literal fixed-tape lowering. Nothing blocks this.

Credit

The construction and every audited identity are Cinna Davis's #4100 (OpenAI Codex assistance), with its retained upstream lineage. This audit and verifier were prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

🤖 Generated with Claude Code