[petalas]

Result

Scoped counting proof with finite corroboration. No new κ, no selected-frontier change. Answers open question 1 of #4239.

Let rank-one idempotents P_i = u_i v_i (v_i u_i = 1) on F_q^m share one complete header G in GL_m(F_q), with request i passing when (G P_i G^-1)[0,0] != 0 (the #4239 interface). For any finite family, orthogonal or not:

Pr(all pass) = N / ((q^m - 1) q^(m-1)),
N = sum over S,T of (-1)^(|S|+|T|) [ q^(2m-1-r_U(S)-r_V(T)) - q^(m-1-mu(S,T)) ],

where r_U(S) and r_V(T) are the ranks of the image vectors and kernel functionals indexed by S and T, and mu(S,T) is the rank of the Gram block [v_j u_i]. For an orthogonal family this factorizes to #4239's J(q,m,k).

For two distinct requests (y = q-1), the joint count N by simultaneous type:

Type	N
same image, or same kernel	y q^(m-2) (y^2 q^(m-2) + 1)
orthogonal (PQ = QP = 0)	y^2 q^(m-3) (y^2 q^(m-2) - 1) (#4239)
one-sided (exactly one of PQ, QP zero)	y q^(m-3) (y^3 q^(m-2) + 1)
generic (tr(PQ) not in {0,1})	y q^(m-3) (y^3 q^(m-2) + q + 1)
degenerate (tr(PQ) = 1, distinct images and kernels, m >= 3)	y q^(m-2) (y^3 q^(m-3) + 1)

The generic law does not depend on the value of tr(PQ). tr(PQ) = 1 holds in four types with three different laws, so the trace alone does not determine the joint law. Every pair count is positive except the orthogonal pair at q = 2, m = 2 (already in #4239), so any two distinct non-orthogonal rank-one requests share a passing header over every finite field.

The proof is in research/projector-pair-header-law/README.md: a pairing-rank count on the subspaces cut out by the vanishing guards, after #4239's equal-fiber scalar-pair reduction (credited, and checked again here by complete conjugation on four small domains).

Evidence and reproduction

verify.py is standard-library only:

• an ordered-pair census over every pair of rank-one idempotents for (q,m) = (2,2), (2,3), (2,4), (3,2), (3,3), (4,2), (4,3), (5,2): 143,249 ordered pairs, each checked against its type's closed form, and each type also against the general formula;
• a complete GL conjugation census for (2,2), (2,3), (3,2), (4,2): 402 headers;
• 320 seeded three- and four-request families, half reusing an image or kernel, each direct count checked against the general formula;
• six controls (independence, trace-only typing, one-sided vs orthogonal, corrupted count, Z/4 in place of F4, generic F2 pair).

A local mutation pass (+1 on each of the seven closed forms, and on the general formula for k > 2) was rejected each time. That pass is local only and not committed.

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

Expected marker: PASS_PROJECTOR_PAIR_HEADER_LAW {"controls": 6, "families": 320, "headers": 402, "ordered_pairs": 143249}. All four commands pass locally; each verifier mode takes about 3 s (CPython 3.12, macOS arm64). RESULT.json is a generated receipt bound to every package file and to the two pinned sources.

Limitations

• Rank one only; finite fields only. Prove the exact joint header law for orthogonal rank-one requests #4239's Z/p^w equal-lift extension is not re-proved here.
• Algebraic header counts. Header selection, emission, dispatch, dirty return and stock are unpriced, and no actual request stream is shown to have these types. Nothing alleges an error in BIT.md's per-request recurrence.
• The census covers m <= 4, q <= 5; the theorems are written proofs for all q and m. Human and proof-kernel review are not claimed.

Open next questions

1. The joint full-guard law for nonorthogonal requests of rank greater than one. (The orthogonal arbitrary-rank case is claimed separately in Handoffs and requests for independent checks #1166.)
2. A real producer whose request rank data make a shared header useful, with the complete caller priced.

Related open work

• Prove the exact joint header law for orthogonal rank-one requests #4239 (head 5e24dfb5463d540721687d92c369609da5589523): orthogonal rank-one law. Its two-request example at q=3, m=2 gives 1/6; this census's orthogonal count there is 4/24 = 1/6, which agrees, checked numerically. Its general J(q,m,k) is the orthogonal specialization of Theorem 1. This PR adds the nonorthogonal types and the general-family law.
• Prove exact extreme-rank BIT header densities #4227 / Prove exact intermediate-rank BIT header densities #4228: single-request densities. Their rank-one value 7/12 at q=3, m=2 matches the "equal" count 14/24 here, checked numerically. Not recounted beyond that.
• Construct a paid pivoted BIT fallback with at most 1+12r children #4235, Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237: fallback child counts. Different quantity; no shared number.
• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215: good-packet normal-form check. Different quantity; no shared number.

CI notes

Hosted run 39492152544 is green on 9f9c89ed75e9fdae6b6762925b080fb308824858: plan passed in 3m19s and the registered package replay in 1m36s. No local obligation was delegated to CI, and no failed job remains.

Produced by Nick Petalas. Builds on #4239's interface and scalar-pair reduction, #4227/#4228's single-request laws, the retained controlled_normalizer.py lineage and #4100's BIT.md. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4240 projector pair header law at 9f9c89ed: 11/11

Code-disjoint local fork; RESULT compared by package verify. Head 9f9c89ed75e9fdae6b6762925b080fb308824858. CLAIM.

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

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