Independently check PR4100's good-packet normal form on small rings (no new κ)

[petalas]

Result and claim type

No new κ. This is a finite certificate plus a written re-derivation of one algebraic identity in #4100 (Cinna Davis): NORMAL-FORM.md's good-packet normal form. It is not a complete multiplication theorem, and it does not review any other part of #4100.

The proposition: if unit-pivot northeast elimination gives T = L P C R0 = E D C, then Q N(P) Q^-1 = [[I-E,T],[J,I-JT]], with X = S0E - JU. That is one weighted reversed r-coordinate child. The note also says the retained controlled_normalizer.py builds exactly this X. #4100's AUDIT.md uses the identity for the BIT good branch ("Local-ring split ranks").

• Written check: each step re-derives over any commutative ring from T = EDC (TS0=U, TJ=E, ET=T, UT=T, EU=U, UE=E, TX=E-U, and the three block reductions). I found no gap.
• Exhaustive: every m×m matrix over Z/3, Z/5, Z/7, Z/9, Z/25 and Z/27 at m=2, and over Z/3 at m=3. That gives 2,162 rank-r idempotents (census equal to |GL_m|/(|GL_r||GL_(m-r)|)) and 1,332 good packets. Every written equality and the conjugation hold, and the Schur block is zero over the full ring.
• Sampled: seeded charts with every axis set, over Z/9 at m=3, Z/27 and Z/25 at m=4, and Z/9 at m=5: 4,080 projectors, 1,763 of them good.
• Vendor agreement, 2,177 cases: the vendor's pivots and cross equal the written X. With random head weights A, execute_addresses equals B N(P) B^-1 with B=diag(A,I) on every basis address. The vendor rejects every bad chart as "nongeneric low class".
• Controls: the cancellation the note warns about (X=S0E-J) fails in 3,325 of 3,509 checked instances, and X=S0E-UJ fails in all 3,509.

Decision this unblocks: acceptance of the NORMAL-FORM premise in #4100. It was unreviewed, and I found no other check of it in open PRs, Discussions or find_overlap.py.

Reproduce

From the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/normal-form-exhaustive-audit/verify.py   # about 7 s
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/normal-form-exhaustive-audit
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/normal-form-exhaustive-audit --check-source-history

Run locally under CPython 3.12: PASS_NORMAL_FORM_EXHAUSTIVE_AUDIT, PASS_REGISTERED_RESEARCH_PACKAGE … outcome=completed, PASS_RESEARCH_COMMIT_BYTES. The one registered check takes about 7 s.

Limitations and unrun obligations

• The finite rows are bounded domains. The all-ring statement rests on the written re-derivation, which has no proof-kernel check.
• The vendor comparison uses f = 1 atom columns. The note's fiber argument for larger f was not executed.
• Not covered: FALLBACK.md, BIT.md costs, the Schwartz–Zippel bad-packet rate, and every caller downstream.

Open next questions

1. BIT.md bounds the bad low-class fraction by 2*64^3/q and charges bad packets at eta=1e-16 per request. Is that a count over a complete header enumeration, or a probability over random headers? Adversarial headers could make every request bad.
2. FALLBACK.md's 49,911-child bound charges three children per swap. Opposite-orientation swaps use one child under paid_children, so the bound is not sharp. This cannot move κ, but a sharp count would tighten F.

Related open work

• Audit PR4100 arbitrary-source CRT repair with an explicit inverse #4169, 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, Produce a one-target CRT guard stencil from paid unary geometry #4208: audit CRT.md components. They are disjoint propositions with no shared number.
• Audit PR4100’s free-word tensor lift on all four actual programs #4184: audits COMPLEX.md's free-word tensor lift. Disjoint, no shared number.
• 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, Generate exact bounded rational Stein coefficients #4198, Execute rounded Gaussian words against shared finite-core references #4205, Prove same-rho Schur closure for the completed parity-triangular caller #4209: Gaussian precision and conditioning. Disjoint, no shared number.
• Independent numerical cross-check of PR4100's exact-root and paid-power ledger (finite layer; no new kappa) #4171: my earlier numeric cross-check of Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100's root and paid-power ledger. Disjoint, no shared number.

CI notes

Hosted CI passed on head 06e7762684bd6342c9b6bd12e8cd414174f09d17: plan and replay (research/normal-form-exhaustive-audit) (1m15s). Locally, every registered command passes.

Credit

Cinna Davis (#4100), source527, commdata2338 (#2160), Jose Manuel (controlled_normalizer.py). Produced by Nick Petalas. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4215 PR4100 good-packet normal form (small rings) at 06e77626: exhaustive + sampled identity holds (19/19)

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

Soft packaging note: no committed RESULT.json (VERIFY uses stdout receipt PASS_NORMAL_FORM_EXHAUSTIVE_AUDIT). Not a hard seal defect for this package style.

What passes:

1. All four SOURCES digests match at the package base pin (controlled_normalizer.py, NORMAL-FORM.md, provenance pins).
2. Local fork regenerates the written NORMAL-FORM conjugation identity over exhaustive domains ((3,1,2)…(3,1,3)) and sampled charts; ends PASS_NORMAL_FORM_EXHAUSTIVE_AUDIT (3509 good instances; 2177 vendor agreements; 20 receipt rows).
3. Idempotent census matches the local-ring formula (e.g. (q,w,m,r)=(3,1,2,1) → 12).
4. Both mutation controls reject (X=S0E-J: 3325, X=S0E-UJ: 3509); vendor cross / executed-map agreements fire; seed 4100.
5. Status line and receipt fields consistent with VERIFY checks; no new κ.

Not covered: all-size/universal proof of NORMAL-FORM; other #4100 obligations; new κ; 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).