Repository navigation
Conversation
Prove whole-endpoint compression with w <= floor((k-t)/2), retaining frames, order, data components and scalar pairings. Includes independent exact checkers and explicit scope counterexamples. No new kappa. Prepared for @CubeJerry with substantial OpenAI Codex assistance and separate AI proof/code review. Apache-2.0.
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.
Prove that any exact k-call scalar-idempotent word with t nonidentity data targets and arbitrarily many exactly restored helpers has an equivalent word with w = rank_F2(V^T U) <= floor((k-t)/2) helpers. It preserves paid frames, call order, data components and all scalar pairings, with the complete new endpoint proved on arbitrary helper inputs.
For #4118's exactly restored subcase, five calls and three data targets reduce to at most one helper; #720 excludes zero helpers under its hypotheses. The four-register question and broader nonidentity-helper problem remain open. New relative to retained rank arguments: the constructive quotient preserves every endpoint block. Its minimum is restricted to the stated preservation contract.
Base: 7c49fe3.
#4118 head: 9f7beec.
#720 head: a942c0a.
Canonical blob/SHA256 pins are in SOURCES.json; replay is self-contained.
Reproduce (CPython 3.12, stdlib):
Expected: PASS_RESTORED_HELPER_COMPRESSION, PASS_C_INDEPENDENT_COMPRESSION_REVIEW and PASS_REGISTERED_RESEARCH_PACKAGE.
Executed normal/-O: all 4,096 pairs of 2x3 helper matrices, 64 data-block checks, 16 structured words, 64 nested-inverse words (seed 2026110617), seven rejection controls. A separate implementation checks 448 factorizations, 181 full endpoints, 121 reductions and six counterexamples. Nonrestoration, zero frames, identity-target counting and false pairing/minimality claims are challenged. Proof/code reviews, committed bytes/modes, export integrity and four Git-free replays pass. Remote full tree matches.
No new κ. Nonzero calls, nonidentity targets and exact whole-matrix restoration are essential; the constructor does not certify those endpoint premises. No 120^5 census, native saving, supplier admission or human/formal acceptance. All five selected assumptions remain. No selected cold-replay PASS or full-history preflight claim.
By @CubeJerry with substantial OpenAI Codex assistance and separate verification/review. Credit Ali Romman (#468), eumemic (#288), waynenilsen's arbitrary-register treatment, David Govea (#720) and unpaidmoon (#4118). Apache-2.0.
Proof, reviewed hashes, exact controls and open questions:
https://github.com/CubeJerry/integer-mult-bounds/tree/3b3d6670d509fd74c1780cfacdf550badf8871db/research/restored-helper-compression