[petalas]

Summary

A scoped counting proof with a finite certificate gives the exact good-header fractions for rank-one and corank-one BIT projectors, in every dimension m >= 2 over every finite field of order q. The rank-one bad fraction is strictly below 2/q. Equal conjugation fibers and complete prime-power header packets preserve these fractions.

T = q^(m-1)(q^m-1)/(q-1)
good rank-one projectors   = q^(m-2)((q-1)q^(m-1)+1)
good corank-one projectors = (q^2-q+1)^(m-1)
good header fraction       = good projectors / T

This adds exact density formulas to the retained normalizer, beyond the earlier small-ring normal-form audit. It also states the complete-enumeration premise precisely: these are deterministic counts for a complete GL header domain. A wholly bad restricted low class and all its high lifts show why the fraction cannot be transferred to arbitrary header subsets. No new kappa or selected-frontier change.

Only research/projector-header-density/ is added. The scientific baseline is canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. SOURCES.json pins the retained selected-bit-recursive-closure normalizer and proof. TASK.json explicitly changes the current card's scope from a #4100 proof audit to this new counting theorem.

Evidence and reproduction

Before this contribution the extreme-rank density formula was not supplied by the retained normal-form argument. The new written proof uses rank-one factorizations and a weighted scalar-product walk. A generated receipt binds exact package bytes and both live inputs to the replay.

Local CPython 3.12 results:

• 951,417 matrix candidates give 2,162 nontrivial idempotents and 1,332 good packets.
• Complete scans enumerate 315,648 invertible headers. The actual retained normalizer agrees on 29,977 admission checks: complete small domains and both extreme ranks of GL3(F3), with a declared index-mod-97 sample at modulus 25.
• Canonical projector censuses cover dimensions through five, with a separate scalar-pair path check. Dropping zero coordinate products changes one checked count from 98 to 8; wrong reversal and final-minor-only controls reject. All 81 high lifts of the bad swap class reject.
• Both registered commands pass locally in 3.357 and 3.331 seconds, below their 180-second limits. These are check durations, not performance comparisons.
• PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES pass. The publication preflight checks all 11 package/input files and source history.
• The official committed export passes its integrity check. Both direct commands pass without Git, with all 12 exported files unchanged. Independent source-corruption, receipt-corruption and overwrite-refusal controls reject as expected.

From the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/projector-header-density/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/projector-header-density/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projector-header-density
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projector-header-density --check-source-history

Expected scientific output: PASS_PROJECTOR_HEADER_DENSITY {"good": 1332, "projectors": 2162}. RESULT.json is generated, never hand-written; the optional --write-receipt /new/external/path.json command creates a fresh candidate outside the checkout.

Limitations and unrun obligations

The universal result is the written scoped proof. Finite replay and separate mathematical/code checking do not supply independent human or formal proof-kernel review. Executable finite-field coverage uses prime fields; extension-field execution is unrun. No GL64 enumeration, intermediate-rank density, complete selected request census, fallback repricing, physical recurrence, supplier admission or complete multiplication theorem is claimed. The complete selected cold replay was not run because no selected input changes.

Open next questions

The package's intermediate-rank question now has a proposed answer in concurrent #4228. This PR does not audit that universal recurrence.

1. At one retained caller, bind complete equally weighted header packets and frozen-ancestor independence to the actual request stream.
2. Price every fallback child and restoration charge before substituting exact rates into an admitted bill. Physical supplier admission remains open.

Related open work

• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215 checks the good-packet normal-form identity. This contribution supplies a distinct all-dimension counting theorem; its independently enumerated 2,162 total / 1,332 good corpus agrees numerically with that PR's reported aggregate.
• Prove sharp fixed BIT repairs and a two-code hybrid controller #4194 uses rank-one idempotents for a different fixed bank-repair model. No density or call-count quantity is shared, so there is no overlapping number to compare.
• Prove exact intermediate-rank BIT header densities #4228 now proposes an exact all-rank recurrence, extending this package's endpoints. Substituting m=4, q=3 into its published formula agrees numerically with this receipt at both overlapping endpoints: 495/1080 good at rank one and 343/1080 at corank one. Its intermediate-rank proof is not checked here.
• Merged Prove conditional uniform R437 COPY contract and complete relative cost #3950 already supplies a rank-seven polynomial/caller bound and complete-header context. Its generic counting context is predecessor work; the exact extreme-rank formulas are the contribution here.

CI notes

Hosted run 39483788680 is green at exact head 3d793eade8de2ba49ec08f8d004c1b2f566a78e6: plan passes in 2m26s and the package replay passes in 1m30s. Both scientific PASS markers appear in the hosted log, along with PASS_REGISTERED_RESEARCH_PACKAGE. The unchanged-input check succeeds. No check failed. Local metadata, both registered checks, publication/source-history preflight and both Git-free export replays also pass.

Merge danger

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

Credit

Produced by Nick Petalas. Source527 and commdata2338 retain the normal-form algebra credit; Jose Manuel retains the recursive closure and normalizer credit. Chris R / Clear1nsight retains #3950's polynomial/caller context. DreamingOfClouds, eumemic, alephnan and the unchanged source notices retain the selected lineage. Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4227 projector header density at 3d793ead: 11/11

Code-disjoint checks; local fork with nested PACKAGE/ROOT; RESULT compared by package verify. Head 3d793eade8de2ba49ec08f8d004c1b2f566a78e6. CLAIM.

No packaging defect. PASS_PROJECTOR_HEADER_DENSITY (good=1332/projectors=2162). Pins + SOURCES digests; fork rc=0.

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