[petalas]

Result

This PR proves the exact fraction of a complete GL_m(F_q) header cover on which k pairwise orthogonal idempotents of arbitrary ranks r_1,...,r_k all pass their full leading-minor guards (sizes 1..r_i) at once, over every finite field.

With the first-stage factor

F(q,n; s) = prod_i (q^s_i - 1) · [(q-1)^k q^e - (-1)^k] / [q^k (q^n - 1)],   e = n - sum s_i,

the joint fraction is the stage product

J(q,m; r) = prod_{t=0}^{max r - 1} F(q, m-t; (r_i - t : r_i > t)).

Its single-request specialization is #4228's law, and its all-rank-one specialization is #4239's J(q,m,k). The guards are dependent. At q=3, m=4, two orthogonal rank-two requests pass together on 88/1755 ≈ 5.0% of headers, while the product of the marginals is (361/1170)^2 ≈ 9.5%.

Zero locus and cover. J = 0 exactly when q = 2, the family is complete and k is even. In that case exactly two headers cover the family; otherwise one does. This extends #4239's cover theorem from rank one to arbitrary ranks under the full guard chain.

The new step is a Schur-orthogonality lemma. At nonzero first pivots, the Schur complements of pairwise orthogonal idempotents are again pairwise orthogonal idempotents of ranks r_i − 1. Conjugation by diag(1,K) makes their conditional law uniform on one GL_{m−1} orbit, and induction gives the product.

Claim type: scoped counting proof with finite corroboration. No new κ, no supplier admission, no complete multiplication theorem, no selected-frontier change. Card uniform-transfer-audit, with the scope changed to a new shared-header counting question (recorded in TASK.json). Only research/orthogonal-chain-header-law/ is added. Base: canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. Advance claim.

Evidence

verify.py uses two independent enumerators. F4 is F2[x]/(x^2+x+1).

• Complete GL census over F2 (m=3,4) and F3 (m=3): 31,560 headers and all 29 rank compositions. For each composition it checks the full law of the passing set by inclusion–exclusion over subfamily stage products. On every header with all first pivots nonzero it checks the Schur lemma directly: idempotent, rank r_i − 1, pairwise orthogonal. It also checks that the conditional Schur tuple is uniform on an orbit of exact size, and that the cover number is 1 or 2 as stated.
• Row/column-pair census: all 1,937,856 pairs (X,Y) with XY = I_2 over F3 (m=4), F5 (m=3), F4 (m=3) and F2 (m=6), across 11 rank tuples, each checked against the full passing-set law.
• Zero-locus and two-header grid over 3,514 tuples (q ∈ {2,3,4,5,7,8,9}, m ≤ 8). 180 specializations reproduce the Prove exact intermediate-rank BIT header densities #4228 and Prove the exact joint header law for orthogonal rank-one requests #4239 closed forms.
• Four controls are rejected: the independence product, a recursion that holds the free dimension fixed, a nonorthogonal pair sharing an image, and an altered count.

From the repository root (any CPython 3.12 can replace the interpreter path):

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/orthogonal-chain-header-law
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/orthogonal-chain-header-law --check-source-history
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/orthogonal-chain-header-law/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/orthogonal-chain-header-law/verify.py

Expected marker:

PASS_ORTHOGONAL_CHAIN_HEADER_LAW {"controls": 4, "formula_grid": 3514, "gl_headers": 31560, "gl_rank_tuples": 29, "pair_rank_tuples": 11, "pairs": 1937856, "specializations": 180}

Local results on macOS arm64 with CPython 3.12.15:

• --check-only metadata passes.
• check_research_commit.py --check-source-history passes at a2d99d73bf21b39fbb0a9a88917424ff26c2e63c.
• The registered replay runs both modes and ends with PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed.
• Each mode used about 78 s of CPU time. Wall time was about 3 min per mode on a loaded machine. These durations are not performance claims.

Limitations and unrun obligations

The universal claim rests on the written proof; the enumerations are finite corroboration. Neither is a proof-kernel result. Orthogonality, fixed idempotents and complete, equally weighted headers are essential premises. The census does not reach m = 64 or rank 42. Not supplied: prime-power lifts, any actual request stream, physical selection/emission/dispatch/dirty-return cost, stock, fallback repricing, and selected or outer replay. Nonorthogonal families are outside scope. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Does the stage product extend to commuting but nonorthogonal idempotents, or to families with prescribed image/kernel intersections? Only the Schur-orthogonality step uses P_i P_j = 0. A first step is to compute one pivot stage for two idempotents with P_i P_j ≠ 0 and identify which pair invariant survives.
2. Can an actual orthogonal BIT request family use a fully charged shared-header caller? Pin one producer family with its ranks, then charge header selection, emission, dispatch, dirty return and stock. The joint law and cover theorem supply none of those prices.

Related open work

• Prove the exact joint header law for orthogonal rank-one requests #4239 (head 5e24dfb5463d540721687d92c369609da5589523): the joint first-pivot law for orthogonal rank-one requests. This package's all-rank-one specialization equals its J(q,m,k) on 180 cases (q ∈ {2,3,4,5,7}, m ≤ 9, k < m), and gives 1/6 at q=3, m=2, k=2, matching its stated value; both checked numerically. New here: arbitrary ranks and the full guard chain.
• Prove exact intermediate-rank BIT header densities #4228 (head bb25dcedb5bbbacd3c35359eb6b5488b087bcde6): the single-request law for all ranks. The k=1 specialization equals its closed form A_s^r / (q^r [m r]_q) on the same 180 (q,m,r) cases, checked numerically; this PR uses its Schur deletion and dot-product counts as cited steps.
• Prove exact extreme-rank BIT header densities #4227 (head 3d793eade8de2ba49ec08f8d004c1b2f566a78e6): extreme-rank single-request densities. They are covered by the same k=1 specialization; no joint quantity is shared.
• Prove the joint header law for nonorthogonal rank-one requests (no new κ) #4240 (head 9f9c89ed75e9fdae6b6762925b080fb308824858): nonorthogonal rank-one pairs at the first pivot. Its orthogonal-pair row y^2 q^(m-3)(y^2 q^(m-2) − 1)/D agrees with this law at ranks (1,1) for q ∈ {2,3,4,5,7}, 2 ≤ m ≤ 8, checked numerically. The two packages are disjoint otherwise: that one covers nonorthogonal rank-one pairs, this one orthogonal families of any rank.

CI notes

Hosted run 39493585632 is green on head a2d99d73bf21b39fbb0a9a88917424ff26c2e63c: plan passed in 2m47s and the package replay in 7m9s. The log shows the exact local marker in both the normal and -O modes, each taking about 2m53s, which is under the 10-minute per-check limit. It also shows PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed. No check failed, and no registered obligation was left unrun.

Credit

Produced by Nick Petalas. Builds on Nick Petalas's #4228 and #4239; Cinna Davis's #4100 BIT.md poses the per-request guard accounting. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4246 orthogonal chain header law at a2d99d73: 7/7

Code-disjoint local fork (stdlib field enumerators). Head a2d99d73bf21b39fbb0a9a88917424ff26c2e63c. CLAIM.

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

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