Repository navigation
Prove the two-relation rank bound at arbitrary helper width (no new κ) - #6777
Merged
Mister-Meeseeks merged 1 commit intoNov 10, 2026
Conversation
Prepared for @CubeJerry with substantial OpenAI Codex assistance and a separately authored mathematical review. No new kappa.
This was referenced Nov 6, 2026
This was referenced Nov 8, 2026
Draft
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Extend #720 and #1456 to arbitrary finite scalar width and word length: in the formal binary rank-one-idempotent model, at most two integral frame relations force every diagonal target to use a disjoint subset of paid frames. Total target rank cannot exceed paid rank. The new all-width image classification and arbitrary odd-core argument exclude eight calls of span six for three invertible 3x3 targets. The historical four-register census in #1846 is credited, not claimed as new.
Base and inherited source revision: 7c49fe3.
Exact #720/#1456/#5921 proof blobs: SOURCES.json.
Proof SHA256: ad05bccffaf0fe11120312d8514146e5433d7032bbc65bd9d57974e06a6c3f82.
Reproduce (Python 3.12, stdlib):
Expected:
PASS_TWO_RELATION_ANY_REGISTERSandPASS_REGISTERED_RESEARCH_PACKAGE.Executed: all 4,964 historical pattern planes, 108,165 width-five planes, 20,097 odd-core prefix cases, invariant-block and exact-endpoint controls. Missing planes, invalid invariant spaces, deleted calls and missing cleanup are rejected. Separate written review checked the universal reduction and the precise inherited #720 lemma. Normal/-O, metadata, certificate regeneration, committed-byte/mode, export and Git-free replay passed.
No new κ. Torsion-free exponents, binary rank-one idempotents and exact diagonal monomial endpoints are required. The #720 theorem is inherited; finite checks do not prove unbounded quantifiers. Span five, three or more relations, other alphabets and physical supplier costs remain open. All five selected assumptions remain.
By @CubeJerry with substantial OpenAI Codex assistance and separately assigned mathematical review. Credit David Govea (#720), woklerx (#1456/#1846), Nick Petalas (#5921), Ali Romman and the pinned lineage. No human/proof-kernel acceptance.
Proof, pins and limits: https://github.com/CubeJerry/integer-mult-bounds/tree/e62a9d0d4143e11c190fcb4d81d83dc1662da782/research/bit-two-relation-any-registers
Complete remote Git tree matches the tested contribution.