Bind emitted k8 helper 450 to the retained Lean wrapper pair

research/k8-hpe450-binding/README.md

@@ -0,0 +1,115 @@
+# Binding an emitted k8 helper to the retained Lean pair
+
+Helper **450** in the seven-slot k8 word has an exact unit output row and
+isolated input column in both emitted local orientations. Its actual wrapper
+events name the same entrance/terminal pair as `HyperplaneEnd.Exact.pair3`, and
+both regenerated wrapper monomials equal that Lean literal, including phase.
+This package connects these finite facts in one reproducible certificate.
+
+This is a partial theorem-to-emission binding, not a new Lean theorem, supplier
+admission or exponent improvement. The selected record is unchanged.
+
+The starting main commit is `ebedc0895eb4c06725af020bc1af165722b0a3ce`.
+At that commit, the selected PR1094 source manifest pins the k8 slot record used
+here. Its raw word content hash is
+`c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8`.
+The raw word retained by Josie Elliston's independent owner audit is rebuilt
+with the pinned native transport, emitter and wrapper generator. The resulting
+canonical payload and **both complete event lists** must match the published
+slot hashes. Gzip container bytes are not used to compare regenerated evidence.
+All consumed source files, including the Clifford engine, are pinned in
+[`SOURCES.json`](SOURCES.json).
+
+[`RESULT.json`](RESULT.json) records the following in each orientation:
+
+| Fact | Exact result |
+|---|---|
+| Complete emitted stream | 24,767 events; 19,693 scalar operations |
+| Scalar domain | 704 local registers and eight private center registers |
+| Helper's entrance and terminal frame IDs | `2` and `999` |
+| Entrance / terminal dimensions | 1 / 8; residual width 7, two spectators |
+| Pre / post wrapper positions, zero based | 7,852 / 24,562 |
+| Frame path | `2 -> 31 -> 556 -> 751 -> 999`, increments `2,3,1,1` |
+| Cleanup-tail touches | positions 16,495 and 16,507 |
+| Helper's output row and input column | exactly the coordinate vector for register 450 |
+
+The checker enumerates each frame's finite span, tracks the emitted frame tags
+and checks the wrapper order. Every scalar operand must carry its event's frame
+tag. No scalar operation or climb on the helper occurs outside its wrappers;
+its last scalar touch is in `cleanup_tail` and the final label remains `999`.
+The actual recipe key is `2:999`. Its ten monomial fields, frame vectors and
+width metadata are compared directly with `pair3` in the pinned Lean source.
+
+The scalar check is independent of the producers' full-matrix replay. Write the
+scalar map as `M = G_m ... G_1`, retaining the emitted COPY and CLEAR operations.
+Starting from `e_450^T`, reverse traversal multiplies this row by `G_m` through
+`G_1`, giving the entire row `e_450^T M`. Separately, forward traversal applies
+the gates to `e_450`, giving the entire column `M e_450`. All coefficients are
+exact rational numbers. The resulting row and column are both unit vectors,
+including zero coefficients on the private coordinates. Thus the scalar output
+is independent of every other arbitrary input, and the helper's initial value
+leaves no scalar residue in other registers.
+
+These are distinct obligations. One control inserts an extra read immediately
+after the helper's last tail touch. Its output row stays restored, but its dirt
+leaks to `L230` with coefficient `1/2` in the forward orientation, and to `L27`
+with coefficient `1` in the backward orientation. The column check rejects it.
+All **28 semantic controls** reach the mathematical checker without checksum
+guards. They also cover omitted/changed tail gates, missing/misplaced wrappers,
+wrong frame tags, global phases, translations and swapped wrapper sides.
+
+Under exact relabel recipes and the existing event-semantics correspondence,
+the unit row gives the unwrapped residual `T_U T_E^-1`. The checked wrapper
+placement gives `L^-1 T_U T_E^-1 R^-1`; the retained `exact_N_pair3` identity
+identifies this with `C7` on seven coordinates and identity on two spectators.
+The generic `hpe_block` statement is the relevant interface. This Python audit
+does **not** instantiate a Lean event word or prove that serialization
+correspondence. It does not discharge `RecipesExact` for all other emitted
+climbs/adapters, physical footprints, ownership, whole-call hosting, the all-size
+compiler, precision/tape bounds, complete costs or analytic transfer. It runs
+neither a fresh Lean build nor the full selected supplier cold replay.
+
+Reproduce from the repository root with Python 3.12; only the standard library
+is needed:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/k8-hpe450-binding
+```
+
+The registered replay regenerates temporary evidence, checks the complete saved
+receipt and runs five tests. A separate dense matrix implementation cross-checks
+all 512 three-operation words over an eight-operation alphabet, at all three
+local coordinates. The tests also reject malformed coefficients, source drift
+and a changed receipt, and replay an optimized source export without Git while
+preserving its input bytes. Normal verification writes only temporary output;
+`verify.py --write-result NEW_PATH` creates a receipt and refuses to overwrite it.
+
+The revision-2 task selector chose `formal-interface-lemma` with nonce
+`7fff7b3cd0d148756c5fc7685585eb0a`. [`TASK.json`](TASK.json) records the refinement
+and the [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1394#discussioncomment-18914238).
+[PR1415](https://github.com/CrocSwap/integer-mult-bounds/pull/1415), inspected at
+`0d8d2c3a96346756f02563b401a042ab97198e20`, already audits the three fixed operator
+identities on all 512 basis inputs. This package addresses its emitted-helper
+follow-up; it does not repeat that kernel audit or execute pending PR code.
+
+Credit belongs to Jeremy Kothe for the HPE Clifford formalization and k8
+construction, DreamingOfClouds for the wrapper and Lemma A/G work, icekylinx for
+the retained compiler, Rohan Arun for the selected packing, Josie Elliston and
+Sagar Thakrar for the retained k8 word/audit lineage, and @commdata2338 for
+PR1415's semantic audit and follow-up question. The underlying realization work
+of Chafik Boukhalfa, Zhihao Chen and the repository's other credited contributors
+is retained unchanged. New work: Hanson Sun (@bbMisk), with substantial OpenAI
+Codex assistance in analysis, implementation, validation and writing.
+Apache-2.0; original source notices are unchanged. No independent human review
+is claimed.
+
+## Open next questions
+
+- Can these finite facts be connected to `hpe_block` through an actual Lean
+  event word? Specify private COPY/CLEAR lifetimes and wrapper labels first.
+  This would reduce the manual serialization boundary; it is blocked on the
+  missing correspondence proof, not another finite identity check.
+- Can helper 450 be traced through every actual T16 hosted invocation? Start
+  with the pinned owner map and chart/route evidence. This would connect the
+  local result to physical realization; exact compiled recipes and disjoint,
+  nonempty footprints remain separate obligations.