Skip to content

Prove the full-guard law for one-way coupled corank-one requests - #4274

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w10-1020g-oneway-header-law
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w10-1020g-oneway-header-law

Conversation

@petalas

@petalas petalas commented Oct 21, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Scoped counting proof with finite corroboration. For rank-one idempotents U,V with UV nonzero and VU=0, count complete GL_m(F_q) headers passing every leading-minor guard of both corank-one requests P=I-U,Q=I-V.

one-way kernel coupling
  -> partial-Gram endpoint [[1,1],[0,1]]
  -> exact all-field transfer
  -> binary numerator (9^(m-1)-5^(m-1))/4

Over F2, for every m>=2, the exact joint fraction is

(9^(m-1)-5^(m-1)) / [4(2^m-1)(2^m-2)2^(2m-4)].

It strictly exceeds #4261's orthogonal-kernel fraction while remaining below the product of the marginals. Values at m=2,3,4 are 1/6, 1/12 and 151/3360. This answers a higher-rank subcase of #4240's open full-guard question. No new kappa or supplier admission.

Only research/oneway-corankone-header-law/ is added. Canonical base 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. Advance claim.

Evidence

Before, #4261's joint full-guard law required orthogonal kernels. The new written proof normalizes one-way coupling and counts the changed terminal state. It is original counting work, not a predecessor audit.

  • 32,094 complete GL headers in six prime-field domains, with generic matrix conjugation, literal no-pivot elimination and all equal-fiber counts.
  • 1,946,574 normalized pairs with YX=[[1,1],[0,1]] in ten domains, separately enumerated and compared with the transfer.
  • 84 transfer cases, including every binary m=2..64. All 63 binary cases match the closed form and strict gain/correlation identities.
  • Five registered controls distinguish orthogonal coupling, wrong parity, omitted zero-factor multiplicity, independent marginals and first-pivot-only admission. At q=2,m=3, first-only admission accepts 66 headers while full admission accepts 14, out of 168.
  • Three local in-memory mutations are rejected for their intended reasons: orthogonal endpoint, zero-factor undercount and first-only matrix guard. A changed exported BIT.md source is rejected before scientific replay.

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

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

Expected markers: PASS_ONEWAY_CORANKONE_HEADER_LAW, PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed and PASS_RESEARCH_COMMIT_BYTES. The scientific receipt is generated on stdout and binds all six package files and both live inputs by SHA256. No handwritten receipt is stored.

The official committed export and integrity check pass. Its Git-free optimized replay produces the same receipt as the direct and registered modes; all eight exported payload files remain unchanged. Source ancestry and exact committed bytes pass at 497b8862d98ab57e33b262fa2631afc5a559257f.

Limitations and unrun obligations

The universal claim rests on the written scoped proof. Executed fields are F2,F3,F5,F7; extension-field execution is unrun. Only F2 has a closed form. Fixed one-way coupled kernels and complete equally weighted headers are essential. Pairs with both products nonzero, coincident images/covectors, restricted covers and finite local rings are outside scope.

Binary guards extend beyond the retained normalizer's odd-prime executable domain. No real producer, selection/emission, dispatch, dirty return, stock, precision or complete physical invoice is supplied. Those costs are unknown. No GL64 scan, selected cold replay, Lean, Docker or full multiplication theorem is claimed. Independent human and formal proof-kernel review are unclaimed.

Open next questions

  1. Count full guards when both UV and VU are nonzero. Start with endpoint [[1,a],[b,1]], separating invertible endpoints from the singular ab=1 case, where extra rank filters are needed to identify one conjugacy type.
  2. Pin an actual odd-field producer and charge its complete one-way shared-header caller, including selection, emission, dispatch, dirty return and stock.

Related open work

Fresh precommit PR and claim checks found no matching one-way full-chain claim. Targeted main-README and merged-title searches were also repeated; broader historical code-diff coverage is partial.

This contribution was produced by Nick Petalas. The cited counting packages are by Nick Petalas. Source527, commdata2338 and Jose Manuel retain the normalizer/recursive-closure lineage; Cinna Davis supplies BIT.md; Chris R / Clear1nsight supplies earlier #3950 counting context. No unmerged code dependency is imported. Apache-2.0.

CI notes

Hosted run 39524532666 passed on 497b8862d98ab57e33b262fa2631afc5a559257f: plan passed in 2m39s and the package replay passed in 1m25s. Both hosted scientific receipts exactly equal the local receipt, and the log contains PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed; the unchanged-input step passed. No failed check remains. The concurrent-work audit addition changes only this PR body; package files and the verified commit are unchanged. Local CPython 3.12.15 on Darwin arm64 passes both registered commands and both directly timed commands. Direct normal and optimized checks took 5.43 s and 4.55 s, each below its 120 s registered limit. These are check durations, not performance comparisons. Warnings are errors; local AST syntax/function-size checks pass. No standalone Ruff executable was available. All registered local obligations ran; none was deferred to CI.

Merge danger

Two-way door. Blast radius is the isolated research package and its opt-in replay. No selected-frontier change.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant