[petalas]

Summary

Scoped exact counting theorem with finite evidence, no new kappa. This answers the intermediate-rank question in #4227 and binds the resulting deterministic rate to the auxiliary BIT recurrence in #4100.

nonzero first pivot
  -> uniform rank-(r-1) idempotent Schur complement
  -> exact recurrence for every leading pivot
  -> exact good fraction and sharp first-order bad coefficient

For s=m-r and A=(q-1)q^s+1, the complete-cover good fraction is
A^r / (q^r [m choose r]_q). Exactly [q^(s-1) A]^r rank-r idempotents pass every leading pivot. The bad fraction is < (r+1)/q, and its first-order coefficient r+1 is sharp as q grows. Every retained BIT request therefore fits 43/(2^89-1) < 10^-16. The old sufficient numerator in BIT.md is 524288. The recurrence, invoices and selected frontier are unchanged.

The result is a written scoped proof, supplemented by enumerated finite certificates. It is not a complete multiplication theorem. Chris R / Clear1nsight's #3950 already supplies the degree-m polynomial argument, rank-seven deterministic interpretation and high-lift passage; those are credited predecessor results. The new result is the Schur-deletion law for intermediate ranks and its sharp coefficient, beyond the concurrent endpoint formulas in #4227.

Only research/bit-deterministic-bad-headers/ changes. Scientific base: 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. Publication commit: bb25dcedb5bbbacd3c35359eb6b5488b087bcde6.

Evidence and reproduction

Before: the retained BIT argument bounds the bad fraction by 2m^3/q. After: an exact fraction is proved for every rank, including intermediate ranks, with the bound above. Complete small-field enumeration checks 26,976 GL headers, 98,880 projector presentations and 132,576 determinant identities. A separate canonical RREF-image/left-inverse census checks all 13,490 nontrivial four-coordinate projectors over F2 and F3. The intermediate case m=4, q=3, r=2 has exactly 3,249 good projectors out of 10,530.

Every one of 7,776 complete Z/9 charts has its low-header decision and agrees with the retained normalizer. A further 1,536 three-coordinate charts test both ranks and every returned pivot ratio. Six controls reject omitted pivots, nonzero/nonunit confusion, a one-over-q shortcut, arbitrary subcovers, simultaneous-good charging and identically distributed pivot assumptions. A generated receipt binds counts to every package file and all six declared live inputs.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bit-deterministic-bad-headers
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/bit-deterministic-bad-headers/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/bit-deterministic-bad-headers/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/unconditional-batched-crt/check_bit_prime.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-deterministic-bad-headers --check-source-history

All commands pass locally on CPython 3.12.15, macOS arm64. The three registered commands take 1.385 s, 1.390 s and 0.018 s respectively, below their 120/120/30-second limits. These are check durations. Markers: PASS_BIT_DETERMINISTIC_BAD_HEADERS, PASS_COMPLETE_BIT_PRIME_CERTIFICATE, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. The preflight authenticates all 11 package/input files and declared source ancestry. The committed package export also passes its integrity checker. All three direct commands pass without Git, with all 12 exported files unchanged; an altered declared BIT.md input is rejected by its source hash before replay.

Limitations and unrun obligations

The all-parameter statement rests on the written proof. Executed fields are prime fields; extension-field execution is unrun. No independent human or formal proof-kernel review, GL64 enumeration, physical request/packet admission, all-size stock, fallback realization, recursive storage/tape/precision proof or downstream multiplication theorem is claimed. The count applies to fixed requests and complete equally weighted header packets. An arbitrary restricted cover can be entirely bad. No selected cold replay is needed or claimed because selected inputs are unchanged.

Open next questions

1. Bind the exact count to an emitted physical recursive header stream, preserving fresh stock, frozen ancestors and equal high-packet multiplicity. Start with one serialized caller; full fixed-tape compiler/stock admission remains open.
2. Sharpen the fallback child bill using actual swap orientations before repricing any recurrence. The fallback implementation itself is outside this proof.

Related open work

• Prove exact extreme-rank BIT header densities #4227 proves exact rank-one and corank-one densities and leaves intermediate rank open. Its published formulas agree numerically with this census at m=4, q=3: 495/1080 good at rank one and 343/1080 at corank one. This contribution supplies the unified intermediate-rank recurrence and answers its first open question; it does not claim the endpoint work as new.
• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215 checks the retained good-packet normal-form algebra. This is a distinct density theorem at its guard. Its reported aggregate corpus differs from this header/image census, so no shared aggregate is asserted or rerun.
• Admit delayed carrier retirement to the full logical BIT recursion #4183 changes a logical BIT word and its paid profile. That admission is not used here; no moment/root number is shared or compared.

The merged #3950 finite rows agree numerically at the four overlapping domains: bad fractions 20/48, 144/480, 468/2016 and 6528/11232. Its F17 row is not rerun. The earlier exact endpoint claim and this contribution's scope are linked in the README.

CI notes

Local metadata, all three registered commands, direct normal/optimized replay, committed-byte/source-history preflight and committed-export integrity pass. Hosted CI is green on publication head bb25dcedb5bbbacd3c35359eb6b5488b087bcde6: run 39484342645, plan passed in 3m6s and the package replay passed in 1m25s. The replay log confirms both scientific modes, the retained prime prerequisite and PASS_REGISTERED_RESEARCH_PACKAGE. No check failed.

Merge danger

Reversible isolated research package. Production sources, existing credits, invoices and the selected record are unchanged.

Credit

Produced by Nick Petalas. Cinna Davis supplies #4100; Chris R / Clear1nsight supplies #3950's polynomial/caller argument. Source527, commdata2338 and Jose Manuel retain the normalizer and recursive-closure lineage, with Ross Richardson's fallback algebra and the unchanged selected-source notices. Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4228 BIT deterministic bad headers at bb25dced: 14/14

Code-disjoint checks; local fork with nested PACKAGE/ROOT. Head bb25dcedb5bbbacd3c35359eb6b5488b087bcde6. CLAIM.

No packaging defect. PASS_BIT_DETERMINISTIC_BAD_HEADERS. Pins + nine SOURCES digests; fork rc=0.

Finite replay ≠ formal proof. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).