[petalas]

Summary

Scoped counting proof with finite corroboration, answering a subcase of #4240 and #4246's nonorthogonal full-guard question. For orthogonal rank-one kernels U,V on F_q^m, count one complete GL_m header passing both corank-one requests P=I-U and Q=I-V. Their images overlap when m>2.

partial 2x2 Gram matrices
  -> q^2(q-1)^2 safe states
  -> exact all-field transfer law
  -> binary density:
(9^(m-1)-2*7^(m-1)+5^(m-1)) / [4(2^m-1)(2^m-2)2^(2m-4)]

Over F2 a common passing header exists exactly for m>=3. The passing events are strictly negatively correlated. The fractions at m=3 and m=4 are 1/84 and 1/80. No new κ or supplier admission.

Only research/corankone-pair-header-law/ is added. Scientific base: canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. Advance claim.

Evidence

Before: single-request marginals do not determine the joint full-chain fraction. After: PROOF.md supplies the transfer theorem and binary closed form; three counts agree:

• 32,274 complete GL headers in seven domains, with literal no-pivot elimination for both requests and complete equal-fiber counts.
• 2,007,234 normalized pairs X,Y with YX=I_2 in 12 domains, enumerated separately from the GL census and transfer. Fields are F2,F3,F4,F5, dimensions at most six. F4 uses x^2+x+1.
• 99 transfer cases: binary m=2..64 and q=3,4,5,7 with m=2..10. All binary cases agree with the closed form. All local rank-one increment multiplicities are separately enumerated.
• Four controls distinguish independence, a lost zero factor, wrong parity and first-pivot-only admission. At q=2,m=3 the full-chain count is 2, while the first-pivot-only count is 54, out of 168 headers.

Both registered commands and both direct modes pass locally on CPython 3.12.15, macOS arm64. Direct normal and optimized runs took 15.16 s and 15.54 s wall time; the registered pair took 31.88 s. These are check durations, not performance claims. Each registered command has a 120 s limit. Ruff 0.14.0 E/F/B/UP passes. Four local mutations are rejected for their intended mathematical/source-check reasons: wrong binary eigenvalue, omitted zero-factor multiplicity, first-pivot-only admission and source corruption.

From the repository root, with any CPython 3.12 replacing this local interpreter path:

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

Markers are PASS_CORANKONE_PAIR_HEADER_LAW, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. The scientific output includes every census numerator/denominator and generated SHA-256 bindings for all package files and both declared inputs. No receipt is handwritten. All eight committed package/input files and source ancestry pass preflight at 4728fc766b3084f3ab2f5c8543a5e74e4a12b126. The official committed export and integrity check also pass. Its Git-free direct replay produces the exact same generated receipt as both committed registered modes, and all eight exported source files remain unchanged.

Limitations and unrun obligations

The universal claim is the written proof. The replay covers only the stated finite domains. Fixed idempotents with orthogonal rank-one kernels and a complete equally weighted header domain are essential. Only q=2 has a closed form here. Binary guards extend the algebra beyond the retained normalizer's odd-prime executable domain. No real producer, header selection/emission, dispatch, dirty return, stock, precision or complete physical invoice is supplied. Those costs remain unknown. No formal-kernel proof, selected cold replay, Lean or Docker run was performed. Independent human and formal proof-kernel review are unclaimed. The selected frontier is unchanged.

Related open work

• Prove exact extreme-rank BIT header densities #4227 (3d793eade8de2ba49ec08f8d004c1b2f566a78e6) supplies the corank-one determinant identity and marginal law. All 12 marginal fractions agree numerically here. The joint law is new.

• Prove exact intermediate-rank BIT header densities #4228 (bb25dcedb5bbbacd3c35359eb6b5488b087bcde6) supplies all-rank single-request densities. Its corank-one specialization agrees numerically in those same 12 cases; its intermediate-rank recurrence is not used.

• Prove the exact joint header law for orthogonal rank-one requests #4239 (5e24dfb5463d540721687d92c369609da5589523) counts orthogonal rank-one joint guards. At m=2 the five q=2,3,4,5,7 transfer fractions agree numerically with its (q-1)(q-2)/(q(q+1)), including 1/6 at q=3. The new case has m>2.

• Prove the joint header law for nonorthogonal rank-one requests (no new κ) #4240 (9f9c89ed75e9fdae6b6762925b080fb308824858) counts nonorthogonal rank-one first guards. This answers a higher-rank full-chain subcase of its first open question. Only the same m=2 orthogonal boundary overlaps, with all five numerical values agreeing.

• Prove the joint full-guard header law for orthogonal requests of any rank (no new κ) #4246 (a2d99d73bf21b39fbb0a9a88917424ff26c2e63c) counts full chains of orthogonal requests. The overlapping-image pair here is outside that hypothesis for m>2. Its m=2 rank-(1,1) boundary agrees numerically on the same five values.

• Prove the exact full-guard header law for laminar projector families (no new κ) #4259 (2a582d8f66d1900b22ee2cd0062ee5dca94e8f85) proves the laminar-family full-guard law. P,Q here are neither nested nor orthogonal for m>2, so this supplies the nonnested overlapping-pair count beyond that law. The common flat q=3,m=2 boundary is 1/6 in both, checked numerically. Its open question 1 asks for the changing Schur-pair classification; this count does not classify those Schur pairs.

The preceding counting packages were produced by Nick Petalas. The retained normalizer and recursive-closure lineage is due to source527, commdata2338 and Jose Manuel; Cinna Davis supplied BIT.md; Chris R / Clear1nsight's #3950 is earlier deterministic counting context. Exact retained contract pins and credit are in the package. No unmerged source code is imported.

Open next questions

1. A closed form or smaller invariant transfer for odd q. Start with the q=3 matrix, preserving both diagonal guard values and rank(I-A).
2. Three or more corank-one requests with orthogonal rank-one kernels. Start with a 3x3 partial Gram matrix over F2 at m=3,4.
3. A real odd-field producer and fully charged shared-header caller, including selection, emission, dispatch, dirty return and stock.

CI notes

All local registered obligations passed. Hosted run 39505168435 is green on 4728fc766b3084f3ab2f5c8543a5e74e4a12b126: plan passed in 2m38s and the package replay passed in 1m27s. Both hosted normal/optimized scientific receipts exactly equal the local committed and Git-free export receipts, and PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed is present in the log. No check failed, and no registered local obligation was delegated to CI.

Merge danger

Two-way door. Blast radius: package. This adds one isolated research package and its bounded replay; existing scientific sources and the selected record are unchanged.

This contribution was produced by Nick Petalas. Apache-2.0.