[petalas]

Summary

A scoped counting proof gives the exact joint full-guard header law for any laminar family of idempotents over every finite field. A laminar family has nested projectors and orthogonal siblings. Its joint fraction is

for each node v, including an unguarded ambient root:
    multiply the orthogonal-family law inside im(v) for its children

The new lemma is that Schur deletion preserves containment. Together with #4246's orthogonality lemma and law, it gives the product and an exact binary-field obstruction at any saturated even branch. At q=3,m=3, a rank-one projector inside a rank-two projector passes jointly on 343/1404 of headers; independent marginals give 931/4563.

The advance claim named the nested rank-one/rank-r case. The same containment lemma proves the more general laminar result delivered here. Claim type: scoped proof with finite corroboration. No new κ or supplier admission. Only research/laminar-header-law/ is added.

Evidence

Before, #4246 left nonorthogonal full-guard families open. The new written argument covers nesting and arbitrary-depth laminar families. The direct census checks 213,714 headers and every one of 1,056 laminar coordinate families across eight domains over F2,F3,F4,F5. All fractions and zero criteria agree. It checks 181,836 Schur-containment cases in both directions, plus six controls. An explicit nonnested commuting pair has noncommuting Schur complements, so that larger class requires a different argument. The stdout receipt is generated and binds every package file by SHA256.

From the repository root, any CPython 3.12 may replace this interpreter:

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

Expected markers: PASS_LAMINAR_HEADER_LAW, PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed, and PASS_RESEARCH_COMMIT_BYTES.

Limitations and unrun obligations

The universal claim is the written proof using the cited orthogonal-family theorem, not a proof-kernel result. The finite census reaches m=4 over F2 and m=3 over F3/F4. General overlapping commuting or noncommuting families, prime-power rings, incomplete/weighted covers and adaptive requests are outside scope. Header selection, emission, dispatch, dirty return, stock and actual producer/caller costs are unpriced. No selected cold replay or formal build is run. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Classify the changing Schur pair for two rank-two commuting projectors in dimension three with nonnested overlap. The explicit noncommuting Schur witness identifies the missing invariant.
2. Pin one actual laminar request producer and fully price its shared-header caller. The count alone supplies no physical saving.

Related open work

• Prove the joint full-guard header law for orthogonal requests of any rank (no new κ) #4246, head a2d99d73bf21b39fbb0a9a88917424ff26c2e63c: orthogonal arbitrary-rank law, used as a cited theorem. This package adds nesting and tree composition. Its flat rank-(2,1) example at q=3,m=3 is 14/117 here, agreeing numerically with the published value. No proof audit is claimed.
• Prove the joint header law for nonorthogonal rank-one requests (no new κ) #4240, head 9f9c89ed75e9fdae6b6762925b080fb308824858: nonorthogonal rank-one families at the first pivot. Distinct higher-rank/full-chain question here. Its equal-projector rank-one value at q=3,m=2 is 7/12; this package's single rank-one count agrees numerically.
• Prove the exact joint header law for orthogonal rank-one requests #4239, head 5e24dfb5463d540721687d92c369609da5589523: orthogonal rank-one law. Its q=3,m=2,k=2 example gives 1/6, agreeing numerically with this census's corresponding flat family.
• Prove exact intermediate-rank BIT header densities #4228, head bb25dcedb5bbbacd3c35359eb6b5488b087bcde6: single-request all-rank law and Schur deletion, cited steps. Its q=3,m=3,r=2 fraction is 49/117, agreeing numerically with this census's single rank-two case.
• Prove exact extreme-rank BIT header densities #4227, head 3d793eade8de2ba49ec08f8d004c1b2f566a78e6: extreme-rank marginal laws. Its q=3,m=2 rank-one fraction is 7/12, agreeing numerically with this census; no new marginal result is claimed.
• Prove the joint full-guard law for an overlapping corank-one pair #4261, head 4728fc766b3084f3ab2f5c8543a5e74e4a12b126: concurrent overlapping corank-one pair law. That pair is neither nested nor orthogonal when m>2, so it is outside this laminar theorem. Its common flat q=3,m=2 boundary is 1/6, agreeing numerically with this census. Its count does not classify the changing Schur pairs asked about in this package's first open question.
• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215: retained good-packet normal form. Different algebraic question, no shared aggregate count compared.
• Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100: the proposed BIT request/complete-header context. This package derives a joint counting law; it does not audit or admit that construction, and no recursive bill or κ is shared.

CI notes

Local environment: macOS 27.0.1 arm64, CPython 3.12.15. Warnings are errors in both registered modes. No standalone Ruff executable was available; code diagnostics used Python warnings and AST inspection.

Local metadata, both registered mathematical checks, and the five-file committed-byte/source-history preflight pass at 2a582d8f66d1900b22ee2cd0062ee5dca94e8f85. The final registered two-command replay took 156.13 seconds total; each command was below that total and its 300-second limit. Separately timed direct normal and optimized commands took 44.99 and 61.70 seconds. These are check durations, not performance comparisons. No local obligation was delegated to CI. Hosted run 39504972933 is green on the same exact head: plan passed in 4m10s and the package replay passed in 3m20s. Both complete hosted receipts equal the local receipts, including every package-file SHA256 and all mathematical fields. The helper suite reports 312 tests, 11 skipped. Both registered normal/optimized checks and PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed are present in the hosted log. No check failed and no registered obligation remains unrun.

Merge danger

Two-way door. Blast radius is the isolated research package. No selected-frontier change.

This package was produced by Nick Petalas. It builds on Nick Petalas's #4228/#4239/#4240/#4246 and Cinna Davis's #4100 request context. Apache-2.0.