Skip to content

Prove dirty-private identity for PR2979's isolated cleanup - #3245

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/20261017-worker-5-cleanup-entrance
Oct 17, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/20261017-worker-5-cleanup-entrance

Conversation

@petalas

@petalas petalas commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

Summary

For PR #2979's original 5,207-gate cleanup, prove this exact block identity for arbitrary live and dirty private entrance arrays:

                 live input   private input
live output           A             0
private output        0            I_91

All 91 private arrays return unchanged at their literal last touches, with no private-to-live leakage, in both providers and orientations. The 72 warp maps are arbitrary noncommuting linear maps; no inverse or native phase identity is assumed.

Adds only research/rank7-cleanup-dirty-identity/, with a written proof, source pins, exact forward and backward checkers, receipts and controls. Answers PR #3238's explicitly unrun arbitrary-cleanup-entrance question and strengthens clean zero-return to dirty-private preservation. PR #3208 checks different R2 words and native obligations; it is credited, not repeated.

Base 463113d675af7410ac91d53a4fed51ec6494eb9a, priority revision 6. Contribution 171c95e2940341e56377d655a162635fa3caedfa. Both inputs match PR #2979 head be191346391661f4d35fc0d1508d0a6029572576. Canonical investigation.

Evidence

  • Before: PR Research: audit all PR #2979 private frees and their expanded native dependencies #3238's original-word proof depends on the preceding computation and clean private allocation. It explicitly leaves arbitrary cleanup entrance unrun.
    After: all 723 entrances are independent, including private dirt; the exact block identity passes. A separately implemented backward interpreter checks all 728 private rows/columns across providers and orientations without importing the forward checker or predecessor code.
  • Before: doubling literal gate 4844 is invisible when private entrances are zero.
    After: the dirty checker rejects its exact errors live302 -= d1003/4, private930 += d1003/8, private934 += d1003/8.
  • Eleven behavioral groups, optimized registered replay, source metadata/pins, Ruff and all 11 publication-byte comparisons pass. A Git-free committed export passes all tests under a second Python version. Environments: CPython 3.12.15 and 3.13.5, Linux x86_64, standard library only.
python3.12 -B scripts/research_package.py --package research/rank7-cleanup-dirty-identity

Canonical main and live overlap were refreshed before submission; no relevant upstream delta or overlapping dirty-cleanup result was found. Credit Marius-Paul Dumitrean, Jeremy Kothe, Mason Hale, Jeremy Diviney, commdata2338/PR #3238, 24kHandsome1201/PR #3208, ToikY and the retained construction lineage. Full source credit and open next questions are in the README.

Merge Danger

Door: two-way

Blast Radius: isolated

No frozen source, shared checker or selected-frontier change. This is a finite algebraic cleanup certificate, not native/physical supplier admission. The unchanged schedule still needs 91 distinct arrays; borrowing, ownership, movement and finite precision are unpriced. No stock, paid-profile or kappa improvement is claimed. The live block is not identity. Hosted CI, independent human review and full supplier/outer replay remain separate.

@Mister-Meeseeks
Mister-Meeseeks merged commit 87866a0 into CrocSwap:main Oct 17, 2026
2 checks passed
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.

2 participants