diff --git a/research/hpe-lean-semantic-binding/README.md b/research/hpe-lean-semantic-binding/README.md
new file mode 100644
index 0000000000..12d4b76d04
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/README.md
@@ -0,0 +1,232 @@
+# Independent semantic binding of the three Lean HPE pairs
+
+**Independent finite audit; all comparisons pass. No new kappa or Lean theorem.**
+
+The twelve frame and wrapper circuits in the retained
+[`HyperplaneEnd/Exact.lean`](../hyperplane-end-lean/HyperplaneEnd/Exact.lean)
+agree exactly with independent Gaussian-dyadic kernels and the retained Python
+constructors. Both orientations pass on every one of the 512 basis inputs.
+The three factorizations
+
+\[
+T_U T_E^{-1}=L(C_{[7]}\otimes I_4)R
+\]
+
+also pass, with global phase and both spectator coordinates retained.
+These identities are already proved for the Lean definitions by Jeremy Kothe's
+PR #593. This package adds a separately implemented, reproducible check of the
+finite correspondence to the Python semantics; it does not claim priority for
+the identities, or replace the existing formal proofs.
+
+The claim is in [Discussion #1394](https://github.com/CrocSwap/integer-mult-bounds/discussions/1394).
+The refined `formal-interface-lemma` card, exact heads, method and limitations
+are in [TASK.json](TASK.json); input hashes and Git blobs are in
+[SOURCES.json](SOURCES.json). Base: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`.
+
+## Exact coverage
+
+| Object | Domain | Checks |
+|---|---|---|
+| `fE1..3`, `fU1..3`, `wL1..3`, `wR1..3` | Twelve literal circuits | Exact circuit-list equality with the retained Python constructors |
+| Same twelve operators and their inverses | 24 matrices, 512 columns each | Literal evaluator and source executor each equal an independent kernel |
+| `lhsLit1..3`, `rhsLit1..3` | Six matrices, 512 columns each | Literal execution equals the composed independent kernels |
+| Three residual factorizations | 512 columns each | Direct exact kernel equality, independent of the receipt hashes |
+| Nine semantic faults per pair | 27 mutations | An explicit differing input/output coefficient for every fault |
+
+The 24 primitive comparisons cover **12,288 columns and 6,291,456 matrix
+entries**, including zeros. Each residual matrix has 65,536 nonzero entries
+and a reduced common denominator of 16. Each terminal frame has 131,072
+nonzero entries, also with denominator 16; each entrance frame has 1,024
+nonzero entries and denominator 2. Each wrapper is a monomial matrix.
+
+[RESULT.json](RESULT.json) records the complete coverage, matrix fingerprints,
+literal fingerprints, source digests and counterexample coefficients. Hashes
+compact the evidence; acceptance compares exact integer pairs and denominators.
+Sparse representations include every nonzero entry, and equality therefore
+checks the implicit zeros as well. Complex linearity extends basis equality to
+every complex input vector.
+
+## Independent kernel derivation
+
+This is a derivation for the six fixed rank-one/rank-eight frames, using the
+source's stated conventions. It does not assert an all-frame port theorem.
+
+Let `U=(u_0,...,u_(r-1))` be one of these frame bases in `F2^9`. Extend it by
+trying the coordinate unit vectors in ascending order, retaining a vector
+exactly when it increases the span. Let `g` send coordinate bits to the XOR of
+the retained columns, and `h=g^{-1}`. The independent implementation builds the
+complete 512-element bijection by span enumeration; it does not call or port
+the source's Gaussian-elimination inverse routine.
+
+For the physical coordinate unit `e_i`, put `c_i=h(e_i)` and define
+
+\[
+Q_{ij}=\delta_{ij}+c_i\cdot c_j\pmod2,\qquad
+\alpha_i=Q_{ii}\in\{0,1\},
+\]
+\[
+q(x)=\sum_i\alpha_i x_i+2\sum_{i<j}Q_{ij}x_ix_j\pmod4.
+\]
+
+The source applies `K` as the permutation `g` followed by this diagonal phase:
+`K e_z = i^{q(g(z))} e_{g(z)}`. Its frame circuit executes `K^{-1}`, then the
+first `r` coordinate C gates, then `K`. Thus, for `delta < 2^r`, the only possible
+output is `y=g(h(x) XOR delta)`, with coefficient
+
+\[
+(T_U)_{y,x}=2^{-r}i^{q(y)-q(x)}
+  (1+i)^{r-|\delta|}(1-i)^{|\delta|}.
+\]
+
+All other coefficients are zero. The inverse conjugates the Fourier factors,
+while retaining the displayed phase difference. This follows directly by
+inverting `K F_r K^{-1}`. The kernel evaluates these powers in `Z[i]`.
+
+For a serialized monomial `(Q,alpha,G,b,p)`, the separate formula is
+
+\[
+M e_x=i^{p+\sum_i\alpha_i x_i+2\sum_{i<j}Q_{ij}x_ix_j}
+       e_{Gx\mathbin{\mathrm{XOR}}b}.
+\]
+
+Its inverse uses the enumerated inverse permutation and conjugate phase.
+The independent kernel computes `Gx` by XORing columns and the phase by
+explicit coordinate pairs. The literal evaluator instead uses row-mask
+pullbacks and applies the parsed gates in order. The residual formula is
+obtained by ordinary exact matrix composition. `C_[7]` only XORs bits 0..6;
+the source's tensor map is `x -> (x mod 128, floor(x/128))`, so bits 7 and 8 are
+the two spectators.
+
+## Source and independence boundary
+
+The audit uses three views:
+
+1. **Closed-form kernels:** span enumeration and the formulas above. These
+   import no producer, source state-vector executor, tableau or packed check.
+2. **Literal execution:** a strict parser reads the twelve primitive and six
+   composite gate lists from `Exact.lean`. A separate evaluator implements the
+   `Clifford.lean` gate conventions, including pullback permutations. All
+   permutation/inverse pairs are checked on the full 512-element domain.
+3. **Source under test:** the byte-pinned `clifford_exact.py` constructs the
+   frame circuits. Only the pure `monomial_op` function is extracted from the
+   pinned HPE adapter module; its environment-dependent driver is not run.
+   Constructor outputs must match the literal lists, and the source executor
+   is compared against the kernel on all primitive columns, in both directions.
+
+The source executor is an additional subject of comparison, not the oracle.
+The kernels and literal evaluator share basic Gaussian-integer arithmetic and
+exact comparison utilities. They are separate algorithms, not separate human
+implementations or proof-assistant developments.
+
+The existing [`verify_hpe_lean_binding.py`](../../scripts/verify_hpe_lean_binding.py)
+compares emitted recipe records with `pair1..3`. Its historical
+[`lean-bindings.json`](../community-hyperplane599-audit/lean-bindings.json)
+receipt is pinned as context; this audit does **not** regenerate those emitted
+38-helper words or revalidate that receipt's underlying runs. The new check
+starts at the three fixed pair records and validates their operator semantics.
+
+## Controls and interpretation
+
+For each pair, the verifier rejects a global phase change, translation change,
+reversed permutation direction, input character, C-sign change, replacement of
+an active C axis by spectator bit 7, swapped wrappers, reversed circuit order,
+and omission of the entrance inverse. Every rejection stores an exact witness.
+
+The input-character control illustrates the need to retain all input columns:
+adding 2 to the first right-wrapper linear phase preserves the zero-input
+column and negates precisely the 256 odd-indexed columns. For pair 1,
+input 1/output 4 changes from `(1-i)/16` to `(-1+i)/16`.
+This is a boundary of a zero-column-only comparison, **not a reported defect**
+in the source compiler, whose separate tableau check is outside this audit.
+PR #702 and PR #712 already discuss analogous phase controls for different,
+rank-four cold wrappers; their priority is retained.
+
+The focused tests additionally check `C(q)^2=X(q)` and `C(q)^*C(q)=I` on five
+specified masks and all 512 inputs; a corrupted frame literal; malformed or
+duplicated declarations; an incorrect permutation inverse; changed source
+bytes; receipt digest/type/duplicate-key corruption; output overwrite refusal;
+and an isolated optimized replay from a copy whose input/package files are
+read-only. Normal verification never rewrites the receipt.
+
+## Reproduce
+
+Standard-library Python 3.12; no Lean, GPU, network or third-party packages.
+Run from the repository root:
+
+```sh
+python3 -I -B research/hpe-lean-semantic-binding/verify.py
+python3 -I -B -m unittest discover -s research/hpe-lean-semantic-binding -p test_verify.py
+python3 -B scripts/research_package.py --package research/hpe-lean-semantic-binding --check-only
+python3 -B scripts/research_package.py --package research/hpe-lean-semantic-binding
+```
+
+The last command runs the verifier and the seven focused tests. Expected direct
+output:
+
+```text
+PASS_HPE_LEAN_SEMANTIC_BINDING pairs=3 operators=24 operator_columns=12288 factorizations=3 controls=27 no_new_lean_build no_new_kappa
+```
+
+A direct replay takes about 30 seconds in the measured CPython 3.12.3
+environment; timing is informational. The standalone audit also works in a
+source export containing the declared inputs. The generic package metadata
+check needs Git history to check provenance.
+
+To create a separate receipt, use `--write-receipt NEW_FILE`; an existing file
+is refused. Canonical receipt comparison preserves JSON types and rejects
+duplicate keys. `--receipt FILE` checks a different expected receipt without
+modifying it.
+
+## Limitations
+
+No Lean installation, kernel build or fresh axiom audit was performed. The
+theorems and their proof-assistant trust base remain those of the retained
+package. This finite result covers only the three fixed pair records and
+their listed literals, not arbitrary frames, all selected helpers or future
+source revisions. Hash pins deliberately reject source drift.
+
+Scalar-word restoration, helper rows/columns, wrapper placement, tail
+chronology, physical hosting/footprints, compiler uniformity, precision/tape,
+complete recursive costs and analytic transfer are not checked here.
+The selected construction, selected record and predecessor packages are
+unchanged. No new physical supplier or improved exponent is claimed.
+
+## Open next questions
+
+- **Can the source-to-formal gate semantics be proved for a shared serialized
+  circuit grammar?** This would reduce the manual semantic-translation trust
+  boundary. A feasible first step is a small formal interpreter for the five
+  gate tags and an explicit correspondence theorem for permutation and C
+  gates. The blocker is a formally specified Python execution semantics or a
+  separately verified shared compiler, not more finite examples.
+- **Can one current emitted helper be bound end-to-end to this finite audit?**
+  That would join the operator check to an actual invocation. Start with a
+  pinned emitted word containing one of the three certified pairs, trace both
+  wrapper records and their actual event positions, and verify the unit row
+  and remaining label/hosting hypotheses. A raw pair match alone does not
+  discharge those obligations. This package supplies no such new admission.
+
+The same questions and blockers are structured in [TASK.json](TASK.json).
+
+## Credit and license
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+Jeremy Kothe / `jeremykothe2` supplied PR #593's exact Clifford formalization,
+the three pair records and their formal factorization proofs.
+DreamingOfClouds supplied the Lemma A/G line, HPE wrapper definitions and
+PR #599's multi-gate/cold extension. The Clifford engine is retained from
+icekylinx's `split-centres-global` lineage. Chafik Boukhalfa / `chafreaky`,
+Zhihao Chen / `jacklightChen`, and the realization/hosting contributors named
+in the retained [NOTICE](../hyperplane-end-lean/NOTICE.md) retain their credit.
+
+Nearby independent audits are BigCactusLabs' PR #702 (all fourteen historical
+rank-four cold wrappers), Joshua Snider / `jsnider3`'s PR #712 (a symbolic
+quadratic certificate for one such wrapper), and Gareth Davidson / `bitplane`'s
+PR #1255 (selected physical chart phases). None is an implementation dependency.
+The operator-domain and semantic-port focus here differ from those audits.
+
+New code and prose are Apache-2.0 under the repository [LICENSE](../../LICENSE).
+No source package is copied or modified. Substantial AI assistance covered
+research, derivation, implementation, checking and writing; no independent
+human review is claimed.
diff --git a/research/hpe-lean-semantic-binding/RESULT.json b/research/hpe-lean-semantic-binding/RESULT.json
new file mode 100644
index 0000000000..c9169b5d5d
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/RESULT.json
@@ -0,0 +1,950 @@
+{
+  "factorizations": [
+    {
+      "entrance": [
+        45
+      ],
+      "left": {
+        "columns": 512,
+        "denominator_exponents": [
+          4
+        ],
+        "entries": 262144,
+        "matrix_sha256": "9e4650ae6a986e9056006c644a5591264da27d356ca99e8a6fd697892885d065",
+        "name": "lhsLit1",
+        "nonzero_entries": 65536,
+        "source_executor_checked": false
+      },
+      "pair": 1,
+      "right": {
+        "columns": 512,
+        "denominator_exponents": [
+          4
+        ],
+        "entries": 262144,
+        "matrix_sha256": "9e4650ae6a986e9056006c644a5591264da27d356ca99e8a6fd697892885d065",
+        "name": "rhsLit1",
+        "nonzero_entries": 65536,
+        "source_executor_checked": false
+      },
+      "terminal": [
+        256,
+        128,
+        64,
+        33,
+        16,
+        9,
+        5,
+        2
+      ]
+    },
+    {
+      "entrance": [
+        51
+      ],
+      "left": {
+        "columns": 512,
+        "denominator_exponents": [
+          4
+        ],
+        "entries": 262144,
+        "matrix_sha256": "eb8aa8c90006ff1c22d02e521a3419d0996137ab04983c89c6bf37aa9151b4c1",
+        "name": "lhsLit2",
+        "nonzero_entries": 65536,
+        "source_executor_checked": false
+      },
+      "pair": 2,
+      "right": {
+        "columns": 512,
+        "denominator_exponents": [
+          4
+        ],
+        "entries": 262144,
+        "matrix_sha256": "eb8aa8c90006ff1c22d02e521a3419d0996137ab04983c89c6bf37aa9151b4c1",
+        "name": "rhsLit2",
+        "nonzero_entries": 65536,
+        "source_executor_checked": false
+      },
+      "terminal": [
+        256,
+        128,
+        64,
+        33,
+        17,
+        8,
+        4,
+        3
+      ]
+    },
+    {
+      "entrance": [
+        30
+      ],
+      "left": {
+        "columns": 512,
+        "denominator_exponents": [
+          4
+        ],
+        "entries": 262144,
+        "matrix_sha256": "49144589207537c8084213bb2b245d93787563a0e2fcf870cde32b02ebf149b7",
+        "name": "lhsLit3",
+        "nonzero_entries": 65536,
+        "source_executor_checked": false
+      },
+      "pair": 3,
+      "right": {
+        "columns": 512,
+        "denominator_exponents": [
+          4
+        ],
+        "entries": 262144,
+        "matrix_sha256": "49144589207537c8084213bb2b245d93787563a0e2fcf870cde32b02ebf149b7",
+        "name": "rhsLit3",
+        "nonzero_entries": 65536,
+        "source_executor_checked": false
+      },
+      "terminal": [
+        256,
+        128,
+        64,
+        32,
+        18,
+        10,
+        6,
+        1
+      ]
+    }
+  ],
+  "kind": "independent finite semantic binding audit",
+  "literal_bindings": [
+    {
+      "literal_gates": 5,
+      "literal_sha256": "6c4a4db870d51ed8932a6f14df0fc6a42f2fc72a9cc31fa15cdeeb0ce8e2e806",
+      "name": "fE1"
+    },
+    {
+      "literal_gates": 12,
+      "literal_sha256": "508c80a80c4e360f7437f0a198658f4b29967bd862a5669372d70f8c896de144",
+      "name": "fU1"
+    },
+    {
+      "literal_gates": 4,
+      "literal_sha256": "6b47fd36cedb60bf0a9824583845770d66cd44689a88c3dc5ae2221417f3dc38",
+      "name": "wL1"
+    },
+    {
+      "literal_gates": 4,
+      "literal_sha256": "f7a8fee03229b5ddf3a5309c84a06729789cf48e8b0aef7d2e9eeec4cc55fbd6",
+      "name": "wR1"
+    },
+    {
+      "literal_gates": 5,
+      "literal_sha256": "8f66204e0a3bf473f7dfb34b4d35ba2b3481f6d97fa857258a6ad9eb77814433",
+      "name": "fE2"
+    },
+    {
+      "literal_gates": 12,
+      "literal_sha256": "f6e5fc268323691f60494708f13350ae3a6355dacd34ace5181b07ad5c3a72ac",
+      "name": "fU2"
+    },
+    {
+      "literal_gates": 4,
+      "literal_sha256": "ba1220263642d03b2a3de0eaa0a871106d484f435f894a60c7dfb5fec138ffa7",
+      "name": "wL2"
+    },
+    {
+      "literal_gates": 4,
+      "literal_sha256": "628df08aa196d47a77432e4b198a4e33d66769259d30ae121c0a192235cfa910",
+      "name": "wR2"
+    },
+    {
+      "literal_gates": 5,
+      "literal_sha256": "e4bf81784195b7b7644bde0f984ff905fe716e4503869ae75e4bd53dadbcdb54",
+      "name": "fE3"
+    },
+    {
+      "literal_gates": 12,
+      "literal_sha256": "e3e0a5dd7d5f342f5f073ad4317ad5c1b11ec3bcb4f5d7fd6ab8668679620079",
+      "name": "fU3"
+    },
+    {
+      "literal_gates": 4,
+      "literal_sha256": "cec4eadcf5f4489ac8f9d053088d1325ff7b45dfdcb902c40f53578a528d84f3",
+      "name": "wL3"
+    },
+    {
+      "literal_gates": 4,
+      "literal_sha256": "4ca54b9c129ffb7c8c48fbde681ac899612770f3938f192652833bab6be793ca",
+      "name": "wR3"
+    }
+  ],
+  "new_kappa": false,
+  "new_lean_build": false,
+  "pairs": 3,
+  "primitive_operator_checks": [
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        1
+      ],
+      "entries": 262144,
+      "matrix_sha256": "8cf02896d98e1ee29e1e3a9e9228144c0f34c441a8705442784cfcd2ef5cc722",
+      "name": "fE1",
+      "nonzero_entries": 1024,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        1
+      ],
+      "entries": 262144,
+      "matrix_sha256": "17d2d2d9bf3ac5d6d9f50dc056fa545461450cb391ad739fbe84ed5fff378819",
+      "name": "fE1_inverse",
+      "nonzero_entries": 1024,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        4
+      ],
+      "entries": 262144,
+      "matrix_sha256": "78227df622706eddbd83b26de7cead83856b9aab813a3c14dc35a3a5c2826dee",
+      "name": "fU1",
+      "nonzero_entries": 131072,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        4
+      ],
+      "entries": 262144,
+      "matrix_sha256": "948af96a4e7f11b24bfabc9049ad8b66e52b4f4efb286316dd48fd7c665c5409",
+      "name": "fU1_inverse",
+      "nonzero_entries": 131072,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "a02ee6593865ae9eb1feb481cf9a98d0823f87faa0d50d5177e679f0240b49b9",
+      "name": "wL1",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "147bb6055fa7223506ea6400674c02fa1e8445e88da63989b56cf7bbf1d4e0b0",
+      "name": "wL1_inverse",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "ccbad997091f14f727f870bd2e8e1755138a5edef7aa3edab0f811082513a371",
+      "name": "wR1",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "9fc662cd3281a3b09765099c42af61261b9ecfec5695a725525ca39bc3a724a4",
+      "name": "wR1_inverse",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        1
+      ],
+      "entries": 262144,
+      "matrix_sha256": "3ac5a0b2af15b3fd9f75ff741315729834f106ff69e923011fb4164c31bde372",
+      "name": "fE2",
+      "nonzero_entries": 1024,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        1
+      ],
+      "entries": 262144,
+      "matrix_sha256": "f69f4499b0c0d1f6a42018b436a7f1516bed2772ebd0f7774593bfc05f7bd256",
+      "name": "fE2_inverse",
+      "nonzero_entries": 1024,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        4
+      ],
+      "entries": 262144,
+      "matrix_sha256": "fd86ecde3c4260d74231a3f6e177214fe467a6b2afd697a71a93a644c5eb0662",
+      "name": "fU2",
+      "nonzero_entries": 131072,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        4
+      ],
+      "entries": 262144,
+      "matrix_sha256": "012c520a4b23ff68b839291076f9a73a4f78a17104bab67068e577f6b9453e20",
+      "name": "fU2_inverse",
+      "nonzero_entries": 131072,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "13ef2614131589f1f9da573391317acacac00563b7efb9e6ae30b1422139c31b",
+      "name": "wL2",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "0aa81e682f6a4fac0ecc979343ed785bf80c5f22cf32233f5b159e3cc1bd2aa9",
+      "name": "wL2_inverse",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "e6fce263e0b9db7cd623ee5363a3c027f808afbad04fad455a89905136abd0c2",
+      "name": "wR2",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "62b9fb72303a865e254fee2a5481f2c0a55375f66e7500f2ff4dae1e5acf4f22",
+      "name": "wR2_inverse",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        1
+      ],
+      "entries": 262144,
+      "matrix_sha256": "2c6e7afb0db05297514a77db6bcbef6fbb5a72d45fec3c8a8e1cd834f3e57034",
+      "name": "fE3",
+      "nonzero_entries": 1024,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        1
+      ],
+      "entries": 262144,
+      "matrix_sha256": "e7c45f5a6e4b1a42f80189fcf78419299a41bd732003a6a80b83835d7583638e",
+      "name": "fE3_inverse",
+      "nonzero_entries": 1024,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        4
+      ],
+      "entries": 262144,
+      "matrix_sha256": "3828cfdc957df4af2f72429700173c35719dd656bbfa968d41cb1047a6fa55cf",
+      "name": "fU3",
+      "nonzero_entries": 131072,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        4
+      ],
+      "entries": 262144,
+      "matrix_sha256": "0c92b32b02a7e9be87c138c1d225583b1f2e08db3395b342cf24878eddcfeab3",
+      "name": "fU3_inverse",
+      "nonzero_entries": 131072,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "c75ed45f824376926d1ea84590fcb1a69d9aa988ee2362addf8177fe5bc731ab",
+      "name": "wL3",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "cb5ae0c674488401de5a3fff6ce4ee464516fa5446c39aa45d9cc9bf28f5286c",
+      "name": "wL3_inverse",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "61de28a3f5be5fc68c29dce97f1062289904f151a32828d3658364fdab4dc54c",
+      "name": "wR3",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    },
+    {
+      "columns": 512,
+      "denominator_exponents": [
+        0
+      ],
+      "entries": 262144,
+      "matrix_sha256": "33ca2eccb8ee51e7e0663981e693cfb57dca5aa222138550f261306c2dba8b3e",
+      "name": "wR3_inverse",
+      "nonzero_entries": 512,
+      "source_executor_checked": true
+    }
+  ],
+  "schema_version": 1,
+  "semantic_controls": [
+    {
+      "mutation": "global_phase",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "translation",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "permutation_direction",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          1,
+          -1,
+          4
+        ],
+        "input": 1,
+        "output": 4
+      }
+    },
+    {
+      "mutation": "input_character",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          -1,
+          1,
+          4
+        ],
+        "expected": [
+          1,
+          -1,
+          4
+        ],
+        "input": 1,
+        "output": 4
+      }
+    },
+    {
+      "mutation": "C_sign",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "spectator_axis",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "sides_swapped",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "reversed_order",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "entrance_not_inverted",
+      "pair": 1,
+      "witness": {
+        "actual": [
+          1,
+          1,
+          4
+        ],
+        "expected": [
+          0,
+          0,
+          4
+        ],
+        "input": 0,
+        "output": 0
+      }
+    },
+    {
+      "mutation": "global_phase",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 3
+      }
+    },
+    {
+      "mutation": "translation",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 3
+      }
+    },
+    {
+      "mutation": "permutation_direction",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          1,
+          -1,
+          4
+        ],
+        "input": 1,
+        "output": 2
+      }
+    },
+    {
+      "mutation": "input_character",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          -1,
+          1,
+          4
+        ],
+        "expected": [
+          1,
+          -1,
+          4
+        ],
+        "input": 1,
+        "output": 2
+      }
+    },
+    {
+      "mutation": "C_sign",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 3
+      }
+    },
+    {
+      "mutation": "spectator_axis",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 3
+      }
+    },
+    {
+      "mutation": "sides_swapped",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 3
+      }
+    },
+    {
+      "mutation": "reversed_order",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 3
+      }
+    },
+    {
+      "mutation": "entrance_not_inverted",
+      "pair": 2,
+      "witness": {
+        "actual": [
+          1,
+          1,
+          4
+        ],
+        "expected": [
+          0,
+          0,
+          4
+        ],
+        "input": 0,
+        "output": 0
+      }
+    },
+    {
+      "mutation": "global_phase",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 6
+      }
+    },
+    {
+      "mutation": "translation",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 6
+      }
+    },
+    {
+      "mutation": "permutation_direction",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          1,
+          -1,
+          4
+        ],
+        "input": 2,
+        "output": 4
+      }
+    },
+    {
+      "mutation": "input_character",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          1,
+          1,
+          4
+        ],
+        "input": 1,
+        "output": 6
+      }
+    },
+    {
+      "mutation": "C_sign",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          -1,
+          -1,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 6
+      }
+    },
+    {
+      "mutation": "spectator_axis",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          1,
+          -1,
+          4
+        ],
+        "expected": [
+          0,
+          0,
+          4
+        ],
+        "input": 0,
+        "output": 5
+      }
+    },
+    {
+      "mutation": "sides_swapped",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 6
+      }
+    },
+    {
+      "mutation": "reversed_order",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          0,
+          0,
+          4
+        ],
+        "expected": [
+          -1,
+          1,
+          4
+        ],
+        "input": 0,
+        "output": 6
+      }
+    },
+    {
+      "mutation": "entrance_not_inverted",
+      "pair": 3,
+      "witness": {
+        "actual": [
+          1,
+          1,
+          4
+        ],
+        "expected": [
+          0,
+          0,
+          4
+        ],
+        "input": 0,
+        "output": 0
+      }
+    }
+  ],
+  "source_inputs": {
+    "research/community-hyperplane599-audit/lean-bindings.json": "313c03104fccf561c6cee457e5b0988b427636a47bc2d2db67b651244d000196",
+    "research/complex-571-hpeq5/code/hpe_adapters_local.py": "b5d976f7496eac0d9c7ed97b3a028efcf6950ec989f1789b8c6f5d2b325c40b3",
+    "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean": "c0c51407b4fa6ff230a79d5f3b07c83b7d1c4b433ce03513f0c4fb725bf3cbe1",
+    "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183",
+    "research/hyperplane-end-lean/NOTICE.md": "2ed2c5763f8dcb204351d3f9dd67bd6e04fa04b516b105f3c9e6ccceef4d344b",
+    "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9",
+    "research/split-centres-global/vendor/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962",
+    "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03"
+  },
+  "status": "PASS_HPE_LEAN_SEMANTIC_BINDING"
+}
diff --git a/research/hpe-lean-semantic-binding/SOURCES.json b/research/hpe-lean-semantic-binding/SOURCES.json
new file mode 100644
index 0000000000..615f3aa178
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/SOURCES.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/community-hyperplane599-audit/lean-bindings.json",
+      "usage": "input",
+      "git_blob": "2510771bf5e2e3acb7a13a8c6c0112438876dfab",
+      "sha256": "313c03104fccf561c6cee457e5b0988b427636a47bc2d2db67b651244d000196"
+    },
+    {
+      "path": "research/complex-571-hpeq5/code/hpe_adapters_local.py",
+      "usage": "input",
+      "git_blob": "f77c09a0cab29e27feae3b20e685df34a3545406",
+      "sha256": "b5d976f7496eac0d9c7ed97b3a028efcf6950ec989f1789b8c6f5d2b325c40b3"
+    },
+    {
+      "path": "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean",
+      "usage": "input",
+      "git_blob": "5970d81439b8bca2935a935d964779845a45057c",
+      "sha256": "c0c51407b4fa6ff230a79d5f3b07c83b7d1c4b433ce03513f0c4fb725bf3cbe1"
+    },
+    {
+      "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean",
+      "usage": "input",
+      "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869",
+      "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183"
+    },
+    {
+      "path": "research/hyperplane-end-lean/NOTICE.md",
+      "usage": "input",
+      "git_blob": "2afcca845b1a40a5cc36450e825688c75791b5e4",
+      "sha256": "2ed2c5763f8dcb204351d3f9dd67bd6e04fa04b516b105f3c9e6ccceef4d344b"
+    },
+    {
+      "path": "research/hyperplane-end-lean/PROOF.md",
+      "usage": "input",
+      "git_blob": "a94a2ac168c088a1282ea411766bc859178620df",
+      "sha256": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9"
+    },
+    {
+      "path": "research/split-centres-global/vendor/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    },
+    {
+      "path": "scripts/verify_hpe_lean_binding.py",
+      "usage": "input",
+      "git_blob": "d295b028edc531dfbfaa023370a9528bada35572",
+      "sha256": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03"
+    }
+  ]
+}
diff --git a/research/hpe-lean-semantic-binding/TASK.json b/research/hpe-lean-semantic-binding/TASK.json
new file mode 100644
index 0000000000..2674d0a075
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/TASK.json
@@ -0,0 +1,114 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 2,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "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."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently bind the three retained noncold HPE pair records and their twelve primitive Lean circuit literals to exact closed-form kernels and the retained Python semantics on all 512 basis columns, in both orientations; verify the three residual factorizations.",
+  "scope_change_reason": "The assigned card explicitly permits a theorem-to-certificate binding audit. This refines that method to the semantic port for Exact.lean pair1/pair2/pair3, without a new formal arithmetic proof or a full multiplication claim.",
+  "bottleneck_link": "The selected construction inherits formal interface assumptions. A finite source-to-formal semantic check strengthens one precisely bounded correspondence without changing the paid recursive profile or asserting that other realization and transfer obligations are discharged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the complete three-pair finite comparison and meaningful failure controls; report any discrepancy exactly. Do not extend to an unbounded frame-port theorem or a supplier adoption. Reserve the final quarter of the bounded session for verification and handoff.",
+  "outcome": "completed",
+  "evidence": "RESULT.json: twelve source constructors match the primitive Lean literal circuits; 24 forward/inverse operators each pass 512 columns against independent kernels and source execution; six composite circuits pass all columns; three residual identities pass exact kernel equality; 27 semantic faults have exact coefficient witnesses. Seven focused tests cover additional mathematical and source/receipt/relocation boundaries.",
+  "author": "commdata2338",
+  "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance in research, derivation, implementation, verification and writing. No independent human review claimed.",
+  "open_questions": [
+    {
+      "question": "Can source-to-formal gate semantics be proved for a shared serialized five-gate grammar?",
+      "why_it_matters": "This could reduce the manual semantic-translation trust boundary left by a finite binding audit.",
+      "first_step": "Specify a small formal interpreter for the five gate tags and prove permutation and C-gate correspondence with an explicit common semantics.",
+      "blocked_by": "A formal model of the Python execution semantics or a separately verified common compiler is needed; additional finite examples alone do not establish the general statement."
+    },
+    {
+      "question": "Can one current emitted helper be bound end-to-end to these exact operator identities?",
+      "why_it_matters": "An invocation needs actual wrapper placement, scalar rows and labels in addition to a matching pair recipe.",
+      "first_step": "Pin one emitted word using a certified pair; trace both wrapper records and their event positions, then verify the unit helper row and label and hosting hypotheses.",
+      "blocked_by": "The emitted word, complete source closure and the remaining realization hypotheses must be supplied; this package does not newly replay the historical 38-helper runs."
+    }
+  ],
+  "assignment": {
+    "nonce": "96f499b6a9e557186c7e873f3edd9551",
+    "track": "independent-verification",
+    "scope_key": "e3ffea67887eeb4c396c",
+    "method": "Audit a formal theorem-to-certificate binding independently.",
+    "refined_scope_key": "HPE-three-pairs/Lean-literals-to-independent-kernels/all-512-columns",
+    "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1394",
+    "other_suggestion": {
+      "task_id": "independent-moment",
+      "scope_key": "c191650c0fa8d2fa514e",
+      "reason_passed": "Independent endpoint engines, PR1293 D/E and PR1262 complex emitted-ledger work already cover the obvious selected-record scopes."
+    }
+  },
+  "task_card": {
+    "task_id_and_scope_key": "formal-interface-lemma / e3ffea67887eeb4c396c; HPE-three-pairs/Lean-literals-to-independent-kernels/all-512-columns",
+    "base_and_heads": {
+      "base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+      "retained_PR593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4",
+      "retained_PR599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32",
+      "selected_PR1094_context": "0fc329d0bec93ca7cd288eaea1295172e8789810",
+      "pending_implementation_dependencies": []
+    },
+    "concrete_object_and_question": "Independently bind the three retained noncold HPE pair records and their twelve primitive Lean circuit literals to exact closed-form kernels and the retained Python semantics on all 512 basis columns, in both orientations; verify the three residual factorizations.",
+    "scope_status_and_reason": "refined: The assigned card explicitly permits a theorem-to-certificate binding audit. This refines that method to the semantic port for Exact.lean pair1/pair2/pair3, without a new formal arithmetic proof or a full multiplication claim.",
+    "claim_audited": "Exact.lean canon and Mono.gates faithfully implement the retained Python canonical_frame and monomial_op semantics for the three certified pairs.",
+    "method_and_domain": "Span-enumerated coordinate charts and closed-form Gaussian-dyadic kernels versus row-pullback literal execution, plus source constructor/executor differential checks; exactly three E dimension1/U dimension8 pairs, all 512 input/output coordinates, forward and inverse, all residual factors.",
+    "nearest_overlap": [
+      {
+        "pr": 702,
+        "head": "27db45ac6befa99d6c06be920a93845023e81937",
+        "distinction": "Fourteen rank-four cold wrappers, rather than three noncold rank-seven Lean pairs and their semantic port."
+      },
+      {
+        "pr": 712,
+        "head": "4773b879a1087540f5919c726ec8c670dadfa0c5",
+        "distinction": "One rank-four cold wrapper by symbolic phases; no imported implementation."
+      },
+      {
+        "pr": 1255,
+        "head": "add1e2673ef000c097ec0fd70058e644af048d6b",
+        "distinction": "Physical chart phase rebases rather than the fixed formal circuit literals."
+      }
+    ],
+    "full_cost_budget_and_observable_improvement": "No circuit, recursive-profile or exponent change. Added evidence must be complete exact finite semantic correspondence with independent failure detection; an unchanged successful construction is corroboration.",
+    "success_falsification_and_cap": "Every listed matrix column agrees, exact residual identities hold and semantic faults reject. A differing exact coefficient falsifies the claimed binding. Standard-library execution, one process for the audit, 60-minute session budget, no more than eight busy processes or threads and 16 GiB.",
+    "predecessor_authors": "Jeremy Kothe/jeremykothe2; DreamingOfClouds; icekylinx; Chafik Boukhalfa/chafreaky; Zhihao Chen/jacklightChen and the retained realization/hosting lineage. Nearby audits: BigCactusLabs, Joshua Snider/jsnider3 and Gareth Davidson/bitplane.",
+    "artifact_and_reproduce": "research/hpe-lean-semantic-binding/; python3 -I -B research/hpe-lean-semantic-binding/verify.py"
+  }
+}
diff --git a/research/hpe-lean-semantic-binding/VERIFY.json b/research/hpe-lean-semantic-binding/VERIFY.json
new file mode 100644
index 0000000000..c73468be98
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/VERIFY.json
@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/community-hyperplane599-audit/lean-bindings.json",
+    "research/complex-571-hpeq5/code/hpe_adapters_local.py",
+    "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean",
+    "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean",
+    "research/hyperplane-end-lean/NOTICE.md",
+    "research/hyperplane-end-lean/PROOF.md",
+    "research/split-centres-global/vendor/clifford_exact.py",
+    "scripts/verify_hpe_lean_binding.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Independent all-column primitive/inverse and residual matrices, source constructors/executor, exact receipt and 27 semantic mutations."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-m",
+        "unittest",
+        "discover",
+        "-s",
+        "{package}",
+        "-p",
+        "test_verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Seven focused mathematical, literal/source/receipt corruption, overwrite and read-only optimized relocation tests."
+    }
+  ]
+}
diff --git a/research/hpe-lean-semantic-binding/test_verify.py b/research/hpe-lean-semantic-binding/test_verify.py
new file mode 100644
index 0000000000..8199304153
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/test_verify.py
@@ -0,0 +1,145 @@
+"""Mathematical and failure-boundary tests for the finite binding audit."""
+import copy
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+
+HERE = Path(__file__).resolve().parent
+SPEC = importlib.util.spec_from_file_location("hpe_binding_audit", HERE / "verify.py")
+audit = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(audit)
+
+
+class BindingTests(unittest.TestCase):
+    @classmethod
+    def setUpClass(cls):
+        cls.text = (audit.ROOT / audit.EXACT).read_text(encoding="utf-8")
+        cls.pairs, cls.circuits = audit.literal_data(cls.text)
+
+    def test_semantic_C_square_and_inverse(self):
+        """C(q)^2=X(q), C(q)^* C(q)=I, including non-coordinate q."""
+        for q in (0, 1, 3, 128, 511):
+            square = audit.compile_literal([["cg", q, True], ["cg", q, True]])
+            inverse = audit.compile_literal([["cg", q, False], ["cg", q, True]])
+            for x in range(audit.N):
+                self.assertEqual(audit.run_literal(square, x), ({x ^ q: (1, 0)}, 0))
+                self.assertEqual(audit.run_literal(inverse, x), ({x: (1, 0)}, 0))
+
+    def test_semantic_zero_column_does_not_bind_input_character(self):
+        """An actual Z0 mutation preserves column zero and changes 256 columns."""
+        original = self.circuits["rhsLit1"]
+        mutant = copy.deepcopy(original)
+        mutant[0][2][0] = (mutant[0][2][0] + 2) % 4
+        c0, c1 = map(audit.compile_literal, (original, mutant))
+        changed = []
+        for x in range(audit.N):
+            v0, e0 = audit.run_literal(c0, x)
+            v1, e1 = audit.run_literal(c1, x)
+            self.assertEqual(e0, e1)
+            sign = -1 if x & 1 else 1
+            self.assertEqual(v1, {y: (sign*a, sign*b) for y, (a, b) in v0.items()})
+            if v0 != v1:
+                changed.append(x)
+        self.assertEqual(changed, list(range(1, audit.N, 2)))
+
+    def test_semantic_frame_literal_corruption(self):
+        mutant = copy.deepcopy(self.circuits["fU1"])
+        position = next(i for i, g in enumerate(mutant) if g[0] == "cg")
+        mutant[position][2] = False
+        compiled = audit.compile_literal(mutant)
+        expected = audit.frame_kernel(self.pairs[0][1])
+        with self.assertRaisesRegex(ValueError, "operator mismatch"):
+            audit.assert_column(audit.run_literal(compiled, 0), expected(0), "changed frame C sign")
+
+    def test_binding_source_drift(self):
+        """Check the bytes actually loaded, before any producer execution."""
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary)
+            for name in audit.check_sources():
+                target = root / name
+                target.parent.mkdir(parents=True, exist_ok=True)
+                shutil.copyfile(audit.ROOT / name, target)
+            self.assertEqual(audit.check_sources(root), audit.check_sources())
+            path = root / audit.CLIFFORD
+            path.write_bytes(path.read_bytes().replace(b"a-sgn*b", b"a+sgn*b", 1))
+            with self.assertRaisesRegex(ValueError, "source drift"):
+                audit.check_sources(root)
+
+    def test_binding_literal_grammar_and_inverse(self):
+        pair = audit.declaration(self.text, "pair1", "Pair")
+        with self.assertRaisesRegex(ValueError, "missing/duplicate"):
+            audit.literal_data(self.text + "\ndef pair1 : Pair := " + pair + "\n\n")
+        bad = self.text.replace(".cg 1 true,", ".cg 1 true ignored,", 1)
+        with self.assertRaisesRegex(ValueError, "bad C gate"):
+            audit.literal_data(bad)
+        bad_gate = copy.deepcopy(next(g for g in self.circuits["wR1"] if g[0] == "pm"))
+        bad_gate[2][0] ^= 1
+        with self.assertRaisesRegex(ValueError, "bad permutation inverse"):
+            audit.compile_literal([bad_gate])
+
+    def test_receipt_corruption_typing_and_overwrite(self):
+        result = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8"))
+        with tempfile.TemporaryDirectory() as temporary:
+            path = Path(temporary) / "receipt.json"
+            path.write_text(json.dumps(result), encoding="utf-8")
+            audit.validate_receipt(path, result)
+            bad = copy.deepcopy(result)
+            bad["primitive_operator_checks"][0]["matrix_sha256"] = "0" * 64
+            path.write_text(json.dumps(bad), encoding="utf-8")
+            with self.assertRaisesRegex(ValueError, "receipt mismatch"):
+                audit.validate_receipt(path, result)
+            bad = copy.deepcopy(result); bad["schema_version"] = True
+            path.write_text(json.dumps(bad), encoding="utf-8")
+            with self.assertRaisesRegex(ValueError, "receipt mismatch"):
+                audit.validate_receipt(path, result)
+            path.write_text('{"pairs":3,"pairs":3}', encoding="utf-8")
+            with self.assertRaisesRegex(ValueError, "duplicate receipt key"):
+                audit.validate_receipt(path, result)
+            before = path.read_bytes()
+            with self.assertRaisesRegex(ValueError, "refusing to overwrite"):
+                audit.main(["--write-receipt", str(path)])
+            self.assertEqual(path.read_bytes(), before)
+
+    def test_readonly_relocation_optimized_replay(self):
+        """A source export replays under -I -O -B with no writes or Git access."""
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary)
+            package = root / "research" / HERE.name
+            package.mkdir(parents=True)
+            for source in HERE.iterdir():
+                if source.is_file():
+                    shutil.copyfile(source, package / source.name)
+            for name in audit.check_sources():
+                target = root / name
+                target.parent.mkdir(parents=True, exist_ok=True)
+                shutil.copyfile(audit.ROOT / name, target)
+            files = sorted(p for p in root.rglob("*") if p.is_file())
+            directories = sorted((p for p in root.rglob("*") if p.is_dir()), reverse=True)
+            before = {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() for p in files}
+            try:
+                for p in files:
+                    p.chmod(0o444)
+                for p in directories:
+                    p.chmod(0o555)
+                process = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")],
+                                         cwd=root, capture_output=True, text=True, timeout=180)
+                self.assertEqual(process.returncode, 0, process.stderr[-2000:])
+                self.assertIn("PASS_HPE_LEAN_SEMANTIC_BINDING", process.stdout)
+                after = {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest()
+                         for p in root.rglob("*") if p.is_file()}
+                self.assertEqual(before, after)
+            finally:
+                for p in directories:
+                    p.chmod(0o755)
+                for p in files:
+                    p.chmod(0o644)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/research/hpe-lean-semantic-binding/verify.py b/research/hpe-lean-semantic-binding/verify.py
new file mode 100644
index 0000000000..234831bc72
--- /dev/null
+++ b/research/hpe-lean-semantic-binding/verify.py
@@ -0,0 +1,496 @@
+#!/usr/bin/env python3
+"""Finite semantic audit of the retained Lean HPE pairs. Apache-2.0.
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+The source engine is a differential-test subject, not the independent kernel
+oracle. No source verifier or packed equality algorithm is imported.
+"""
+import argparse
+import ast
+import copy
+import hashlib
+import json
+from pathlib import Path
+import re
+import sys
+import types
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+EXACT = "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean"
+CLIFFORD = "research/split-centres-global/vendor/clifford_exact.py"
+ADAPTERS = "research/complex-571-hpeq5/code/hpe_adapters_local.py"
+N = 512
+ZERO = (0, 0)
+UNITS = ((1, 0), (0, 1), (-1, 0), (0, -1))
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def canonical_json(value):
+    return json.dumps(value, sort_keys=True, separators=(",", ":"))
+
+
+def digest(value):
+    return hashlib.sha256(canonical_json(value).encode()).hexdigest()
+
+
+def validate_receipt(path, actual):
+    def unique_object(pairs):
+        out = {}
+        for key, value in pairs:
+            require(key not in out, "duplicate receipt key: " + key)
+            out[key] = value
+        return out
+
+    expected = json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_object)
+    # Python equality identifies True, 1 and 1.0; JSON evidence must not.
+    require(canonical_json(expected) == canonical_json(actual), "receipt mismatch")
+
+
+def check_sources(root=ROOT, package=PACKAGE):
+    manifest = json.loads((package / "SOURCES.json").read_text(encoding="utf-8"))
+    result = {}
+    for row in manifest["files"]:
+        if row["usage"] != "input":
+            continue
+        path = Path(row["path"])
+        require(not path.is_absolute() and ".." not in path.parts, "invalid input path")
+        data = (root / path).read_bytes()
+        require(hashlib.sha256(data).hexdigest() == row["sha256"], "source drift: " + row["path"])
+        result[row["path"]] = row["sha256"]
+    return result
+
+
+def declaration(text, name, kind):
+    matches = list(re.finditer(r"^def " + re.escape(name) + r" : " + re.escape(kind)
+                              + r" :=\s*", text, re.M))
+    require(len(matches) == 1, "missing/duplicate declaration: " + name)
+    start = matches[0].end()
+    end = text.find("\n\n", start)
+    require(end >= 0, "unterminated declaration: " + name)
+    return text[start:end].strip()
+
+
+def literal_data(text):
+    """Closed grammar for source literals; no arbitrary Lean evaluation."""
+    pairs, circuits = [], {}
+    for i in range(1, 4):
+        raw = declaration(text, f"pair{i}", "Pair")
+        require(re.fullmatch(r"[0-9\s,\[\]⟨⟩]+", raw) is not None, "nonliteral pair")
+        pair = ast.literal_eval(raw.replace("⟨", "[").replace("⟩", "]"))
+        require(len(pair) == 4 and len(pair[0]) == 1 and len(pair[1]) == 8, "unexpected pair shape")
+        pairs.append(pair)
+        for prefix in ("fE", "fU", "wL", "wR", "lhsLit", "rhsLit"):
+            name = f"{prefix}{i}"
+            raw = declaration(text, name, "List Gate")
+            require(raw.startswith("[") and raw.endswith("]"), "nonlist circuit")
+            parts = re.split(r"\.(pm|dg|cg|xg|ph)\s+", raw[1:-1])
+            require(not parts[0].strip() and len(parts) % 2 == 1, "unparsed circuit content")
+            gates = []
+            for tag, args in zip(parts[1::2], parts[2::2]):
+                args = args.strip().removesuffix(",").strip()
+                if tag in ("pm", "dg"):
+                    m = re.fullmatch(r"(\[[0-9,\s]*\])\s+(\[[0-9,\s]*\])", args)
+                    require(m is not None, "bad two-list gate")
+                    gate = [tag, ast.literal_eval(m[1]), ast.literal_eval(m[2])]
+                elif tag == "cg":
+                    m = re.fullmatch(r"([0-9]+)\s+(true|false)", args)
+                    require(m is not None, "bad C gate")
+                    gate = [tag, int(m[1]), m[2] == "true"]
+                else:
+                    require(re.fullmatch(r"[0-9]+", args) is not None, "bad scalar gate")
+                    gate = [tag, int(args)]
+                gates.append(gate)
+            require(gates, "empty literal circuit")
+            circuits[name] = gates
+    return pairs, circuits
+
+
+def mul(a, b):
+    return a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0]
+
+
+def add(a, b):
+    return a[0] + b[0], a[1] + b[1]
+
+
+def rotate(z, p):
+    a, b = z
+    return ((a, b), (-b, a), (-a, -b), (b, -a))[p % 4]
+
+
+def normalize(vector, exponent):
+    vector = {x: z for x, z in vector.items() if z != ZERO}
+    while exponent and all(a % 2 == 0 and b % 2 == 0 for a, b in vector.values()):
+        vector = {x: (a // 2, b // 2) for x, (a, b) in vector.items()}
+        exponent -= 1
+    return vector, exponent
+
+
+def packed_column(vector):
+    v, e = normalize(*vector)
+    return [e, [[x, *v[x]] for x in sorted(v)]]
+
+
+def assert_column(actual, expected, context):
+    a, b = normalize(*actual), normalize(*expected)
+    if a != b:
+        x = next((x for x in range(N)
+                  if tuple(c * 2**b[1] for c in a[0].get(x, ZERO))
+                  != tuple(c * 2**a[1] for c in b[0].get(x, ZERO))), None)
+        raise ValueError(f"operator mismatch: {context}; output={x}")
+
+
+# Literal evaluator: row-mask pullbacks and term-by-term gate application.
+def literal_mv(rows, x):
+    return sum(((r & x).bit_count() % 2) << i for i, r in enumerate(rows))
+
+
+def literal_q(rows, linear, x):
+    return (sum(linear[i] for i in range(9) if (x >> i) & 1)
+            + 2 * sum(((rows[i] >> (i + 1)) & (x >> (i + 1))).bit_count()
+                      for i in range(9) if (x >> i) & 1)) % 4
+
+
+def adjoint(circuit):
+    out = []
+    for g in reversed(circuit):
+        if g[0] == "pm":
+            out.append(["pm", g[2], g[1]])
+        elif g[0] == "dg":
+            out.append(["dg", g[1], [(-a) % 4 for a in g[2]]])
+        elif g[0] == "cg":
+            out.append(["cg", g[1], not g[2]])
+        elif g[0] == "ph":
+            out.append(["ph", (-g[1]) % 4])
+        else:
+            out.append(copy.deepcopy(g))
+    return out
+
+
+def compile_literal(circuit):
+    out = []
+    for g in circuit:
+        if g[0] == "pm":
+            require(len(g[1]) == len(g[2]) == 9, "bad permutation shape")
+            forward = [literal_mv(g[1], x) for x in range(N)]
+            backward = [literal_mv(g[2], x) for x in range(N)]
+            require(sorted(forward) == list(range(N)) and
+                    all(backward[forward[x]] == x for x in range(N)), "bad permutation inverse")
+            out.append(("pull", backward))
+        elif g[0] == "dg":
+            require(len(g[1]) == len(g[2]) == 9, "bad diagonal shape")
+            out.append(("phase", [literal_q(g[1], g[2], x) for x in range(N)]))
+        elif g[0] == "xg":
+            require(0 <= g[1] < N, "bad translation")
+            out.append(("pull", [x ^ g[1] for x in range(N)]))
+        elif g[0] == "ph":
+            out.append(("phase", [g[1] % 4] * N))
+        elif g[0] == "cg":
+            require(0 <= g[1] < N and type(g[2]) is bool, "bad C gate")
+            out.append(("C", (g[1], 1 if g[2] else -1)))
+        else:
+            raise ValueError("unknown gate")
+    return out
+
+
+def run_literal(compiled, basis):
+    vec, exponent = {basis: (1, 0)}, 0
+    for tag, data in compiled:
+        if tag == "pull":
+            vec = {x: vec[y] for x, y in enumerate(data) if y in vec}
+        elif tag == "phase":
+            vec = {x: rotate(z, data[x]) for x, z in vec.items()}
+        else:
+            q, sign = data
+            result = {}
+            for x in vec.keys() | {x ^ q for x in vec}:
+                a, b = vec.get(x, ZERO)
+                c, d = vec.get(x ^ q, ZERO)
+                z = (a - sign*b + c + sign*d, b + sign*a + d - sign*c)
+                if z != ZERO:
+                    result[x] = z
+            vec, exponent = result, exponent + 1
+    return normalize(vec, exponent)
+
+
+# Independent kernels: enumerate charts by XORing columns, without producer
+# Gaussian elimination; phases sum over pairs of set coordinates.
+def coordinate_chart(frame):
+    require(len(set(frame)) == len(frame) and all(0 < u < N for u in frame), "invalid frame vectors")
+    columns, image = [], [0]
+    for u in list(frame) + [2**i for i in range(9)]:
+        if u not in image:
+            columns.append(u)
+            image += [v ^ u for v in image]
+    require(len(columns) == 9 and len(image) == N and len(set(image)) == N, "incomplete chart")
+    require(columns[:len(frame)] == list(frame), "dependent frame")
+    coordinate = [0] * N
+    for z, x in enumerate(image):
+        coordinate[x] = z
+    inverse_columns = [coordinate[2**i] for i in range(9)]
+    phases = []
+    for x in range(N):
+        bits = [i for i in range(9) if x & 2**i]
+        linear = sum(1 - inverse_columns[i].bit_count() % 2 for i in bits)
+        cross = sum((inverse_columns[i] & inverse_columns[j]).bit_count() % 2
+                    for pos, i in enumerate(bits) for j in bits[pos+1:])
+        phases.append((linear + 2 * cross) % 4)
+    return image, coordinate, phases
+
+
+def gaussian_power(z, n):
+    out = (1, 0)
+    for _ in range(n):
+        out = mul(out, z)
+    return out
+
+
+def fourier_weights(rank, inverse=False):
+    sign = -1 if inverse else 1
+    return [mul(gaussian_power((1, sign), rank - w),
+                gaussian_power((1, -sign), w)) for w in range(rank + 1)]
+
+
+def frame_kernel(frame, inverse=False):
+    rank = len(frame)
+    image, coordinate, phases = coordinate_chart(frame)
+    weights = fourier_weights(rank, inverse)
+
+    def column(x):
+        vec = {}
+        for delta in range(2**rank):
+            y = image[coordinate[x] ^ delta]
+            vec[y] = mul(UNITS[(phases[y] - phases[x]) % 4], weights[delta.bit_count()])
+        return normalize(vec, rank)
+
+    return column
+
+
+def monomial_kernel(record, inverse=False):
+    Q, linear, rows, offset, phase = record
+    require(len(Q) == len(linear) == len(rows) == 9, "bad monomial shape")
+    require(all(0 <= x < N for x in Q + rows) and 0 <= offset < N, "monomial mask out of range")
+    columns = [sum(((rows[j] // 2**i) % 2) * 2**j for j in range(9)) for i in range(9)]
+    images, factors = [], []
+    for x in range(N):
+        bits = [i for i in range(9) if x & 2**i]
+        y = offset
+        for i in bits:
+            y ^= columns[i]
+        q = phase + sum(linear[i] for i in bits)
+        q += 2 * sum((Q[i] // 2**j) % 2 for k, i in enumerate(bits) for j in bits[k+1:])
+        images.append(y)
+        factors.append(UNITS[q % 4])
+    require(sorted(images) == list(range(N)), "noninvertible monomial")
+    if inverse:
+        preimage = [0] * N
+        for x, y in enumerate(images):
+            preimage[y] = x
+        return lambda y: ({preimage[y]: (factors[preimage[y]][0], -factors[preimage[y]][1])}, 0)
+    return lambda x: ({images[x]: factors[x]}, 0)
+
+
+def fourier_kernel(rank=7, inverse=False):
+    weights = fourier_weights(rank, inverse)
+    return lambda x: normalize({x ^ d: weights[d.bit_count()] for d in range(2**rank)}, rank)
+
+
+def compose_columns(first, second, x):
+    av, ae = first(x)
+    rows = [(a, second(y)) for y, a in av.items()]
+    exponent = max((ae + be for _, (_, be) in rows), default=0)
+    out = {}
+    for a, (bv, be) in rows:
+        scale = 2**(exponent - ae - be)
+        for z, b in bv.items():
+            c = mul(a, b)
+            out[z] = add(out.get(z, ZERO), (scale*c[0], scale*c[1]))
+    return normalize(out, exponent)
+
+
+def composed(*operators):
+    def column(x):
+        def step(k, y):
+            if k == 0:
+                return operators[0](y)
+            return compose_columns(lambda z: step(k-1, z), operators[k], y)
+        return step(len(operators)-1, x)
+    return column
+
+
+def source_subject(root=ROOT):
+    module = types.ModuleType("hpe_binding_source_subject")
+    sys.modules[module.__name__] = module
+    exec(compile((root / CLIFFORD).read_text(encoding="utf-8"), CLIFFORD, "exec"), module.__dict__)
+    # Extract the pure decoder only; do not execute unrelated path/env setup.
+    tree = ast.parse((root / ADAPTERS).read_text(encoding="utf-8"))
+    functions = [node for node in tree.body if isinstance(node, ast.FunctionDef)
+                 and node.name == "monomial_op"]
+    require(len(functions) == 1, "source monomial decoder inventory")
+    namespace = dict(module.__dict__, n=9)
+    exec(compile(ast.Module(body=functions, type_ignores=[]), ADAPTERS, "exec"), namespace)
+    return module, namespace["monomial_op"]
+
+
+def source_circuit(circuit, source):
+    out = []
+    for g in circuit:
+        if g[0] == "P":
+            out.append(["pm", list(g[1]), list(source.inv(g[1], 9))])
+        elif g[0] == "D":
+            out.append(["dg", list(g[1]), list(g[2])])
+        elif g[0] == "C":
+            require(g[2] in (-1, 1), "source C sign")
+            out.append(["cg", g[1], g[2] == 1])
+        elif g[0] == "X":
+            out.append(["xg", g[1]])
+        elif g[0] == "phase":
+            out.append(["ph", g[1]])
+        else:
+            raise ValueError("unknown source gate")
+    return out
+
+
+def source_record(mono):
+    return dict(zip(("quadratic_rows", "linear_Z4", "matrix_rows", "offset", "phase"), mono, strict=True))
+
+
+def compare_operator(name, circuit, oracle, source_op=None):
+    compiled = compile_literal(circuit)
+    fingerprint, nonzero, denominators = hashlib.sha256(), 0, set()
+    for x in range(N):
+        expected = oracle(x)
+        assert_column(run_literal(compiled, x), expected, f"{name}, input={x}")
+        if source_op is not None:
+            vec, exponent = source_op.zero_state(x)
+            assert_column(({i: z for i, z in enumerate(vec) if z != ZERO}, exponent),
+                          expected, f"source {name}, input={x}")
+        fingerprint.update((canonical_json(packed_column(expected)) + "\n").encode())
+        v, e = normalize(*expected)
+        nonzero += len(v)
+        denominators.add(e)
+    return {"name": name, "columns": N, "entries": N*N, "nonzero_entries": nonzero,
+            "denominator_exponents": sorted(denominators), "matrix_sha256": fingerprint.hexdigest(),
+            "source_executor_checked": source_op is not None}
+
+
+def first_difference(circuit, oracle):
+    compiled = compile_literal(circuit)
+    for x in range(N):
+        actual, expected = run_literal(compiled, x), oracle(x)
+        if normalize(*actual) != normalize(*expected):
+            a, ae = normalize(*actual)
+            b, be = normalize(*expected)
+            y = next(y for y in range(N)
+                     if tuple(v * 2**be for v in a.get(y, ZERO))
+                     != tuple(v * 2**ae for v in b.get(y, ZERO)))
+            return {"input": x, "output": y, "actual": [*a.get(y, ZERO), ae],
+                    "expected": [*b.get(y, ZERO), be]}
+    raise ValueError("semantic mutation was not rejected")
+
+
+def semantic_controls(pairs, circuits):
+    controls = []
+    for i, (_, _, L, R) in enumerate(pairs, 1):
+        expected = composed(monomial_kernel(R), fourier_kernel(), monomial_kernel(L))
+        base, mutants = circuits[f"rhsLit{i}"], {}
+        v = copy.deepcopy(base); v[-1][1] = (v[-1][1] + 1) % 4
+        mutants["global_phase"] = v
+        v = copy.deepcopy(base)
+        k = next(k for k, g in enumerate(v) if g[0] == "xg"); v[k][1] ^= 1
+        mutants["translation"] = v
+        v = copy.deepcopy(base)
+        k = next(k for k, g in enumerate(v) if g[0] == "pm"); v[k][1], v[k][2] = v[k][2], v[k][1]
+        mutants["permutation_direction"] = v
+        v = copy.deepcopy(base)
+        k = next(k for k, g in enumerate(v) if g[0] == "dg"); v[k][2][0] = (v[k][2][0] + 2) % 4
+        mutants["input_character"] = v
+        v = copy.deepcopy(base)
+        k = next(k for k, g in enumerate(v) if g[0] == "cg"); v[k][2] = not v[k][2]
+        mutants["C_sign"] = v
+        v = copy.deepcopy(base)
+        k = next(k for k, g in enumerate(v) if g[0] == "cg"); v[k][1] = 128
+        mutants["spectator_axis"] = v
+        mutants["sides_swapped"] = (copy.deepcopy(circuits[f"wL{i}"])
+                                      + [["cg", 2**k, True] for k in range(7)]
+                                      + copy.deepcopy(circuits[f"wR{i}"]))
+        mutants["reversed_order"] = list(reversed(copy.deepcopy(base)))
+        mutants["entrance_not_inverted"] = circuits[f"fE{i}"] + circuits[f"fU{i}"]
+        for name, mutant in mutants.items():
+            controls.append({"pair": i, "mutation": name, "witness": first_difference(mutant, expected)})
+    return controls
+
+
+def audit(root=ROOT):
+    sources = check_sources(root)
+    pairs, circuits = literal_data((root / EXACT).read_text(encoding="utf-8"))
+    source, decoder = source_subject(root)
+    checks, composition, mapping = [], [], []
+    for i, (E, U, L, R) in enumerate(pairs, 1):
+        require(E[0] in coordinate_chart(U)[0][:256], "entrance not contained in terminal")
+        objects = [("fE", E, source.canonical_frame(9, tuple(E)), frame_kernel),
+                   ("fU", U, source.canonical_frame(9, tuple(U)), frame_kernel),
+                   ("wL", L, decoder(source_record(L)), monomial_kernel),
+                   ("wR", R, decoder(source_record(R)), monomial_kernel)]
+        for prefix, data, op, kernel in objects:
+            name = f"{prefix}{i}"
+            require(source_circuit(op.circuit, source) == circuits[name],
+                    "source constructor differs from Lean literal: " + name)
+            mapping.append({"name": name, "literal_gates": len(circuits[name]),
+                            "literal_sha256": digest(circuits[name])})
+            for inverse in (False, True):
+                c = adjoint(circuits[name]) if inverse else circuits[name]
+                sop = op.adjoint() if inverse else op
+                checks.append(compare_operator(name + ("_inverse" if inverse else ""),
+                                               c, kernel(data, inverse), sop))
+        require(circuits[f"lhsLit{i}"] == adjoint(circuits[f"fE{i}"]) + circuits[f"fU{i}"],
+                "lhs literal composition")
+        require(circuits[f"rhsLit{i}"] == circuits[f"wR{i}"]
+                + [["cg", 2**k, True] for k in range(7)] + circuits[f"wL{i}"], "rhs literal composition")
+        lhs = composed(frame_kernel(E, True), frame_kernel(U))
+        rhs = composed(monomial_kernel(R), fourier_kernel(), monomial_kernel(L))
+        left = compare_operator(f"lhsLit{i}", circuits[f"lhsLit{i}"], lhs)
+        right = compare_operator(f"rhsLit{i}", circuits[f"rhsLit{i}"], rhs)
+        require(left["matrix_sha256"] == right["matrix_sha256"], "factorization digest mismatch")
+        # Acceptance uses exact equality too; hashes are only compact receipts.
+        for x in range(N):
+            assert_column(lhs(x), rhs(x), f"pair{i} exact factorization input={x}")
+        composition.append({"pair": i, "entrance": E, "terminal": U, "left": left, "right": right})
+    controls = semantic_controls(pairs, circuits)
+    return {"schema_version": 1, "status": "PASS_HPE_LEAN_SEMANTIC_BINDING",
+            "kind": "independent finite semantic binding audit", "source_inputs": sources,
+            "pairs": 3, "primitive_operator_checks": checks, "literal_bindings": mapping,
+            "factorizations": composition, "semantic_controls": controls,
+            "new_lean_build": False, "new_kappa": False}
+
+
+def main(argv=None):
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--write-receipt", type=Path,
+                        help="create a receipt exclusively; normal replay is read-only")
+    parser.add_argument("--receipt", type=Path, default=PACKAGE / "RESULT.json")
+    args = parser.parse_args(argv)
+    if args.write_receipt:
+        require(not args.write_receipt.exists(), "refusing to overwrite receipt")
+    result = audit()
+    if args.write_receipt:
+        with args.write_receipt.open("x", encoding="utf-8") as handle:
+            handle.write(json.dumps(result, indent=2, sort_keys=True) + "\n")
+    else:
+        validate_receipt(args.receipt, result)
+    count = len(result["primitive_operator_checks"])
+    print(f"PASS_HPE_LEAN_SEMANTIC_BINDING pairs=3 operators={count} "
+          f"operator_columns={count*N} factorizations=3 controls={len(result['semantic_controls'])} "
+          "no_new_lean_build no_new_kappa")
+
+
+if __name__ == "__main__":
+    try:
+        main()
+    except (ValueError, OSError, KeyError, SyntaxError) as exc:
+        raise SystemExit("FAIL_HPE_LEAN_SEMANTIC_BINDING: " + str(exc)) from exc