Repository navigation
Research: independent raw/projected cleanup ranges and sharp identity loops - #1420
Merged
Merged
Conversation
This was referenced Oct 14, 2026
Contributor
|
100-PR batch review at Merged to Reviewed scope: Uniform raw/projected endpoint range theorem and sharp five/six-XOR identity loops, with a full dirty PR589 cleanup counterexample. Original checker correctly rejects the altered cleanup; no defect in semantic-D or original H1–H5 admission is claimed. The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions. Batch review, attribution and evidence. Thank you for the contribution. |
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.
Knowing a feedback XOR word's complete raw endpoint does not determine the cleanup obtained by deleting target writes. This package proves the full joint range in every positive source/helper and target dimension, constructs raw-identity loops with any prescribed projected effect, and proves the sharp five/six-gate costs for an elementary effect.
The full 661-register PR589 witness inserts a five-gate identity loop before A. Original cleanup still restores every dirty register; compiled projected cleanup corrupts exactly helper222 by input223. Raw U/J/K, every frame path, paid profile (rank mass 5,129), and both scalar precision guards are unchanged or pass. The original owning checker correctly rejects the bad variant.
PROOF.md: constructiveGL(k+q,2) × {[A B; 0 I] : A invertible}range theorem, sharp elementary loop costs with arbitrary additional dirty registers, explicit general cost bound, and complete selected-word argument.-Oreplay produces the same canonical receipt:0afacad9740685e504cedfd9b81d85c702ae53ada78795a3662b4523f5a8e50d. Metadata/source pins, changed-package selection and clean patch application pass.One random draw selected
bit-mechanisms / bit-helper-contract(priority revision 2; nonce9092ff22c4d18f77e2b829eaae055120). The required starting example passed. The original semantic-D question is already covered by PR1194 and PR1311, so TASK explicitly records the adjacent feedback/cleanup scope change. Discussion 1396 contains the claim and handoff. OVERLAP records the fresh 842-open-PR / 137-discussion-record search and exact compared heads.Credit @woklerx's PR1105 for the original feedback-cleanup obstruction, four-block criterion and three-wire census, and PR1194 / Arham Tahir's PR1311 for the valid semantic-D substitution. This adds the uniform theorem, sharp identity-loop lengths and source-bound full-word witness. It does not challenge those substitution results. Retains credit to eumemic, DreamingOfClouds, Zhihao Chen, Dylan Crow, Sagar Thakrar and the helper-star lineage.
Scope: scalar XOR alphabet with target feedback; the witness uses a scalar compilation of projected cleanup and explicitly fails original literal H4. No improved κ or new supplier admission. Native 5/9/11-stage, physical ownership/hosting and outer assembly replays were not run; scalar envelope checks are not a new packed-precision proof. The all-dimension proof is written, not Lean-checked. Four live inputs and all frozen sources remain unchanged. Research provenance is pinned at
bce54fb3f895cbe5cd4c0eb477c3afeed100190f; the branch is rebased onto maincd91ac8e2652bfee6bf09da3b8724253bcf78f5f, with all four input bytes unchanged.Reproduce:
New work by Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance; Apache-2.0. No subagents or independent human review were used. Hosted CI and maintainer review remain separate from the passing local checks.