diff --git a/research/hpe-post-wrapper-lemma/README.md b/research/hpe-post-wrapper-lemma/README.md new file mode 100644 index 0000000000..c8abcb4461 --- /dev/null +++ b/research/hpe-post-wrapper-lemma/README.md @@ -0,0 +1,161 @@ +# Post-wrapper uniqueness for hyperplane-ended helpers + +**One interface lemma, formalized with its actual hypotheses.** No new kappa, no +supplier, no frontier change. This package answers the drawn `formal-interface-lemma` +card ("Can one small, precisely scoped interface lemma be formalized with its actual +hypotheses?") by formalizing the one boundary lemma the hyperplane-end interface +leaves open on the wrapper side, and binding it exactly to the three certified +Lean pairs. + +The hyperplane-end proof `research/hyperplane-end-lean/` formalizes +`factor_iff_pre` ("the pre wrapper must be the `(E, U)` recipe") in +`HyperplaneEnd/Labels.lean`. The integration review +`docs/research/community-hyperplane599-review.md` requires **both** pre and post +wrappers to use the pair `(E, U)` rather than `E` alone, but no post-side +counterpart of `factor_iff_pre` exists in the Lean sources or in any research +package (`hpe-prewrapper-binding` states only the pre-side implication and +explicitly defers its arithmetic). The lemma below is that missing post-side +statement, sharpened to pin the global-phase field. + +## The lemma + +Write `C7 = fourier(7)`, the residual on the seven coordinate qubits tensored +with the identity on the two spectators. As in `PROOF.md`, `(N)` for a pair +`(E, U)` is the exact identity `T_U T_E^{-1} = L (C7 \otimes id) R` between +linear maps, global phase included. + +**Lemma (post-wrapper uniqueness, phase-sharp).** Assume `(N)` holds for the +pair `(E, U)` with invertible monomial wrappers `L, R`. Let `L'` be any +invertible wrapper and `\lambda` a scalar. Then + + L'^{-1} T_U T_E^{-1} R^{-1} = \lambda (C7 \otimes id) + +holds if and only if `L' = \lambda^{-1} L`. In particular the identity with +`\lambda = 1` (hypothesis (F) of `hpe_word_exact`) holds if and only if the +executed post wrapper is exactly the `(E, U)` recipe's `L`; every other post +wrapper, including a FULL recipe `L_{E, FULL}`, breaks `(F)`. For wrappers +restricted to the gate family the only scalars are `\lambda \in \{1, i, -1, -i\}`, +and the wrapper record's phase field is decisive: `L' = i^{t} L` satisfies the +identity with `\lambda = i^{-t}` and with no other `\lambda`. + +**Proof.** Substituting `(N)` turns the left side into `L'^{-1} L (C7 \otimes id)`, +so the identity is `(L'^{-1} L - \lambda I)(C7 \otimes id) = 0`. The residual +`C7` is invertible (a product of `C` gates), hence `C7 \otimes id` is invertible, +so `L'^{-1} L = \lambda I`, that is `L' = \lambda^{-1} L`. Conversely +`L' = \lambda^{-1} L` gives `L'^{-1} L (C7 \otimes id) = \lambda (C7 \otimes id)` +directly. The proof uses `(N)`, invertibility of `L'` and of `C7`, and equality +as linear maps; no phase may be dropped on either side, which is exactly why the +`\lambda` slack is the whole freedom. `\square` + +The symmetric pre-side statement with `\lambda` is proved the same way and +strictly extends `factor_iff_pre` (its `\lambda = 1` case); this package claims +only the post side, which was missing. + +## Hypotheses actually used, and what is not claimed + +Used: exact `(N)` for the pair with these `L, R`; invertibility of the executed +wrapper `L'` (monomial wrappers are); invertibility of `C7`; equality of linear +maps including global phase; `\lambda` a scalar on a 512-dimensional complex +space (`C^{128} \otimes C^{4}`). + +Not claimed: no Lean kernel proof of this lemma (the proof above is written, and +the instance binding is exact Python); nothing about the other conjuncts of +`hrec` (climb identities, tail shape, unit row, footprints, whole invocations); +no statement about pairs outside the three certified ones; no complete +multiplication theorem; no kappa. + +## Exact instance binding (`verify.py`) + +`verify.py` reads the pinned literal circuits of `HyperplaneEnd/Exact.lean` and +evaluates them with an independently written exact gate semantics over `Z[i]` +(the documented five gate kinds of `HyperplaneEnd/Clifford.lean`, `C` gates +without their `1/2`, denominators `2^{#C}` compared exactly; no floating point). +Packed superposition evaluation gives every matrix column at once, and witness +rows/columns are decoded exactly. + +For each of the three certified pairs `(E, U)` (`pair1`-`pair3`): + +1. **Port controls.** Our `adj`, GF(2) inverse and composition conventions + reproduce the kernel-evaluated literals `lhsLit`, `rhsLit`, `wL`, `wR` + (`lits1`-`lits3` in `Exact.lean`), and the permutation matrices are mutual + inverses on all 512 basis states. This cross-checks the semantics port against + the certified arithmetic before any new claim is tested. +2. **Positive fixture.** `L^{-1} T_U T_E^{-1} R^{-1} = C7 \otimes id` exactly, + phase included. +3. **Width guard.** The same identity fails against `C8 \otimes id`. +4. **Mutant family (declared, one field at a time).** `phase+1`, `phase-1`, + `phase+2` satisfy the identity at exactly their `\lambda` form and no other; + `offset-xor-1`, `linear-Z4-flip`, `quadratic-live-bit`, `matrix-row-swap` and + `swapped-L-R` break every `\lambda \in \{1, i, -1, -i\}`, each with an exact + `(row, column)` witness; `quadratic-dead-bit` is a precision control and must + **not** break the identity (see below). +5. **Checker failure control.** `--self-test` corrupts a wrapper literal + self-consistently and requires the pipeline to reject it. + +The `quadratic-dead-bit` control records one real observation: the documented +`qv` semantics reads a diagonal row `Q_i` only through bits above position `i`, +so low-triangle bits are record-dead. Two wrapper records differing only there +denote the **same** operator, and a semantics-level binding accepts them; a +byte-level recipe comparison would reject them. The binding therefore compares +operators, not records. + +Run from the repository root: + +```sh +python3.12 -B research/hpe-post-wrapper-lemma/verify.py +python3.12 -B research/hpe-post-wrapper-lemma/verify.py --self-test +``` + +Expected output ends with `PASS_HPE_POST_WRAPPER_UNIQUENESS pairs=3 +mutants_per_pair=9 controls=3`. `RESULT.json` records the mutant classification +and witnesses. Standard library only, Python 3.10+; the registered replay is +`python3.12 scripts/research_package.py --package research/hpe-post-wrapper-lemma`. + +## Credit + +The interface is [PR 593](https://github.com/CrocSwap/integer-mult-bounds/pull/593) +by Jeremy Kothe (`jeremykothe2`): `factor_iff_pre`, the arbitrary-terminal +extension and the exact non-cold Clifford factorizations. The multi-gate and +cold extensions retained beside it are +[PR 599](https://github.com/CrocSwap/integer-mult-bounds/pull/599) by +DreamingOfClouds. The hyperplane-ended construction is +[PR 591](https://github.com/CrocSwap/integer-mult-bounds/pull/591) and +[PR 596](https://github.com/CrocSwap/integer-mult-bounds/pull/596) by Jeremy +Kothe. The pre/post wrapper requirement is the integration review's +(`docs/research/community-hyperplane599-review.md`, maintainer integration by +Douglas Colkitt with OpenAI Codex assistance). +[PR 2706](https://github.com/CrocSwap/integer-mult-bounds/pull/2706) by Riquelme +Soares (`hevlyo`) in `research/hpe-prewrapper-binding` stated the pre-side +boundary implication and left its arithmetic unrun; +`research/hpe-wrapper-event-binding` compares emitted records to the Lean +literals at event level. The local 511-hyperplane cold check referenced below is +[PR 1697](https://github.com/CrocSwap/integer-mult-bounds/pull/1697) by Aaron +Wang (`navinor`). This package supplies the missing post-side statement, its +phase-sharp form, and the deferred exact arithmetic on the certified instances. +Prepared by Aaron Wang with help from opencode (substantial AI assistance; no +model named; no independent human review claimed). + +## Open next questions + +- **Can the lemma be kernel-checked in Lean?** Why it matters: the written proof + is two lines from `factor_of_exact` and would discharge the post-side conjunct + of `hrec` with the same trust level as `factor_iff_pre`. First step: add + `factor_iff_post` (and the `\lambda` sharpening) to + `research/hyperplane-end-lean/HyperplaneEnd/Labels.lean` mirroring + `factor_iff_pre`, and extend `PrintAxioms` coverage. Blocked by: no Lean + toolchain in this session's environment, and frozen predecessor packages must + not be edited in place; a successor note or additive PR is required. +- **Does the post-side binding hold for cold `(E = 0)` helpers and multi-gate + tails?** Why it matters: the certified pairs are the three non-cold pairs only; + cold ends (`width 8`) and multi-gate tails keep `(N)` and the wrapper hypotheses + as assumptions (`PROOF.md` sections 4 and 7). First step: run + `research/hpe-wrapper-event-binding/verify.py --run` on an emitted cold-end run + and extend its literal comparison with cold recipe pairs, or certify one cold + pair exactly with this package's semantics. Blocked by: no cold `(N)` literal + pairs exist in Lean (only the local 511-hyperplane tool check), and the + emitted HPE runs are not vendored in this repository. +- **Should record-level recipe comparison be relaxed to operator equality?** + Why it matters: dead quadratic bits make byte comparison reject a correct + wrapper record. First step: document the `qv` low-triangle degeneracy in + `scripts/verify_hpe_lean_binding.py` and add a dead-bit mutation control there. + Blocked by: shared-tool changes need maintainer review. diff --git a/research/hpe-post-wrapper-lemma/RESULT.json b/research/hpe-post-wrapper-lemma/RESULT.json new file mode 100644 index 0000000000..70a1987101 --- /dev/null +++ b/research/hpe-post-wrapper-lemma/RESULT.json @@ -0,0 +1,523 @@ +{ + "controls": [ + "pair1: adj/inverse/composition ports reproduce the kernel literals", + "pair2: adj/inverse/composition ports reproduce the kernel literals", + "pair3: adj/inverse/composition ports reproduce the kernel literals" + ], + "lean_source": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "lean_source_sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "pairs": [ + { + "E": [ + 45 + ], + "U": [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + "mutants": [ + { + "k_satisfying": [ + 3 + ], + "lambda1_witness": [ + 0, + 0, + [ + -4096, + -4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase+1" + }, + { + "k_satisfying": [ + 1 + ], + "lambda1_witness": [ + 0, + 0, + [ + 4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase-1" + }, + { + "k_satisfying": [ + 2 + ], + "lambda1_witness": [ + 0, + 0, + [ + -4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase+2" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 0, + 0, + [ + 0, + 0 + ], + [ + 1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "offset-xor-1" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 1, + 0, + [ + 4096, + -4096 + ], + [ + -1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "linear-Z4-flip" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 3, + 0, + [ + 4096, + -4096 + ], + [ + -1024, + 1024 + ] + ], + "mode": "reject", + "mutant": "quadratic-live-bit" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 2, + 0, + [ + 0, + 0 + ], + [ + -1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "matrix-row-swap" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 0, + 0, + [ + 0, + 0 + ], + [ + 1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "swapped-L-R" + }, + { + "k_satisfying": [ + 0 + ], + "lambda1_witness": null, + "mode": "equal", + "mutant": "quadratic-dead-bit" + } + ], + "pair": 1, + "positive": "exact", + "width_guard_C8": "rejected" + }, + { + "E": [ + 51 + ], + "U": [ + 256, + 128, + 64, + 33, + 17, + 8, + 4, + 3 + ], + "mutants": [ + { + "k_satisfying": [ + 3 + ], + "lambda1_witness": [ + 0, + 0, + [ + -4096, + -4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase+1" + }, + { + "k_satisfying": [ + 1 + ], + "lambda1_witness": [ + 0, + 0, + [ + 4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase-1" + }, + { + "k_satisfying": [ + 2 + ], + "lambda1_witness": [ + 0, + 0, + [ + -4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase+2" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 0, + 0, + [ + 0, + 0 + ], + [ + 1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "offset-xor-1" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 1, + 0, + [ + 4096, + -4096 + ], + [ + -1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "linear-Z4-flip" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 3, + 0, + [ + 4096, + -4096 + ], + [ + -1024, + 1024 + ] + ], + "mode": "reject", + "mutant": "quadratic-live-bit" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 1, + 0, + [ + 0, + 0 + ], + [ + -1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "matrix-row-swap" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 0, + 0, + [ + 0, + 0 + ], + [ + 1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "swapped-L-R" + }, + { + "k_satisfying": [ + 0 + ], + "lambda1_witness": null, + "mode": "equal", + "mutant": "quadratic-dead-bit" + } + ], + "pair": 2, + "positive": "exact", + "width_guard_C8": "rejected" + }, + { + "E": [ + 30 + ], + "U": [ + 256, + 128, + 64, + 32, + 18, + 10, + 6, + 1 + ], + "mutants": [ + { + "k_satisfying": [ + 3 + ], + "lambda1_witness": [ + 0, + 0, + [ + -4096, + -4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase+1" + }, + { + "k_satisfying": [ + 1 + ], + "lambda1_witness": [ + 0, + 0, + [ + 4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase-1" + }, + { + "k_satisfying": [ + 2 + ], + "lambda1_witness": [ + 0, + 0, + [ + -4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "phase", + "mutant": "phase+2" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 0, + 0, + [ + 4096, + 4096 + ], + [ + 1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "offset-xor-1" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 1, + 0, + [ + -4096, + 4096 + ], + [ + -1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "linear-Z4-flip" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 3, + 0, + [ + 4096, + -4096 + ], + [ + -1024, + 1024 + ] + ], + "mode": "reject", + "mutant": "quadratic-live-bit" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 1, + 0, + [ + 0, + 0 + ], + [ + -1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "matrix-row-swap" + }, + { + "k_satisfying": [], + "lambda1_witness": [ + 0, + 0, + [ + 0, + 0 + ], + [ + 1024, + -1024 + ] + ], + "mode": "reject", + "mutant": "swapped-L-R" + }, + { + "k_satisfying": [ + 0 + ], + "lambda1_witness": null, + "mode": "equal", + "mutant": "quadratic-dead-bit" + } + ], + "pair": 3, + "positive": "exact", + "width_guard_C8": "rejected" + } + ], + "semantics": "documented five-gate semantics of HyperplaneEnd/Clifford.lean over Z[i]; C gates without their 1/2, denominators 2^#C compared exactly", + "status": "PASS_HPE_POST_WRAPPER_UNIQUENESS" +} diff --git a/research/hpe-post-wrapper-lemma/SOURCES.json b/research/hpe-post-wrapper-lemma/SOURCES.json new file mode 100644 index 0000000000..b851711c37 --- /dev/null +++ b/research/hpe-post-wrapper-lemma/SOURCES.json @@ -0,0 +1,36 @@ +{ + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869", + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "usage": "input" + }, + { + "git_blob": "8315bdda8db4993ef713b24a01ce0e7c1837dff1", + "path": "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean", + "sha256": "febdc3f1734281178b043d714ab70b197d1c34d58ad15462386060b821b80e0c", + "usage": "provenance" + }, + { + "git_blob": "a94a2ac168c088a1282ea411766bc859178620df", + "path": "research/hyperplane-end-lean/PROOF.md", + "sha256": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "usage": "provenance" + }, + { + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "path": "docs/research/agent-task-catalog.json", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "usage": "provenance" + }, + { + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "path": "certificates/selected-result.json", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/hpe-post-wrapper-lemma/TASK.json b/research/hpe-post-wrapper-lemma/TASK.json new file mode 100644 index 0000000000..8ea6a67214 --- /dev/null +++ b/research/hpe-post-wrapper-lemma/TASK.json @@ -0,0 +1,105 @@ +{ + "actual_scope": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "ai_assistance": "Substantial AI assistance (no model named) in the derivation, implementation, exact checks and writing; no independent human review claimed.", + "author": "Aaron Wang, with help from opencode", + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa: hpe_word_exact's wrapper side carried an unformalized post-wrapper obligation; this closes it for the three certified pairs with exact arithmetic and states the universal lemma.", + "budget_minutes": 60, + "draw": { + "cards": [ + "formal-interface-lemma", + "independent-moment" + ], + "chosen": "formal-interface-lemma (first suggestion; construction reading of its drawn method)", + "pair_collision_check": "disc-comments --grep over discussions 1317 and 1166 at 2026-10-16T20:30Z (claims enumerated by headers and timestamps): no live CLAIM on this object. Nearest rows: comment 18917564 (2026-10-14T06:43Z, formal-interface-lemma scope key e3ffea67887eeb4c396c) DONE/released as PR 1697; comment 18921325 (2026-10-14T10:07Z, independent-moment scope key c6f2494b197df3bc3591) closed; comment 18941591 (2026-10-15T05:28Z, independent-moment, scope changed) expired 2026-10-15T07:30Z. All different scope keys and expired or released. Own CLAIM posted 2026-10-16T20:40Z: discussion 1317 comment 18982589.", + "re_draw": null, + "saturation_handling": "Census/coverage readings of the card are saturated: find_overlap OR-mode ('post wrapper' 'wrapper uniqueness' 'factor_iff' 'hyperplane end' 'formal interface' 'interface lemma') returned 201 possible matches at 2026-10-16T20:38Z (complete pagination; 291 open PRs, 1786 discussion records), the first 20 rows all local original_card rows of this heavily drawn card (hpe-prewrapper-binding, hpe-wrapper-event-binding, hpe-lean-semantic-binding, hpe-axiom-inventory-audit, cold-hyperplane-semantic-binding and others). The construction reading named by the drawn method is unpriced: Labels.lean proves only factor_iff_pre; no package states the post-side uniqueness or its lambda-sharp form; hpe-prewrapper-binding states the pre-side implication and explicitly defers the arithmetic. Took that construction reading inside the card; no saturation re-draw needed.", + "seed": "80692bf8777fc3a7d12b201233cd6ae2" + }, + "environment": { + "arithmetic": "exact integer Gaussian arithmetic; no floating point", + "platform": "Windows (win32), native CPython, standard library only", + "python": "3.12.14" + }, + "evidence": "Written post-wrapper uniqueness lemma (phase-sharp) with full hypotheses; exact stdlib instance binding on the three certified Lean pairs pair1-3 of HyperplaneEnd/Exact.lean: positive identity exact for the shipped post wrappers, C8 width guard rejected, per pair 9 mutants classified (3 phase mutants hold at exactly their lambda form i^{-t} and no other; 5 wrong wrappers break all four lambda forms each with an exact (row, column) witness; 1 record-dead quadratic bit is inert and correctly accepted), port controls reproduce the kernel literals lits1-3, --self-test rejects a self-consistent corrupted wrapper literal. Author-checked; no Lean kernel proof of the lemma and no independent human review.", + "freshness": { + "canonical_main": "d8e0f83f00191df62174b641e9fff055c357f641", + "catalog_sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "checked_utc": "2026-10-16T20:38Z", + "priority_revision": 6 + }, + "open_questions": [ + { + "blocked_by": "No Lean toolchain in this session's environment; frozen predecessor packages are not edited in place.", + "first_step": "Add the theorem mirroring factor_iff_pre (rewrite with wrapped_block and (N), invertibility of C7 tensor id) and extend PrintAxioms coverage.", + "question": "Can factor_iff_post and its lambda-sharp form be kernel-checked in HyperplaneEnd/Labels.lean beside factor_iff_pre?", + "why_it_matters": "It would discharge the post-side conjunct of hrec with the same trust level as the pre side." + }, + { + "blocked_by": "No cold (N) literal pairs exist in Lean (only the local 511-hyperplane tool check); emitted HPE runs are not vendored in this repository.", + "first_step": "Bind one cold pair exactly with this package's semantics, or extend research/hpe-wrapper-event-binding to cold recipe pairs on an emitted run.", + "question": "Does the post-side binding hold for cold (E = 0) helpers and multi-gate tails?", + "why_it_matters": "The certified pairs cover three non-cold pairs only; cold ends and multi-gate tails keep (N) and the wrapper hypotheses as assumptions." + }, + { + "blocked_by": "Shared-tool changes need maintainer review.", + "first_step": "Document the degeneracy in scripts/verify_hpe_lean_binding.py and add a dead-bit mutation control there.", + "question": "Should record-level wrapper comparison be relaxed to operator equality on dead quadratic bits?", + "why_it_matters": "The qv semantics reads Q_i only through bits above i, so byte comparison can reject a correct wrapper record." + } + ], + "original_card": { + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "id": "formal-interface-lemma", + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ], + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ] + }, + "outcome": "completed", + "priority_revision": 6, + "schema_version": 1, + "scope_change_reason": "", + "scope_status": "unchanged", + "selection": { + "chooser_scope_key": "636f26dec98e26b296e8", + "drawn_card": "formal-interface-lemma", + "drawn_method": "Formalize a missing boundary lemma identified by the selected review.", + "original_nonce": "80692bf8777fc3a7d12b201233cd6ae2", + "original_track": "independent-verification", + "suggested_cards": [ + "formal-interface-lemma", + "independent-moment" + ] + }, + "stop_rule": "Stop after one formal lemma with exact instance binding and its failure controls; no supplier, kappa or frontier claim, no second lemma, no census.", + "task_id": "formal-interface-lemma" +} diff --git a/research/hpe-post-wrapper-lemma/VERIFY.json b/research/hpe-post-wrapper-lemma/VERIFY.json new file mode 100644 index 0000000000..ab80b9deb5 --- /dev/null +++ b/research/hpe-post-wrapper-lemma/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "checks": "Exact instance binding of the post-wrapper uniqueness lemma on the three certified Lean pairs: port controls against the kernel literals, positive identity fixtures, C8 width guard, and the declared nine-entry wrapper-mutant family with exact (row, column) witnesses.", + "timeout_seconds": 300 + }, + { + "argv": ["{python}", "-B", "{package}/verify.py", "--self-test"], + "checks": "Failure control: a self-consistently corrupted wrapper literal must be rejected by the same pipeline.", + "timeout_seconds": 300 + } + ], + "inputs": ["research/hyperplane-end-lean/HyperplaneEnd/Exact.lean"] +} diff --git a/research/hpe-post-wrapper-lemma/make_meta.py b/research/hpe-post-wrapper-lemma/make_meta.py new file mode 100644 index 0000000000..001b56e0af --- /dev/null +++ b/research/hpe-post-wrapper-lemma/make_meta.py @@ -0,0 +1,127 @@ +"""Write TASK.json (draw_card extraction + session record) and SOURCES.json (exact pins). + +The original_card is extracted programmatically from the pinned task catalogue +(docs/research/agent-task-catalog.json) so it is byte-equal to the catalogue card +object; the chooser's flattened "method" shape is never hand-copied. + +usage: python -B research/hpe-post-wrapper-lemma/make_meta.py (Python 3.12)""" +import hashlib +import json +import subprocess +import sys +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +BASE = "d8e0f83f00191df62174b641e9fff055c357f641" +CATALOG = "docs/research/agent-task-catalog.json" +TASK_ID = "formal-interface-lemma" + + +def git_bytes(expr): + return subprocess.run(["git", "show", expr], cwd=ROOT, capture_output=True, + check=True).stdout + + +def git_blob(expr): + out = subprocess.run(["git", "rev-parse", expr], cwd=ROOT, capture_output=True, + check=True, text=True).stdout.strip() + return out + + +def draw_card(task_id): + """The full catalogue card object for task_id, verbatim.""" + catalog = json.loads(git_bytes(BASE + ":" + CATALOG)) + cards = [t for track in catalog["tracks"] for t in track["tasks"] if t["id"] == task_id] + assert len(cards) == 1, "draw_card: expected exactly one card for " + task_id + return cards[0] + + +def pin(path): + data = git_bytes(BASE + ":" + path) + return {"path": path, "git_blob": git_blob(BASE + ":" + path), + "sha256": hashlib.sha256(data).hexdigest()} + + +def main(): + card = draw_card(TASK_ID) + sources = { + "schema_version": 1, + "base_commit": BASE, + "files": [ + dict(pin("research/hyperplane-end-lean/HyperplaneEnd/Exact.lean"), usage="input"), + dict(pin("research/hyperplane-end-lean/HyperplaneEnd/Labels.lean"), usage="provenance"), + dict(pin("research/hyperplane-end-lean/PROOF.md"), usage="provenance"), + dict(pin(CATALOG), usage="provenance"), + dict(pin("certificates/selected-result.json"), usage="provenance"), + ], + } + task = { + "schema_version": 1, + "task_id": TASK_ID, + "priority_revision": 6, + "base_commit": BASE, + "original_card": card, + "scope_status": "unchanged", + "actual_scope": card["question"], + "scope_change_reason": "", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa: hpe_word_exact's wrapper side carried an unformalized post-wrapper obligation; this closes it for the three certified pairs with exact arithmetic and states the universal lemma.", + "budget_minutes": 60, + "stop_rule": "Stop after one formal lemma with exact instance binding and its failure controls; no supplier, kappa or frontier claim, no second lemma, no census.", + "outcome": "completed", + "evidence": ("Written post-wrapper uniqueness lemma (phase-sharp) with full hypotheses; exact stdlib instance binding on the three certified Lean pairs pair1-3 of HyperplaneEnd/Exact.lean: positive identity exact for the shipped post wrappers, C8 width guard rejected, per pair 9 mutants classified (3 phase mutants hold at exactly their lambda form i^{-t} and no other; 5 wrong wrappers break all four lambda forms each with an exact (row, column) witness; 1 record-dead quadratic bit is inert and correctly accepted), port controls reproduce the kernel literals lits1-3, --self-test rejects a self-consistent corrupted wrapper literal. Author-checked; no Lean kernel proof of the lemma and no independent human review."), + "author": "Aaron Wang, with help from opencode", + "ai_assistance": "Substantial AI assistance (no model named) in the derivation, implementation, exact checks and writing; no independent human review claimed.", + "open_questions": [ + {"question": "Can factor_iff_post and its lambda-sharp form be kernel-checked in HyperplaneEnd/Labels.lean beside factor_iff_pre?", + "why_it_matters": "It would discharge the post-side conjunct of hrec with the same trust level as the pre side.", + "first_step": "Add the theorem mirroring factor_iff_pre (rewrite with wrapped_block and (N), invertibility of C7 tensor id) and extend PrintAxioms coverage.", + "blocked_by": "No Lean toolchain in this session's environment; frozen predecessor packages are not edited in place."}, + {"question": "Does the post-side binding hold for cold (E = 0) helpers and multi-gate tails?", + "why_it_matters": "The certified pairs cover three non-cold pairs only; cold ends and multi-gate tails keep (N) and the wrapper hypotheses as assumptions.", + "first_step": "Bind one cold pair exactly with this package's semantics, or extend research/hpe-wrapper-event-binding to cold recipe pairs on an emitted run.", + "blocked_by": "No cold (N) literal pairs exist in Lean (only the local 511-hyperplane tool check); emitted HPE runs are not vendored in this repository."}, + {"question": "Should record-level wrapper comparison be relaxed to operator equality on dead quadratic bits?", + "why_it_matters": "The qv semantics reads Q_i only through bits above i, so byte comparison can reject a correct wrapper record.", + "first_step": "Document the degeneracy in scripts/verify_hpe_lean_binding.py and add a dead-bit mutation control there.", + "blocked_by": "Shared-tool changes need maintainer review."}, + ], + "selection": { + "original_nonce": "80692bf8777fc3a7d12b201233cd6ae2", + "original_track": "independent-verification", + "suggested_cards": ["formal-interface-lemma", "independent-moment"], + "drawn_card": TASK_ID, + "drawn_method": "Formalize a missing boundary lemma identified by the selected review.", + "chooser_scope_key": "636f26dec98e26b296e8", + }, + "draw": { + "seed": "80692bf8777fc3a7d12b201233cd6ae2", + "cards": ["formal-interface-lemma", "independent-moment"], + "chosen": "formal-interface-lemma (first suggestion; construction reading of its drawn method)", + "re_draw": None, + "saturation_handling": ("Census/coverage readings of the card are saturated: find_overlap OR-mode ('post wrapper' 'wrapper uniqueness' 'factor_iff' 'hyperplane end' 'formal interface' 'interface lemma') returned 201 possible matches at 2026-10-16T20:38Z (complete pagination; 291 open PRs, 1786 discussion records), the first 20 rows all local original_card rows of this heavily drawn card (hpe-prewrapper-binding, hpe-wrapper-event-binding, hpe-lean-semantic-binding, hpe-axiom-inventory-audit, cold-hyperplane-semantic-binding and others). The construction reading named by the drawn method is unpriced: Labels.lean proves only factor_iff_pre; no package states the post-side uniqueness or its lambda-sharp form; hpe-prewrapper-binding states the pre-side implication and explicitly defers the arithmetic. Took that construction reading inside the card; no saturation re-draw needed."), + "pair_collision_check": ("disc-comments --grep over discussions 1317 and 1166 at 2026-10-16T20:30Z (claims enumerated by headers and timestamps): no live CLAIM on this object. Nearest rows: comment 18917564 (2026-10-14T06:43Z, formal-interface-lemma scope key e3ffea67887eeb4c396c) DONE/released as PR 1697; comment 18921325 (2026-10-14T10:07Z, independent-moment scope key c6f2494b197df3bc3591) closed; comment 18941591 (2026-10-15T05:28Z, independent-moment, scope changed) expired 2026-10-15T07:30Z. All different scope keys and expired or released. Own CLAIM posted 2026-10-16T20:40Z: discussion 1317 comment 18982589."), + }, + "freshness": { + "canonical_main": BASE, + "priority_revision": 6, + "catalog_sha256": hashlib.sha256(git_bytes(BASE + ":" + CATALOG)).hexdigest(), + "checked_utc": "2026-10-16T20:38Z", + }, + "environment": { + "python": sys.version.split()[0], + "platform": "Windows (win32), native CPython, standard library only", + "arithmetic": "exact integer Gaussian arithmetic; no floating point", + }, + } + (PKG / "TASK.json").write_text(json.dumps(task, indent=1, sort_keys=True, ensure_ascii=False) + "\n", + encoding="utf-8", newline="\n") + (PKG / "SOURCES.json").write_text(json.dumps(sources, indent=1, sort_keys=True) + "\n", + encoding="utf-8", newline="\n") + card_bytes = json.dumps(card, sort_keys=True, separators=(",", ":")) + print("TASK.json and SOURCES.json written; original_card is the catalogue object", + hashlib.sha256(card_bytes.encode()).hexdigest()[:16], "files:", len(sources["files"])) + + +if __name__ == "__main__": + main() diff --git a/research/hpe-post-wrapper-lemma/verify.py b/research/hpe-post-wrapper-lemma/verify.py new file mode 100644 index 0000000000..0c389aafdc --- /dev/null +++ b/research/hpe-post-wrapper-lemma/verify.py @@ -0,0 +1,400 @@ +#!/usr/bin/env python3 +"""Exact instance binding for the post-wrapper uniqueness lemma (HPE interface). + +Reads the literal circuits of the pinned input +research/hyperplane-end-lean/HyperplaneEnd/Exact.lean and, with an independently +written exact gate semantics over Z[i] (integer semantics, the 1/2 of each C gate +carried as an explicit denominator 2^#C), checks on the three certified (E, U) pairs +of HyperplaneEnd.Exact: + + ports : adj/inv/composition conventions reproduce the kernel literals + (lhsLit = adjC(fE) ++ fU, rhsLit = wR ++ fourierC 7 ++ wL, + Mono.gates(pair.L/R) = wL/wR with our own GF(2) inverse); + positive : L^-1 T_U T_E^-1 R^-1 = C7 (x) id exactly, phase included; + width guard : the identity fails against C8 (x) id (wrong residual width); + lemma : for every declared one-field post-wrapper mutant L' and every + k in 0..3, L'^-1 T_U T_E^-1 R^-1 = i^k (C7 (x) id) holds only + when L' = i^t L with k = -t mod 4 (phase sharpness), and never + for a non-phase mutant; + failure ctl : a corrupted wrapper literal must be rejected (mutant suite). + +usage: python3 -B research/hpe-post-wrapper-lemma/verify.py [--write-result PATH] +Python 3.10+, standard library only. Apache-2.0. +""" +import ast +import hashlib +import json +import re +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +LEAN = ROOT / "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" +N = 512 # 2^9 basis states + +BRACKETS = {0x27E8: "[", 0x27E9: "]", 0x2329: "[", 0x232A: "]", 0x00AB: "[", + 0x00BB: "]", 0x2039: "[", 0x203A: "]", 0xFF08: "(", 0xFF09: ")"} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def translated(text): + return "".join(BRACKETS.get(ord(ch), ch) for ch in text) + + +def bracket_block(text, start): + """Return the [...] block starting at the first '[' at or after start.""" + i = text.index("[", start) + depth = 0 + for j in range(i, len(text)): + if text[j] == "[": + depth += 1 + elif text[j] == "]": + depth -= 1 + if depth == 0: + return text[i:j + 1] + raise ValueError("unterminated bracket block") + + +def parse_gate_block(block): + """Parse `.dg Q Iv | .pm G Gi | .cg q s | .xg b | .ph p` into tuples.""" + gates = [] + for m in re.finditer(r"\.(dg|pm|cg|xg|ph)\b", block): + kind = m.group(1) + pos = m.end() + args = [] + if kind in ("dg", "pm"): + for _ in range(2): + start = block.index("[", pos) + arg = bracket_block(block, pos) + args.append(ast.literal_eval(arg)) + pos = start + len(arg) + elif kind == "cg": + m2 = re.match(r"\s*(\d+)\s+(true|false)", block[pos:]) + need(m2 is not None, "bad cg gate") + args = [int(m2.group(1)), m2.group(2) == "true"] + elif kind == "xg": + m2 = re.match(r"\s*(\d+)", block[pos:]) + need(m2 is not None, "bad xg gate") + args = [int(m2.group(1))] + else: + m2 = re.match(r"\s*(\d+)", block[pos:]) + need(m2 is not None, "bad ph gate") + args = [int(m2.group(1))] + gates.append(tuple([kind] + args)) + return gates + + +def parse_defs(text): + """Extract the literal gate lists and pair monomials from Exact.lean.""" + text = translated(text) + out = {} + for name in ("fE1", "fU1", "fE2", "fU2", "fE3", "fU3", + "wL1", "wR1", "wL2", "wR2", "wL3", "wR3", + "lhsLit1", "rhsLit1", "lhsLit2", "rhsLit2", "lhsLit3", "rhsLit3"): + m = re.search(r"def " + name + r" : List Gate :=", text) + need(m is not None, "missing literal " + name) + out[name] = parse_gate_block(bracket_block(text, m.end())) + for n in (1, 2, 3): + m = re.search(r"def pair" + str(n) + r" : Pair :=", text) + need(m is not None, "missing literal pair%d" % n) + data = ast.literal_eval(bracket_block(text, m.end())) + need(len(data) == 4, "pair%d shape" % n) + out["pair%d" % n] = data # [E, U, [Q,Iv,G,b,p], [Q,Iv,G,b,p]] + return out + + +# ---- exact bit arithmetic (ports of the documented semantics) ---- + +def mv(rows, x): + y = 0 + for i, r in enumerate(rows): + if bin(r & x).count("1") & 1: + y |= 1 << i + return y + + +def qv(q_rows, alpha, x): + s = 0 + for i in range(len(q_rows)): + if (x >> i) & 1: + s += alpha[i] + 2 * (bin((q_rows[i] >> (i + 1)) & (x >> (i + 1))).count("1") & 1) + return s % 4 + + +def inv_rows(rows, n): + """GF(2) inverse of the matrix with the given rows (unique).""" + aug = [[rows[i] if i < len(rows) else 0, 1 << i] for i in range(n)] + for col in range(n): + piv = None + for i in range(col, n): + if (aug[i][0] >> col) & 1: + piv = i + break + need(piv is not None, "singular matrix") + aug[col], aug[piv] = aug[piv], aug[col] + for i in range(n): + if i != col and (aug[i][0] >> col) & 1: + aug[i][0] ^= aug[col][0] + aug[i][1] ^= aug[col][1] + return [aug[i][1] for i in range(n)] + + +def mono_gates(mono): + q_rows, alpha, g, b, p = mono + return [("dg", q_rows, alpha), ("pm", g, inv_rows(g, 9)), ("xg", b), ("ph", p)] + + +def adj(g): + kind = g[0] + if kind == "pm": + return ("pm", g[2], g[1]) + if kind == "dg": + return ("dg", g[1], [(4 - a % 4) % 4 for a in g[2]]) + if kind == "cg": + return ("cg", g[1], not g[2]) + if kind == "xg": + return g + return ("ph", (4 - g[1] % 4) % 4) + + +def adj_c(circ): + return [adj(g) for g in reversed(circ)] + + +def fourier_c(r): + return [("cg", 1 << i, True) for i in range(r)] + + +# ---- integer semantics over Z[i] (C gates without their 1/2) ---- + +def ipow(k, a, b): + k %= 4 + if k == 0: + return a, b + if k == 1: + return -b, a + if k == 2: + return -a, -b + return b, -a + + +def apply_circuit(circ, re, im): + for g in circ: + kind = g[0] + if kind == "pm": + nre, nim = [0] * N, [0] * N + for y in range(N): + s = mv(g[2], y) + nre[y], nim[y] = re[s], im[s] + re, im = nre, nim + elif kind == "dg": + for x in range(N): + re[x], im[x] = ipow(qv(g[1], g[2], x), re[x], im[x]) + elif kind == "cg": + q, s = g[1], g[2] + nre, nim = [0] * N, [0] * N + for x in range(N): + a, b = re[x], im[x] + c, d = re[x ^ q], im[x ^ q] + if s: + nre[x] = (a - b) + (c + d) + nim[x] = (a + b) + (-c + d) + else: + nre[x] = (a + b) + (c - d) + nim[x] = (-a + b) + (c + d) + re, im = nre, nim + elif kind == "xg": + bit = g[1] + nre, nim = [0] * N, [0] * N + for x in range(N): + nre[x], nim[x] = re[x ^ bit], im[x ^ bit] + re, im = nre, nim + else: + for x in range(N): + re[x], im[x] = ipow(g[1], re[x], im[x]) + return re, im + + +def packed(circ, base): + re = [0] * N + im = [0] * N + power = 1 + for x in range(N): + re[x] = power + power *= base + return apply_circuit(circ, re, im) + + +def ncg(circ): + return sum(1 for g in circ if g[0] == "cg") + + +def signed_digits(value, base, count): + digits = [] + for _ in range(count): + t = value % base + if t > base // 2: + t -= base + digits.append(t) + value = (value - t) // base + need(value == 0, "packed value exceeds digit budget") + return digits + + +def map_equal(circ_a, circ_b): + """Exact equality of the two circuits as C-linear maps (1/2 per C gate). + + Returns None when equal, else a witness (row, column, entry_a, entry_b). + """ + ca, cb = ncg(circ_a), ncg(circ_b) + da, db = 1 << ca, 1 << cb + expo = max(cb + 2 * ca, ca + 2 * cb) + base = 1 << (expo + 3) # signed digits |d| <= 2^expo < base/2 + re_a, im_a = packed(circ_a, base) + re_b, im_b = packed(circ_b, base) + for x in range(N): + if re_a[x] * db != re_b[x] * da or im_a[x] * db != im_b[x] * da: + dre_a = signed_digits(re_a[x] * db, base, N) + dim_a = signed_digits(im_a[x] * db, base, N) + dre_b = signed_digits(re_b[x] * db, base, N) + dim_b = signed_digits(im_b[x] * db, base, N) + for y in range(N): + if (dre_a[y], dim_a[y]) != (dre_b[y], dim_b[y]): + return (x, y, [dre_a[y], dim_a[y]], [dre_b[y], dim_b[y]]) + need(False, "row differs but no column witness decodes") + return None + + +def phase_mul(circ, k): + """circ followed by a global phase i^k (kept as an extra gate).""" + return list(circ) + [("ph", k % 4)] + + +def post_id(pair, post_mono): + """Circuit of L'^-1 T_U T_E^-1 R'^-1 for the pair's literals.""" + _, _, left, right = pair + return (adj_c(mono_gates(right)) + adj_c(pair_fE) + pair_fU + + adj_c(mono_gates(post_mono))) + + +def main(): + args = sys.argv[1:] + write = None + if "--write-result" in args: + write = Path(args[args.index("--write-result") + 1]) + text = LEAN.read_text(encoding="utf-8") + d = parse_defs(text) + if "--self-test" in args: + # failure control: a corrupted wrapper literal must fail the pipeline + bad = list(d["wL1"]) + bad[3] = ("ph", (bad[3][1] + 1) % 4) + d["wL1"] = bad + d["pair1"][2][4] = (d["pair1"][2][4] + 1) % 4 + try: + run(d) + except ValueError as exc: + print("PASS_SELF_TEST corrupted literal rejected: " + str(exc)) + return + need(False, "self-test: corrupted wrapper literal was accepted") + run(d, write) + + +def run(d, write=None): + controls = [] + result_pairs = [] + global pair_fE, pair_fU + + for n in (1, 2, 3): + pair = d["pair%d" % n] + e_rows, u_rows, left, right = pair + fE, fU = d["fE%d" % n], d["fU%d" % n] + wL, wR = d["wL%d" % n], d["wR%d" % n] + pair_fE, pair_fU = fE, fU + + # port controls: the kernel literals must match our conventions + need(adj_c(fE) + fU == d["lhsLit%d" % n], "pair%d: adj convention differs from lhsLit" % n) + need(wR + fourier_c(7) + wL == d["rhsLit%d" % n], "pair%d: composition differs from rhsLit" % n) + need(mono_gates(left) == wL, "pair%d: our GF(2) inverse/Mono port differs from wL" % n) + need(mono_gates(right) == wR, "pair%d: our GF(2) inverse/Mono port differs from wR" % n) + for rows, gi in ((wL[1][1], wL[1][2]), (wR[1][1], wR[1][2])): + for x in range(N): + need(mv(rows, mv(gi, x)) == x and mv(gi, mv(rows, x)) == x, + "pair%d: pm matrices are not mutual inverses" % n) + controls.append("pair%d: adj/inverse/composition ports reproduce the kernel literals" % n) + + # positive fixture: the shipped post wrapper satisfies the identity exactly + lhs = post_id(pair, left) + c7 = fourier_c(7) + witness = map_equal(lhs, c7) + need(witness is None, "pair%d: shipped post wrapper fails the identity" % n) + # width guard: C8 must not satisfy the identity + need(map_equal(lhs, fourier_c(8)) is not None, + "pair%d: identity wrongly holds against C8" % n) + + # smallest falsifying instance first, then the declared mutant family. + # mode: "phase" = i^t L (lambda sharpness), "reject" = must break every + # lambda form, "equal" = record-only change that must NOT change the map + # (qv reads Q_i only through bits above i, so bit 0 of Q_0 is dead data). + q_rows, alpha, g, b, p = left + mutants = [ + ("phase+1", [q_rows, alpha, g, b, p + 1], "phase", 3), + ("phase-1", [q_rows, alpha, g, b, p - 1], "phase", 1), + ("phase+2", [q_rows, alpha, g, b, p + 2], "phase", 2), + ("offset-xor-1", [q_rows, alpha, g, b ^ 1, p], "reject", None), + ("linear-Z4-flip", [q_rows, [alpha[0] ^ 1] + alpha[1:], g, b, p], "reject", None), + ("quadratic-live-bit", [[q_rows[0] ^ 2] + q_rows[1:], alpha, g, b, p], "reject", None), + ("matrix-row-swap", [q_rows, alpha, [g[1], g[0]] + g[2:], b, p], "reject", None), + ("swapped-L-R", right, "reject", None), + ("quadratic-dead-bit", [[q_rows[0] ^ 1] + q_rows[1:], alpha, g, b, p], "equal", 0), + ] + mutant_rows = [] + for name, mono, mode, sharp_k in mutants: + ks_ok = [k for k in range(4) + if map_equal(post_id(pair, mono), phase_mul(c7, k)) is None] + if mode == "phase": + need(ks_ok == [sharp_k], + "pair%d: phase mutant %s must hold only at k=%d, got %s" % (n, name, sharp_k, ks_ok)) + elif mode == "equal": + need(ks_ok == [0], + "pair%d: inert mutant %s must keep the identity at k=0 only, got %s" % (n, name, ks_ok)) + else: + need(ks_ok == [], + "pair%d: mutant %s must break every lambda form, got %s" % (n, name, ks_ok)) + w = map_equal(post_id(pair, mono), c7) + if mode == "equal": + need(w is None, "pair%d: mutant %s unexpectedly breaks lambda=1" % (n, name)) + else: + need(w is not None, "pair%d: mutant %s not rejected at lambda=1" % (n, name)) + mutant_rows.append({"mutant": name, "mode": mode, + "lambda1_witness": w, "k_satisfying": ks_ok}) + result_pairs.append({"pair": n, "E": e_rows, "U": u_rows, + "positive": "exact", "width_guard_C8": "rejected", + "mutants": mutant_rows}) + print("pair%d: positive exact; C8 rejected; %d mutants classified with witnesses" + % (n, len(mutant_rows))) + sys.stdout.flush() + + status = "PASS_HPE_POST_WRAPPER_UNIQUENESS" + print(status + " pairs=3 mutants_per_pair=9 controls=" + str(len(controls))) + for line in controls: + print(" control: " + line) + if write is not None: + payload = { + "status": status, + "lean_source": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "lean_source_sha256": hashlib.sha256(LEAN.read_bytes()).hexdigest(), + "semantics": "documented five-gate semantics of HyperplaneEnd/Clifford.lean over Z[i]; C gates without their 1/2, denominators 2^#C compared exactly", + "controls": controls, + "pairs": result_pairs, + } + write.write_text(json.dumps(payload, indent=1, sort_keys=True) + "\n", + encoding="utf-8", newline="\n") + print("wrote " + str(write)) + + +if __name__ == "__main__": + main()