Repository navigation
Tooling: sparse exact U8 phase compilation with identical recipes - #1029
Merged
Mister-Meeseeks merged 1 commit intoOct 13, 2026
Merged
Conversation
thakrarsagar
added a commit
to thakrarsagar/integer-mult-bounds
that referenced
this pull request
Oct 14, 2026
- The producer's lower_child check (signed Z4 tableau plus column 0) is complete but not independent; K2 is a control on this package's own comparator, not a gap in the producer's check. Lemma G's I-tr and check_adapters.py ran on four other words. - Scope is record level for CLIFFORD-RECIPES.json; identity adapters are 866 per orientation (352 entry + 514 exit). - Gate-order equivalence holds on all 224 adapters (counted in RESULT). - B3 accepts only the selected record or checkpoints/frontier1094.json; B8 uses a path pin in the source manifest. - Tests (26): mutated child/adapter records rejected by evaluate(), receipts cover each pair once, measured digit bound on the 16-gate identities and a beta = 2K collision, I5/I6/I7 and fixture-pin negatives, calibration reproduced. - Credits: HyperplaneEnd Lean (jeremykothe2, CrocSwap#593), Lemma G (DreamingOfClouds), CrocSwap#433 H6 identities, PR425 (jacklightChen), CrocSwap#1029/CrocSwap#662 engines.
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
2 participants
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.
The complete selected U8 phase compiler spends most of its time on exact
Clifford state evaluation. This optional entry point stores only nonzero
Gaussian amplitudes, uses the unchanged PR662 gate tables, and removes exact
cancellations after each mixing gate. It preserves every frame, directed
edge, endpoint, tableau and global-phase check. Verification tooling; no
new kappa or circuit.
Three alternating rounds of complete fresh-process commands on Python
3.14.7/macOS arm64 gave:
The ratios of median times are 2.20× against PR662 and 16.44× against
the original driver. The sparse command used 5.09 MiB more peak memory than
the dense command. The host was shared and OS caches were not flushed;
measurements are descriptive, with no timing threshold. Timings include
imports, source admission for the optional entry points, parsing, all
lowering checks and output writing. Raw wall/CPU/memory samples and source
hashes are in
research/selected-replay-fastpath/evidence/.All nine runs produced identical complete recipe bytes and identical review
fields except elapsed seconds. The pinned input contains 1,005 frames,
2,949 directed edges and 224 endpoint adapters. The exact recipe SHA256 is
4629507dcbdd516457c001ff8f9dbe750d1a0cbfa5cfa3c6be003d45804ba0c5.Validation
states and 540 mixed-circuit states with the retained scalar evaluator.
All gate kinds, both mixing signs, zero displacement, dimension zero,
cancellation and inverse circuits are covered.
Four corrupted words are rejected by the actual original command and
both optional engines: 12 rejection cases.
are rejected. A relocated minimal source tree passes.
reviewed the source and proof. This is separate AI review, not independent
human review.
selected certificate, frozen predecessors and
upstream/are unchanged.and 3.14. Hosted CI has not been run for this proposal.
Reproduce from the repository root with a fresh output path:
Expected:
PASS_COMPLETE_U8_PHASE_RECIPES_IDENTICAL.The proof in
PROOF.mdgives an exact gate induction, including sparsecancellation and denominator normalization. The optional lowering uses
normal evaluator arguments. It does not patch retained functions or change
the default selected replay. The public entry point rejects
-Obefore itloads the retained assertion-based algebra.
Base:
8bddbee377e2f3ce1f1247196c4b290d55767d20. PR662 supplies the directdense baseline and the imported gate tables. PR942 supplies the pinned U8
replay archive. PR1006's T37 occupancy audit and PR900's historical rank
reduction change separate paths; neither is imported. New local-word
proposals are outside this benchmark.
This is a complete phase-compiler measurement on archived U8 input, not a
fresh supplier reconstruction or whole-frontier speed measurement. Full
make verify, selected cold reconstruction and Lean were not run. Allinherited compiler, realization, hosting, precision/tape, analytic and bit
interface obligations remain.
Prepared for Ali Romman with substantial OpenAI Codex assistance. Source
credit is retained for Charles Bethin's PR662 tables, the exact Clifford
compiler, Jonathan Capalbo's PR942 archive, and the U8/controller lineage.
See
NOTICE.md. Apache-2.0. No independent human review or priority forsparse state propagation is claimed.
The coordinator also reran the complete sparse command and checked every recipe byte and every review field against the pinned archive. The source freeze matches the repeated benchmark.