Repository navigation
Audit: exact gate-operand parity contract at the checker/exporter boundary (answers PR3696 OQ1; no new kappa) - #3738
Merged
Mister-Meeseeks merged 1 commit intoOct 20, 2026
Conversation
…export boundary Answer the supplier-boundary cascade's remaining open question (PR3696 OQ1, following CrocSwap#2977/CrocSwap#2992/CrocSwap#3004 and scatter-parity-contract-audit): for one gate (d, srcs), the pinned symbolic checker operator (accumulate-then-write) and the pinned exporter operator (sequential per-source ADD) agree as linear maps over F2^n iff d is absent from srcs, or the destination multiplicity is odd and every register occurring before the destination's last occurrence occurs an even number of times there. Measured on 9330 (d, srcs) pairs (6 registers, source lists length 0..4, the published census domain, extended to 55986 pairs at length <= 5): destination- free 4686 all agree; destination-in 4644 split into 3492 divergent and 1152 agreeing; simulation and the independent coefficient prediction agree on 100% of pairs. Guard census: the checker's own contract and distinct-only and dest-free-only are sound with 4608 / 4602 / 1152 agreeing rejections (smallest nonempty destination-free witness [a,a]); a transplanted scatter simple-support guard is unsound, admitting 1350 divergent gates; the exact minimal guard is sound with zero over-rejections. The pinned selected tuned word has 5472 D/A/B/C gates, all with distinct nonempty operands, so every sound guard preserves its export; its 111 scatter rows are simple supports. No new kappa (selected 0.001672660197076918 unchanged); no production adoption; frozen packages unchanged. Reproduce: python3.12 -B scripts/research_package.py --package research/gate-operand-parity-contract
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.
Summary
Bounded boundary audit, no new κ (selected
0.001672660197076918unchanged). New packageresearch/gate-operand-parity-contract/, completing the checker/exporter schema cascade's remaining open question — PR #3696's open question 1 (itself refining #3004 under #2977's cascade):The exact gate-operand parity contract. For one gate
(d, srcs)the pinned symbolic checker operator (xcheck_p.py: accumulate pre-gate XOR, then write once) and the pinned exporter operator (export_records.py: one sequentialADD(d, s)per listed source) agree as linear maps over F2^n iffd ∉ srcs, or (m_dodd and every register occurring before the destination's last occurrence occurs an even number of times there).Measured (independent re-implementation, stdlib only; simulation vs an independent coefficient-level prediction agree on 100% of pairs;
-O-enforced admissions):[d]+srcsdistinct) sound, 4,608 agreeing rejections; distinct-only sound, 4,602; dest-free-only sound, 1,152 (exactly the agreeing destination-in residue); transplanted scatter simple-support unsound — admits 1,350 divergent gates (destination in sources but not first, e.g.[a,d]); exact minimal guard sound with zero over-rejections (accepted chain 1,230 ⊂ 1,236 ⊂ 4,686 ⊂ 5,838, all matching closed forms).[a,a]; smallest overall: the empty source list, which agrees but the checker rejects as malformed). Every rejected agreeing list is already checker-rejected (bad operands), so adopting the checker's own operand contract at the exporter aligns the two boundaries without affecting any checker-accepted word.e3e301e6…,v=111,R=439) has 5,472 D/A/B/C gates, all with distinct nonempty operands, and 111 simple scatter rows (9 retained totals, 527 terms) — every sound guard preserves each selected gate's export. Gate-list census only; the 27,234/27,235-record stream counts are PR Research: gate-operand export parity — dest-free always agrees; dest-in can diverge (answers #3004 OQ2; no new kappa) #3696's published measurements, cited not re-derived.Task and overlap
supplier-boundary-audit,scope_status: changedwith the reason recorded inTASK.json: the scatter side is settled on main (scatter-parity-contract-audit+ Enforce simple scatter supports at opt-in checker and exporter boundaries #2992/Repair scatter export with a versioned XOR-normalized boundary #3273/Compose integer labels with checked XOR scatter export #3346), and this takes PR Research: gate-operand export parity — dest-free always agrees; dest-in can diverge (answers #3004 OQ2; no new kappa) #3696's stated open question 1.20ecf2891d80b5acf18d980b2164fb44ea7faa90(current main).scripts/find_overlap.py --task supplier-boundary-auditand by reading the cascade packages; a CLAIM was posted in discussion Handoffs and requests for independent checks #1166 before the work. No open PR touches gate-operand schema selection as of submission.Validation
All commands from a repository root, CPython 3.12.15 (
~/git/integer-mult-bounds/.venv/bin/python3.12, used read-only):Expected:
All five checks were run locally and pass. No native backend, Lean, Docker or historical replay was run; the native-rejection question stays open (see package OQ2) and CI replay is welcome as additional certification.
Credit
Credit Nick Petalas for the scatter multiplicity gap (#2977); Kumagi for the exact scatter agreement contract (#3004); Wentao Li (VictorLiwentao) for the gate-operand census, witnesses and the open question completed here; Dylan Crow for the exporter; eumemic for the symbolic checker; and the retained tuned-word lineage. This contribution was produced by Nick Petalas with AI assistance. No independent human or proof-assistant review is claimed.
Open next questions