diff --git a/research/hyperplane-end-lean/.gitignore b/research/hyperplane-end-lean/.gitignore
new file mode 100644
index 0000000000..2b00952692
--- /dev/null
+++ b/research/hyperplane-end-lean/.gitignore
@@ -0,0 +1 @@
+.lake
diff --git a/research/hyperplane-end-lean/HyperplaneEnd.lean b/research/hyperplane-end-lean/HyperplaneEnd.lean
new file mode 100644
index 0000000000..e0c9b70142
--- /dev/null
+++ b/research/hyperplane-end-lean/HyperplaneEnd.lean
@@ -0,0 +1,4 @@
+import HyperplaneEnd.Labels
+import HyperplaneEnd.Tail
+import HyperplaneEnd.Main
+import HyperplaneEnd.Multi
diff --git a/research/hyperplane-end-lean/HyperplaneEnd/Labels.lean b/research/hyperplane-end-lean/HyperplaneEnd/Labels.lean
new file mode 100644
index 0000000000..8315bdda8d
--- /dev/null
+++ b/research/hyperplane-end-lean/HyperplaneEnd/Labels.lean
@@ -0,0 +1,98 @@
+/-
+Hyperplane-ended helpers, labels: Lemma G's extended labels with an arbitrary terminal frame.
+
+Lemma G (`../e8-lemma-g-lean/PROOF.md` §1.3) reads every wrapper as a relabel by giving an
+entering helper `j` two register-specific tags with operators
+* `T_(prew,j) = R_E T_E`        (before the pre wrapper `R_E⁻¹`),
+* `T_(done,j) = L_E⁻¹ T_FULL`   (after the post wrapper `L_E⁻¹`).
+Here the terminal frame `FULL` is replaced by an arbitrary frame `U_j` (`term j`), and the
+wrappers are keyed by the pair `(E_j, U_j)`.  Nothing below names `FULL`.
+
+* `pre_recipe`, `post_recipe`   the wrappers execute `R_{E,U}⁻¹` and `L_{E,U}⁻¹`;
+* `wrapped_block`               `T_(done,j) T_(prew,j)⁻¹ = L⁻¹ T_U T_E⁻¹ R⁻¹`;
+* `factor_of_exact`             (N) `T_U T_E⁻¹ = L (C ⊗ id) R` gives Lemma A's (F);
+* `factor_iff_pre`              with an invertible residual, (F) holds iff the pre wrapper is the
+                                `(E, U)` recipe (review finding F1: `R_{E,FULL}` is wrong).
+Apache-2.0.  Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2.
+-/
+import Mathlib.LinearAlgebra.TensorProduct.Basic
+
+namespace HyperplaneEnd
+
+open TensorProduct
+
+/-- Extended labels: a frame of the word's family, or the register-specific tag of an entering
+helper before its pre wrapper (`prew`) or after its post wrapper (`done`). -/
+inductive XLab (ι Fr : Type*) where
+  | frame (F : Fr)
+  | prew (j : ι)
+  | done (j : ι)
+
+variable {K : Type*} [CommSemiring K]
+variable {M : Type*} [AddCommMonoid M] [Module K M]
+variable {ι Fr : Type*}
+
+/-- The operators of the extended labels.  `T` is the word's frame family, `ent j` and `term j`
+the entrance and terminal frames of helper `j`, `Lw E U` and `Rw E U` the serialized wrapper
+monomials of the pair `(E, U)`. -/
+def Text (T : Fr → M ≃ₗ[K] M) (ent term : ι → Fr) (Lw Rw : Fr → Fr → M ≃ₗ[K] M) :
+    XLab ι Fr → M ≃ₗ[K] M
+  | .frame F => T F
+  | .prew j => (T (ent j)).trans (Rw (ent j) (term j))
+  | .done j => (T (term j)).trans (Lw (ent j) (term j)).symm
+
+variable (T : Fr → M ≃ₗ[K] M) (ent term : ι → Fr) (Lw Rw : Fr → Fr → M ≃ₗ[K] M)
+
+/-- The pre wrapper `relabel j (prew j) (ent j)` executes `T_E T_(prew,j)⁻¹ = R_{E,U}⁻¹`. -/
+theorem pre_recipe (j : ι) (v : M) :
+    Text T ent term Lw Rw (.frame (ent j)) ((Text T ent term Lw Rw (.prew j)).symm v) =
+      (Rw (ent j) (term j)).symm v := by
+  simp [Text, LinearEquiv.symm_trans_apply]
+
+/-- The post wrapper `relabel j (term j) (done j)` executes `T_(done,j) T_U⁻¹ = L_{E,U}⁻¹`. -/
+theorem post_recipe (j : ι) (v : M) :
+    Text T ent term Lw Rw (.done j) ((Text T ent term Lw Rw (.frame (term j))).symm v) =
+      (Lw (ent j) (term j)).symm v := by
+  simp [Text]
+
+/-- The wrapped block of helper `j`: `T_(done,j) T_(prew,j)⁻¹ = L⁻¹ T_U T_E⁻¹ R⁻¹`. -/
+theorem wrapped_block (j : ι) (v : M) :
+    Text T ent term Lw Rw (.done j) ((Text T ent term Lw Rw (.prew j)).symm v) =
+      (Lw (ent j) (term j)).symm (T (term j) ((T (ent j)).symm ((Rw (ent j) (term j)).symm v))) := by
+  simp [Text, LinearEquiv.symm_trans_apply]
+
+variable {A B : Type*} [AddCommMonoid A] [Module K A] [AddCommMonoid B] [Module K B]
+
+/-- **(N) gives (F).**  If the nested-children factorization `T_U T_E⁻¹ = L (C ⊗ id) R` holds
+exactly (global phase included) for the pair `(E_j, U_j)`, the wrapped block in the extended
+labels is `C ⊗ id`: Lemma A's hypothesis (F), whatever the terminal frame `U_j` is. -/
+theorem factor_of_exact (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (ent term : ι → Fr)
+    (Lw Rw : Fr → Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (j : ι) (C : A →ₗ[K] A)
+    (hN : ∀ v, T (term j) ((T (ent j)).symm v) =
+      Lw (ent j) (term j) (C.rTensor B (Rw (ent j) (term j) v))) (v : A ⊗[K] B) :
+    Text T ent term Lw Rw (.done j) ((Text T ent term Lw Rw (.prew j)).symm v) = C.rTensor B v := by
+  rw [wrapped_block, hN]
+  simp
+
+/-- **The pre wrapper must be the `(E, U)` recipe** (review finding F1).  Suppose (N) holds for
+`(E_j, U_j)` with `L, R` and an invertible residual `C`, and the pre wrapper that actually ran
+executed `R'⁻¹`.  Then `L⁻¹ T_U T_E⁻¹ R'⁻¹ = C ⊗ id` exactly when `R' = R`.  In particular a
+pre wrapper decoded against the FULL recipe `R_{E,FULL} ≠ R_{E,U}` breaks (F). -/
+theorem factor_iff_pre (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (E U : Fr)
+    (L R R' : (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (C : A ≃ₗ[K] A)
+    (hN : ∀ v, T U ((T E).symm v) = L ((C : A →ₗ[K] A).rTensor B (R v))) :
+    (∀ v, L.symm (T U ((T E).symm (R'.symm v))) = (C : A →ₗ[K] A).rTensor B v) ↔ R' = R := by
+  constructor
+  · intro h
+    have hinj : Function.Injective ((C : A →ₗ[K] A).rTensor B) := by
+      rw [← LinearEquiv.coe_rTensor]
+      exact (LinearEquiv.rTensor B C).injective
+    ext w
+    have := h (R' w)
+    rw [LinearEquiv.symm_apply_apply, hN, LinearEquiv.symm_apply_apply] at this
+    exact (hinj this).symm
+  · rintro rfl v
+    rw [hN]
+    simp
+
+end HyperplaneEnd
diff --git a/research/hyperplane-end-lean/HyperplaneEnd/Main.lean b/research/hyperplane-end-lean/HyperplaneEnd/Main.lean
new file mode 100644
index 0000000000..88fcee5376
--- /dev/null
+++ b/research/hyperplane-end-lean/HyperplaneEnd/Main.lean
@@ -0,0 +1,125 @@
+/-
+Hyperplane-ended helpers, main theorems: Lemma A with an arbitrary terminal frame.
+
+Lemma A (`../e8-lemma-a-lean`) is stated for any label family; its hypothesis (F) is
+`T_{λ¹_j} T_{λ⁰_j}⁻¹ = C ⊗ id` on Lemma G's extended labels.  Instantiating the labels with
+`Text` (terminal frame `U_j` arbitrary, wrappers keyed by `(E_j, U_j)`) and discharging (F) by
+the exact factorization (N) `T_U T_E⁻¹ = L (C ⊗ id) R` gives:
+
+* `hpe_block`     the helper's register ends as `(C ⊗ id) h_j` (local run);
+* `hpe_family`    realized on families: the helper's family ends as `χ⁻¹ (C ⊗ id) χ` of itself;
+* `hpe_streams`   the same on physical streams with disjoint footprints (Lemma A's main form);
+* `hpe_word`      the same for the concrete HPE word `a ++ tail ++ b ++ [post]` (Tail.lean);
+* `hyperplane_width`  on frames of `F₂⁹`: `E ≤ U`, `dim E = 1`, `dim U = 8` give width
+                  `dim U - dim E = 7`, `9 - 7 = 2` spectators, and `U ≠ FULL`.
+The FULL-ended helpers of #484 are the instance `term j = ⊤`.
+Apache-2.0.  Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2.
+-/
+import HyperplaneEnd.Tail
+import LemmaA
+import LemmaG.Frames
+
+namespace HyperplaneEnd
+
+open TensorProduct LemmaG LemmaG.Stream LemmaA
+
+variable {K : Type*} [CommSemiring K]
+variable {A B : Type*} [AddCommMonoid A] [Module K A] [AddCommMonoid B] [Module K B]
+variable {ι Fr : Type*} [DecidableEq ι] [Fintype ι]
+
+/-- **The HPE helper block.**  A well-labelled invocation with exact recipes in the extended
+labels `Text`, a helper `j` with a unit row that starts at `(prew, j)` and ends at `(done, j)`, and
+the exact factorization (N) for its pair `(E_j, U_j)`: register `j` ends as `(C ⊗ id) h_j`. -/
+theorem hpe_block (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (ent term : ι → Fr)
+    (Lw Rw : Fr → Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B))
+    (rec : XLab ι Fr → XLab ι Fr → A ⊗[K] B → A ⊗[K] B) (es : List (Event ι (XLab ι Fr) K))
+    (l : ι → XLab ι Fr) (h : ι → A ⊗[K] B) (hrec : RecipesExact (Text T ent term Lw Rw) rec es)
+    (hw : WellLabelled es l) (j : ι) (hS : ∀ s, S es j s = if s = j then 1 else 0)
+    (hstart : l j = .prew j) (hend : labRun es l j = .done j) (C : A →ₗ[K] A)
+    (hN : ∀ v, T (term j) ((T (ent j)).symm v) =
+      Lw (ent j) (term j) (C.rTensor B (Rw (ent j) (term j) v))) :
+    physRun rec es h j = C.rTensor B (h j) :=
+  helper_block (Text T ent term Lw Rw) rec es l h hrec hw j hS C
+    (fun v => by rw [hstart, hend]; exact factor_of_exact T ent term Lw Rw j C hN v)
+
+/-- **Lemma A for a hyperplane-ended helper, on families.** -/
+theorem hpe_family {Φ W : Type*} [DecidableEq Φ] [AddCommMonoid W] [Module K W]
+    (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (ent term : ι → Fr)
+    (Lw Rw : Fr → Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (σ : Hosting ι Φ K W (A ⊗[K] B))
+    (hinj : Function.Injective σ.own) (rec : XLab ι Fr → XLab ι Fr → A ⊗[K] B → A ⊗[K] B)
+    (es : List (Event ι (XLab ι Fr) K)) (l : ι → XLab ι Fr) (y : Φ → W)
+    (hrec : RecipesExact (Text T ent term Lw Rw) rec es) (hw : WellLabelled es l) (j : ι)
+    (hS : ∀ s, S es j s = if s = j then 1 else 0)
+    (hstart : l j = .prew j) (hend : labRun es l j = .done j) (C : A →ₗ[K] A)
+    (hN : ∀ v, T (term j) ((T (ent j)).symm v) =
+      Lw (ent j) (term j) (C.rTensor B (Rw (ent j) (term j) v))) :
+    realizeRun σ rec es y (σ.own j) = (σ.chart j).symm (C.rTensor B (σ.chart j (y (σ.own j)))) :=
+  lemmaA_family (Text T ent term Lw Rw) σ hinj rec es l y hrec hw j hS C
+    (fun v => by rw [hstart, hend]; exact factor_of_exact T ent term Lw Rw j C hN v)
+
+/-- **Lemma A for a hyperplane-ended helper, on streams.**  Same hypotheses as
+`LemmaA.lemmaA_streams`, with (F) replaced by the start/end tags and (N) for the pair
+`(E_j, U_j)`.  The terminal frame `term j` is arbitrary; nothing requires it to be FULL. -/
+theorem hpe_streams {Fam G Cc W : Type*} [DecidableEq Fam] [Group G] [DecidableEq G]
+    [AddCommMonoid W] [Module K W]
+    (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (ent term : ι → Fr)
+    (Lw Rw : Fr → Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B))
+    (fam : ι → Fam) (σ : ι → G) (d : G)
+    (fp : G → Set Cc) (hne : ∀ r, (fp (σ r)).Nonempty)
+    (hdis : ∀ r r', r ≠ r' → fam r = fam r' → Disjoint (fp (σ r)) (fp (σ r')))
+    (chart : ι → W ≃ₗ[K] (A ⊗[K] B)) (rec : XLab ι Fr → XLab ι Fr → A ⊗[K] B → A ⊗[K] B)
+    (es : List (Event ι (XLab ι Fr) K)) (l : ι → XLab ι Fr) (y : Fam × G → W)
+    (hrec : RecipesExact (Text T ent term Lw Rw) rec es) (hw : WellLabelled es l) (j : ι)
+    (hS : ∀ s, S es j s = if s = j then 1 else 0)
+    (hstart : l j = .prew j) (hend : labRun es l j = .done j) (C : A →ₗ[K] A)
+    (hN : ∀ v, T (term j) ((T (ent j)).symm v) =
+      Lw (ent j) (term j) (C.rTensor B (Rw (ent j) (term j) v))) :
+    realizeRun ⟨streamOwner fam σ d, chart⟩ rec es y (streamOwner fam σ d j) =
+      (chart j).symm (C.rTensor B (chart j (y (streamOwner fam σ d j)))) :=
+  lemmaA_streams (Text T ent term Lw Rw) fam σ d fp hne hdis chart rec es l y hrec hw j hS C
+    (fun v => by rw [hstart, hend]; exact factor_of_exact T ent term Lw Rw j C hN v)
+
+/-- **The HPE word.**  For the word `a ++ tail ++ b ++ [post]` of `hpe_labels` (the helper `h`
+starts at `(prew, h)`, its single cleanup gate runs at `U = term h` in `cleanup_tail`, the
+remaining cleanup `b` never relabels it, the post wrapper names `U`), with exact recipes, a unit
+row and (N) for `(ent h, term h)`, the helper's stream ends as `χ⁻¹ (C ⊗ id) χ` of itself. -/
+theorem hpe_word {Fam G Cc W : Type*} [DecidableEq Fam] [Group G] [DecidableEq G]
+    [AddCommMonoid W] [Module K W]
+    (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (ent term : ι → Fr)
+    (Lw Rw : Fr → Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B))
+    (fam : ι → Fam) (σ : ι → G) (d : G)
+    (fp : G → Set Cc) (hne : ∀ r, (fp (σ r)).Nonempty)
+    (hdis : ∀ r r', r ≠ r' → fam r = fam r' → Disjoint (fp (σ r)) (fp (σ r')))
+    (chart : ι → W ≃ₗ[K] (A ⊗[K] B)) (rec : XLab ι Fr → XLab ι Fr → A ⊗[K] B → A ⊗[K] B)
+    (h p : ι) (hp : h ≠ p) (Ah Ap : Fr) (q : K) (l : ι → XLab ι Fr)
+    (a b : List (Event ι (XLab ι Fr) K)) (y : Fam × G → W)
+    (ha : WellLabelled a l) (lh : labRun a l h = .frame Ah) (lp : labRun a l p = .frame Ap)
+    (hb : WellLabelled b (labRun (a ++ tail h p Ah Ap (term h) q) l))
+    (hmv : ∀ e ∈ b, ¬ e.moves h)
+    (hrec : RecipesExact (Text T ent term Lw Rw) rec
+      (a ++ tail h p Ah Ap (term h) q ++ b ++ [.relabel h (.frame (term h)) (.done h)]))
+    (hS : ∀ s, S (a ++ tail h p Ah Ap (term h) q ++ b ++ [.relabel h (.frame (term h)) (.done h)])
+      h s = if s = h then 1 else 0)
+    (hstart : l h = .prew h) (C : A →ₗ[K] A)
+    (hN : ∀ v, T (term h) ((T (ent h)).symm v) =
+      Lw (ent h) (term h) (C.rTensor B (Rw (ent h) (term h) v))) :
+    realizeRun ⟨streamOwner fam σ d, chart⟩ rec
+        (a ++ tail h p Ah Ap (term h) q ++ b ++ [.relabel h (.frame (term h)) (.done h)]) y
+        (streamOwner fam σ d h) =
+      (chart h).symm (C.rTensor B (chart h (y (streamOwner fam σ d h)))) :=
+  let hl := hpe_labels h p hp Ah Ap (term h) q l a b ha lh lp hb hmv
+  hpe_streams T ent term Lw Rw fam σ d fp hne hdis chart rec _ l y hrec hl.1 h hS hstart hl.2 C hN
+
+/-- **Width and spectators of a hyperplane end** (frames of `F₂⁹`).  For an entrance `E` of
+dimension 1 inside a hyperplane `U` (dimension 8), the residual width is `dim U - dim E = 7`,
+the hosted chart has `9 - 7 = 2` spectators, and `U` is not the full frame. -/
+theorem hyperplane_width (E U : Frame) (hEU : E ≤ U) (hE : frameRank E = 1) (hU : frameRank U = 8) :
+    frameRank U - frameRank E = 7 ∧ 9 - (frameRank U - frameRank E) = 2 ∧ U ≠ ⊤ ∧
+      frameRank E ≤ frameRank U := by
+  refine ⟨by omega, by omega, ?_, frameRank_strictMono.monotone hEU⟩
+  rintro rfl
+  have : frameRank (⊤ : Frame) = 9 := by
+    simp [frameRank, finrank_top, Module.finrank_fin_fun]
+  omega
+
+end HyperplaneEnd
diff --git a/research/hyperplane-end-lean/HyperplaneEnd/Multi.lean b/research/hyperplane-end-lean/HyperplaneEnd/Multi.lean
new file mode 100644
index 0000000000..7b92352426
--- /dev/null
+++ b/research/hyperplane-end-lean/HyperplaneEnd/Multi.lean
@@ -0,0 +1,309 @@
+/-
+Hyperplane-ended helpers with a MULTI-GATE `cleanup_tail`, several helpers at once, and the cold
+instance `E = ⊥`.
+
+`Tail.lean` treats one helper with one cleanup gate `h -= p`.  Here the `cleanup_tail` is modelled
+as an arbitrary list of gates `t += q • s` (or `t *= q`), each at its own frame `F`: every operand not
+already at `F` climbs to `F` (one relabel), then the gate runs.  The shipped hyperplane-ended helpers
+of #591/#592 are the one-gate case; multi-gate and `scale` tails are not checked here against
+emitted words.  A helper `j` may be touched by any number of tail gates (as target or as partner); what
+matters is the LAST tail gate touching it, whose frame must be `term j`.  The remaining cleanup `b`
+never relabels a hyperplane-ended helper, and the post wrappers `relabel j (term j) (done j)` close
+every such helper.
+
+* `mtail_wellLabelled`   the tail is always well labelled: every gate runs with its operands at
+                         its frame (G0 for the partners), whatever the gate list;
+* `labRun_mtail`         after the tail a register sits at the frame of the last gate touching it
+                         (`lastFrame`), and is untouched otherwise;
+* `hpe_labels_multi`     the word `a ++ mtail ++ b ++ posts` is well labelled and every helper of
+                         the list ends at `(done, j)`;
+* `hpe_labels_tail`      the single-gate word of `Tail.lean` is the one-gate instance when both
+                         operands start away from `U`;
+* `hpe_word_multi`       Lemma A on streams for every such helper (per-helper `C j` and (N));
+* `exact_cold`, `cold_hyperplane_width`   the cold specialisation: given `T_E = id` (true of the
+                         canonical frame of `E = ⊥`, an input checked outside Lean), (N) reduces to
+                         `T_U = L (C ⊗ id) R`; `⊥ ≤ U` with `dim U = 8` gives width 8 (rank arithmetic).
+                         #593's `hpe_word` already takes an arbitrary entrance frame.
+Apache-2.0.
+-/
+import HyperplaneEnd.Main
+
+namespace HyperplaneEnd
+
+open TensorProduct LemmaG LemmaG.Stream LemmaA
+
+deriving instance DecidableEq for XLab
+
+/-- A gate of the `cleanup_tail`: `t += q • s` or `t *= q`, run at frame `F`. -/
+inductive TGate (ι Fr K : Type*) where
+  | add (t s : ι) (F : Fr) (q : K)
+  | scale (t : ι) (F : Fr) (q : K)
+
+namespace TGate
+
+variable {ι Fr K : Type*}
+
+/-- The frame the gate runs at. -/
+def frame : TGate ι Fr K → Fr
+  | add _ _ F _ => F
+  | scale _ F _ => F
+
+/-- The registers the gate touches (its operands). -/
+def regs : TGate ι Fr K → List ι
+  | add t s _ _ => [t, s]
+  | scale t _ _ => [t]
+
+end TGate
+
+section Labels
+
+variable {ι Fr K : Type*} [DecidableEq ι] [DecidableEq Fr]
+
+/-- The climb of register `r` to frame `F` in this model: nothing if `r` is already
+at `F`, else one relabel from its current label. -/
+def climb (r : ι) (F : Fr) (l : ι → XLab ι Fr) : List (Event ι (XLab ι Fr) K) :=
+  if l r = .frame F then [] else [.relabel r (l r) (.frame F)]
+
+/-- One tail gate as emitted: the climbs of its operands to its frame, then the scalar gate. -/
+def block (g : TGate ι Fr K) (l : ι → XLab ι Fr) : List (Event ι (XLab ι Fr) K) :=
+  match g with
+  | .add t s F q => climb t F l ++ climb s F (labRun (climb (K := K) t F l) l) ++ [.add t s q]
+  | .scale t F q => climb t F l ++ [.scale t q]
+
+/-- The emitted `cleanup_tail` of a gate list, threading the labels. -/
+def mtail : List (TGate ι Fr K) → (ι → XLab ι Fr) → List (Event ι (XLab ι Fr) K)
+  | [], _ => []
+  | g :: gs, l => block g l ++ mtail gs (labRun (block g l) l)
+
+/-- The frame of the last gate of the list touching `r` (`none` if no gate touches it). -/
+def lastFrame (r : ι) : List (TGate ι Fr K) → Option Fr
+  | [] => none
+  | g :: gs =>
+    match lastFrame r gs with
+    | some F => some F
+    | none => if r ∈ g.regs then some g.frame else none
+
+/-- The post wrappers `relabel j (term j) (done j)` of a list of helpers. -/
+def posts (term : ι → Fr) (hs : List ι) : List (Event ι (XLab ι Fr) K) :=
+  hs.map fun j => .relabel j (.frame (term j)) (.done j)
+
+theorem labRun_climb (r : ι) (F : Fr) (l : ι → XLab ι Fr) :
+    labRun (climb (K := K) r F l) l = Function.update l r (.frame F) := by
+  unfold climb
+  split_ifs with h
+  · simp only [labRun]
+    rw [← h, Function.update_eq_self]
+  · simp [labRun, Event.lab]
+
+theorem wellLabelled_climb (r : ι) (F : Fr) (l : ι → XLab ι Fr) :
+    WellLabelled (climb (K := K) r F l) l := by
+  unfold climb
+  split_ifs
+  · trivial
+  · simp [WellLabelled, Event.Admissible]
+
+theorem labRun_block (g : TGate ι Fr K) (l : ι → XLab ι Fr) (i : ι) :
+    labRun (block g l) l i = if i ∈ g.regs then .frame g.frame else l i := by
+  cases g with
+  | add t s F q =>
+    simp only [block]
+    rw [labRun_append, labRun_append, labRun_climb, labRun_climb]
+    by_cases hs : i = s
+    · subst hs; simp [labRun, Event.lab, TGate.regs, TGate.frame]
+    · by_cases ht : i = t
+      · subst ht; simp [labRun, Event.lab, TGate.regs, TGate.frame, Function.update_of_ne hs]
+      · simp [labRun, Event.lab, TGate.regs, Function.update_of_ne hs, Function.update_of_ne ht, hs, ht]
+  | scale t F q =>
+    simp only [block]
+    rw [labRun_append, labRun_climb]
+    by_cases ht : i = t
+    · subst ht; simp [labRun, Event.lab, TGate.regs, TGate.frame]
+    · simp [labRun, Event.lab, TGate.regs, Function.update_of_ne ht, ht]
+
+/-- Every emitted tail gate is admissible: both operands are at the gate's frame (G0). -/
+theorem wellLabelled_block (g : TGate ι Fr K) (l : ι → XLab ι Fr) :
+    WellLabelled (block g l) l := by
+  cases g with
+  | add t s F q =>
+    simp only [block]
+    have h1 := labRun_climb (K := K) t F l
+    rw [wellLabelled_append, wellLabelled_append, labRun_append, h1, labRun_climb]
+    refine ⟨⟨wellLabelled_climb _ _ _, wellLabelled_climb _ _ _⟩, ?_⟩
+    simp only [WellLabelled, Event.Admissible, and_true]
+    by_cases hts : t = s
+    · subst hts; rfl
+    · rw [Function.update_of_ne hts, Function.update_self, Function.update_self]
+  | scale t F q =>
+    simp only [block]
+    rw [wellLabelled_append]
+    exact ⟨wellLabelled_climb _ _ _, by simp [WellLabelled, Event.Admissible]⟩
+
+/-- The emitted tail is well labelled for ANY gate list and any starting labels. -/
+theorem mtail_wellLabelled : ∀ (gs : List (TGate ι Fr K)) (l : ι → XLab ι Fr),
+    WellLabelled (mtail gs l) l
+  | [], _ => trivial
+  | g :: gs, l => by
+    simp only [mtail]
+    rw [wellLabelled_append]
+    exact ⟨wellLabelled_block g l, mtail_wellLabelled gs _⟩
+
+/-- After the tail, a register sits at the frame of the last tail gate touching it; a register
+touched by no tail gate keeps its label. -/
+theorem labRun_mtail : ∀ (gs : List (TGate ι Fr K)) (l : ι → XLab ι Fr) (i : ι),
+    labRun (mtail gs l) l i = ((lastFrame i gs).map XLab.frame).getD (l i)
+  | [], _, _ => rfl
+  | g :: gs, l, i => by
+    simp only [mtail, lastFrame]
+    rw [labRun_append, labRun_mtail gs _ i, labRun_block]
+    cases lastFrame i gs with
+    | some F => rfl
+    | none => by_cases hi : i ∈ g.regs <;> simp [hi]
+
+theorem labRun_mtail_last (gs : List (TGate ι Fr K)) (l : ι → XLab ι Fr) (i : ι) (U : Fr)
+    (h : lastFrame i gs = some U) : labRun (mtail gs l) l i = .frame U := by
+  rw [labRun_mtail, h]; rfl
+
+omit [DecidableEq Fr] in
+theorem posts_spec (term : ι → Fr) : ∀ (hs : List ι) (l : ι → XLab ι Fr), hs.Nodup →
+    (∀ j ∈ hs, l j = .frame (term j)) →
+    WellLabelled (posts (K := K) term hs) l ∧
+      ∀ i, labRun (posts (K := K) term hs) l i = if i ∈ hs then .done i else l i
+  | [], _, _, _ => ⟨trivial, fun _ => by simp [posts, labRun]⟩
+  | j :: hs, l, hnd, hl => by
+    have hj : j ∉ hs := (List.nodup_cons.1 hnd).1
+    have hnd' : hs.Nodup := (List.nodup_cons.1 hnd).2
+    have hl' : ∀ j' ∈ hs, Function.update l j (.done j) j' = .frame (term j') := by
+      intro j' hj'
+      have hne : j' ≠ j := fun h => hj (h ▸ hj')
+      rw [Function.update_of_ne hne]; exact hl j' (List.mem_cons_of_mem _ hj')
+    obtain ⟨ih1, ih2⟩ := posts_spec term hs (Function.update l j (.done j)) hnd' hl'
+    refine ⟨⟨hl j List.mem_cons_self, ih1⟩, fun i => ?_⟩
+    change labRun (posts (K := K) term hs) (Function.update l j (.done j)) i = _
+    rw [ih2 i]
+    by_cases hij : i = j
+    · subst hij; simp [hj]
+    · by_cases hi : i ∈ hs
+      · simp [hi]
+      · simp [hi, hij, Function.update_of_ne hij]
+
+/-- **The terminal labels of hyperplane-ended helpers with a multi-gate tail.**  Let the word be
+`a ++ mtail gs ++ b ++ posts term hs`, where `a` is well labelled, every helper `j` of the
+(duplicate-free) list `hs` has its LAST tail gate at frame `term j` (any number of earlier tail
+gates, as target or partner, at any frames), and the remaining cleanup `b` is well labelled and
+never relabels a helper of `hs`.  Then the whole word is well labelled and every `j ∈ hs` ends at
+`(done, j)`. -/
+theorem hpe_labels_multi (term : ι → Fr) (hs : List ι) (hnd : hs.Nodup) (l : ι → XLab ι Fr)
+    (a : List (Event ι (XLab ι Fr) K)) (gs : List (TGate ι Fr K)) (b : List (Event ι (XLab ι Fr) K))
+    (ha : WellLabelled a l) (hlast : ∀ j ∈ hs, lastFrame j gs = some (term j))
+    (hb : WellLabelled b (labRun (a ++ mtail gs (labRun a l)) l))
+    (hmv : ∀ e ∈ b, ∀ j ∈ hs, ¬ e.moves j) :
+    WellLabelled (a ++ mtail gs (labRun a l) ++ b ++ posts term hs) l ∧
+      ∀ j ∈ hs, labRun (a ++ mtail gs (labRun a l) ++ b ++ posts term hs) l j = .done j := by
+  set w := a ++ mtail gs (labRun a l) ++ b
+  have hU : ∀ j ∈ hs, labRun w l j = .frame (term j) := by
+    intro j hj
+    simp only [w]
+    rw [labRun_append, labRun_untouched b _ j (fun e he => hmv e he j hj), labRun_append,
+      labRun_mtail_last gs _ j (term j) (hlast j hj)]
+  have hwl : WellLabelled w l := by
+    simp only [w]
+    rw [wellLabelled_append, wellLabelled_append]
+    exact ⟨⟨ha, mtail_wellLabelled gs _⟩, hb⟩
+  obtain ⟨hp1, hp2⟩ := posts_spec (K := K) term hs (labRun w l) hnd hU
+  refine ⟨(wellLabelled_append _ _ _).2 ⟨hwl, hp1⟩, fun j hj => ?_⟩
+  rw [labRun_append, hp2 j, if_pos hj]
+
+/-- The shipped single-gate tail (`Tail.tail`) is the one-gate `mtail` when both operands climb. -/
+theorem tail_eq_mtail (h p : ι) (hp : h ≠ p) (Ah Ap U : Fr) (q : K) (l : ι → XLab ι Fr)
+    (lh : l h = .frame Ah) (lp : l p = .frame Ap) (hAh : Ah ≠ U) (hAp : Ap ≠ U) :
+    mtail [TGate.add h p U q] l = tail h p Ah Ap U q := by
+  have c1 : climb (K := K) h U l = [.relabel h (.frame Ah) (.frame U)] := by
+    simp [climb, lh, hAh]
+  have c2 : climb (K := K) p U (labRun (climb (K := K) h U l) l) =
+      [.relabel p (.frame Ap) (.frame U)] := by
+    rw [labRun_climb]
+    simp [climb, Function.update_of_ne (Ne.symm hp), lp, hAp]
+  simp only [mtail, block, List.append_nil]
+  rw [c2, c1]
+  rfl
+
+/-- **The single-gate word is the one-gate instance** of `hpe_labels_multi` (so the shipped
+`hpe_labels` is a special case). -/
+theorem hpe_labels_tail (h p : ι) (hp : h ≠ p) (Ah Ap U : Fr) (q : K) (l : ι → XLab ι Fr)
+    (a b : List (Event ι (XLab ι Fr) K))
+    (ha : WellLabelled a l) (lh : labRun a l h = .frame Ah) (lp : labRun a l p = .frame Ap)
+    (hAh : Ah ≠ U) (hAp : Ap ≠ U)
+    (hb : WellLabelled b (labRun (a ++ tail h p Ah Ap U q) l))
+    (hmv : ∀ e ∈ b, ¬ e.moves h) :
+    WellLabelled (a ++ tail h p Ah Ap U q ++ b ++ [.relabel h (.frame U) (.done h)]) l ∧
+      labRun (a ++ tail h p Ah Ap U q ++ b ++ [.relabel h (.frame U) (.done h)]) l h = .done h := by
+  have ht := tail_eq_mtail (K := K) h p hp Ah Ap U q (labRun a l) lh lp hAh hAp
+  have hl : lastFrame h [TGate.add h p U q] = some U := by
+    simp [lastFrame, TGate.regs, TGate.frame]
+  rw [← ht] at hb ⊢
+  have := hpe_labels_multi (fun _ => U) [h] (List.nodup_singleton h) l a [TGate.add h p U q] b ha
+    (by simpa using hl) hb (by simpa using hmv)
+  exact ⟨by simpa [posts] using this.1, by simpa [posts] using this.2 h List.mem_cons_self⟩
+
+end Labels
+
+/-- **Lemma A for every hyperplane-ended helper of a multi-gate word** (streams form).  Each helper
+`j ∈ hs` starts at `(prew, j)`, has a unit row, and (N) for its pair `(ent j, term j)` with its own
+`C j`; the word is `a ++ mtail gs ++ b ++ posts term hs` as in `hpe_labels_multi`.  Then each
+helper's stream ends as `χ⁻¹ (C j ⊗ id) χ` of itself.  Nothing restricts `ent j` (cold: `ent j = ⊥`). -/
+theorem hpe_word_multi {ι Fr K : Type*} [DecidableEq ι] [DecidableEq Fr] [CommSemiring K]
+    {A B : Type*} [AddCommMonoid A] [Module K A] [AddCommMonoid B] [Module K B] [Fintype ι]
+    {Fam G Cc W : Type*} [DecidableEq Fam] [Group G] [DecidableEq G]
+    [AddCommMonoid W] [Module K W]
+    (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (ent term : ι → Fr)
+    (Lw Rw : Fr → Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B))
+    (fam : ι → Fam) (σ : ι → G) (d : G)
+    (fp : G → Set Cc) (hne : ∀ r, (fp (σ r)).Nonempty)
+    (hdis : ∀ r r', r ≠ r' → fam r = fam r' → Disjoint (fp (σ r)) (fp (σ r')))
+    (chart : ι → W ≃ₗ[K] (A ⊗[K] B)) (rec : XLab ι Fr → XLab ι Fr → A ⊗[K] B → A ⊗[K] B)
+    (hs : List ι) (hnd : hs.Nodup) (l : ι → XLab ι Fr)
+    (a : List (Event ι (XLab ι Fr) K)) (gs : List (TGate ι Fr K)) (b : List (Event ι (XLab ι Fr) K))
+    (y : Fam × G → W)
+    (ha : WellLabelled a l) (hlast : ∀ j ∈ hs, lastFrame j gs = some (term j))
+    (hb : WellLabelled b (labRun (a ++ mtail gs (labRun a l)) l))
+    (hmv : ∀ e ∈ b, ∀ j ∈ hs, ¬ e.moves j)
+    (hrec : RecipesExact (Text T ent term Lw Rw) rec (a ++ mtail gs (labRun a l) ++ b ++ posts term hs))
+    (hS : ∀ j ∈ hs, ∀ s, S (a ++ mtail gs (labRun a l) ++ b ++ posts term hs) j s =
+      if s = j then 1 else 0)
+    (hstart : ∀ j ∈ hs, l j = .prew j) (C : ι → A →ₗ[K] A)
+    (hN : ∀ j ∈ hs, ∀ v, T (term j) ((T (ent j)).symm v) =
+      Lw (ent j) (term j) ((C j).rTensor B (Rw (ent j) (term j) v))) :
+    ∀ j ∈ hs, realizeRun ⟨streamOwner fam σ d, chart⟩ rec
+        (a ++ mtail gs (labRun a l) ++ b ++ posts term hs) y (streamOwner fam σ d j) =
+      (chart j).symm ((C j).rTensor B (chart j (y (streamOwner fam σ d j)))) := by
+  intro j hj
+  have hl := hpe_labels_multi term hs hnd l a gs b ha hlast hb hmv
+  exact hpe_streams T ent term Lw Rw fam σ d fp hne hdis chart rec _ l y hrec hl.1 j (hS j hj)
+    (hstart j hj) (hl.2 j hj) (C j) (hN j hj)
+
+
+/-! ### The cold instance `E = ⊥` -/
+
+/-- **(N) for a cold helper.**  If the entrance operator is the identity (`T_⊥ = id`, as
+`clifford_exact.canonical_frame(n, ())` is) then (N) for `(⊥, U)` is just a monomial factorization
+of `T_U` itself; e.g. `T_U = K⁻¹ (C ⊗ id) K`, which is how `canonical_frame` DEFINES `T_U`. -/
+theorem exact_cold {K : Type*} [CommSemiring K] {A B : Type*} [AddCommMonoid A] [Module K A]
+    [AddCommMonoid B] [Module K B] {Fr : Type*} (T : Fr → (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (E U : Fr)
+    (L R : (A ⊗[K] B) ≃ₗ[K] (A ⊗[K] B)) (C : A →ₗ[K] A)
+    (hE : ∀ v, (T E).symm v = v) (hU : ∀ v, T U v = L (C.rTensor B (R v))) :
+    ∀ v, T U ((T E).symm v) = L (C.rTensor B (R v)) := by
+  intro v; rw [hE, hU]
+
+/-- **Width of a cold hyperplane end** (frames of `F₂⁹`): `E = ⊥ ≤ U`, `dim U = 8` give width
+`dim U - dim ⊥ = 8`, one spectator, and `U ≠ FULL`. -/
+theorem cold_hyperplane_width (U : Frame) (hU : frameRank U = 8) :
+    frameRank U - frameRank ⊥ = 8 ∧ 9 - (frameRank U - frameRank ⊥) = 1 ∧ U ≠ ⊤ ∧
+      (⊥ : Frame) ≤ U := by
+  have h0 : frameRank (⊥ : Frame) = 0 := by simp [frameRank]
+  refine ⟨by omega, by omega, ?_, bot_le⟩
+  rintro rfl
+  have : frameRank (⊤ : Frame) = 9 := by
+    simp [frameRank, finrank_top, Module.finrank_fin_fun]
+  omega
+
+end HyperplaneEnd
diff --git a/research/hyperplane-end-lean/HyperplaneEnd/Tail.lean b/research/hyperplane-end-lean/HyperplaneEnd/Tail.lean
new file mode 100644
index 0000000000..11a43b6504
--- /dev/null
+++ b/research/hyperplane-end-lean/HyperplaneEnd/Tail.lean
@@ -0,0 +1,75 @@
+/-
+Hyperplane-ended helpers, the word: the `cleanup_tail` segment and the helper's terminal label.
+
+In the HPE word, helper `h` and its partner `p` climb to the join `U` of their frames, the single
+cleanup gate `h -= p` runs there (both operands at `U`: clause G0), the remaining cleanup never
+moves `h`, and the post wrapper takes `h` from `U` to `(done, h)`.
+
+* `tail_labels`        the tail is well labelled and ends with `h` and `p` both at `U`;
+* `hpe_labels`         the whole word `a ++ tail ++ b ++ [post wrapper]` is well labelled and the
+                       helper's terminal extended label is `(done, h)`;
+* `residual_block`     the unwrapped helper block of a unit row is `T_U T_E⁻¹` (Lemma G, (C)).
+Apache-2.0.  Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2.
+-/
+import HyperplaneEnd.Labels
+import LemmaG.Stream
+
+namespace HyperplaneEnd
+
+open LemmaG LemmaG.Stream
+
+variable {ι Fr K : Type*} [DecidableEq ι]
+
+/-- The `cleanup_tail` segment of one HPE helper `h` with partner `p`: both climb to `U`, then
+the gate `h += q • p` (in the word `q = -1`) runs at `U`. -/
+def tail (h p : ι) (Ah Ap U : Fr) (q : K) : List (Event ι (XLab ι Fr) K) :=
+  [.relabel h (.frame Ah) (.frame U), .relabel p (.frame Ap) (.frame U), .add h p q]
+
+/-- The tail is well labelled (the gate runs with both operands at `U`) and leaves both
+registers at `U`; every other register keeps its label. -/
+theorem tail_labels (h p : ι) (hp : h ≠ p) (Ah Ap U : Fr) (q : K) (l : ι → XLab ι Fr)
+    (lh : l h = .frame Ah) (lp : l p = .frame Ap) :
+    WellLabelled (tail h p Ah Ap U q) l ∧
+      labRun (tail h p Ah Ap U q) l =
+        Function.update (Function.update l h (.frame U)) p (.frame U) := by
+  refine ⟨?_, rfl⟩
+  simp [tail, WellLabelled, Event.Admissible, Event.lab, Function.update_apply, lh, lp, hp,
+    Ne.symm hp]
+
+/-- **The terminal label of an HPE helper.**  Let the word be `a ++ tail ++ b ++ [post]`, where
+`a` brings `h` and `p` to `A_h` and `A_p`, `b` (the remaining FULL cleanup) never relabels `h`,
+and `post` is the post wrapper `relabel h U (done h)`.  If `a` and `b` are well labelled, the whole
+word is well labelled and `h` ends at `(done, h)`: the post wrapper is admissible because `h`
+is still at `U`. -/
+theorem hpe_labels (h p : ι) (hp : h ≠ p) (Ah Ap U : Fr) (q : K) (l : ι → XLab ι Fr)
+    (a b : List (Event ι (XLab ι Fr) K))
+    (ha : WellLabelled a l) (lh : labRun a l h = .frame Ah) (lp : labRun a l p = .frame Ap)
+    (hb : WellLabelled b (labRun (a ++ tail h p Ah Ap U q) l))
+    (hmv : ∀ e ∈ b, ¬ e.moves h) :
+    WellLabelled (a ++ tail h p Ah Ap U q ++ b ++ [.relabel h (.frame U) (.done h)]) l ∧
+      labRun (a ++ tail h p Ah Ap U q ++ b ++ [.relabel h (.frame U) (.done h)]) l h = .done h := by
+  obtain ⟨ht, hlt⟩ := tail_labels h p hp Ah Ap U q (labRun a l) lh lp
+  have hU : labRun (a ++ tail h p Ah Ap U q ++ b) l h = .frame U := by
+    rw [labRun_append, labRun_untouched b _ h hmv, labRun_append, hlt]
+    simp [Function.update_apply, hp]
+  have hat : WellLabelled (a ++ tail h p Ah Ap U q) l := (wellLabelled_append _ _ _).2 ⟨ha, ht⟩
+  have hatb : WellLabelled (a ++ tail h p Ah Ap U q ++ b) l :=
+    (wellLabelled_append _ _ _).2 ⟨hat, hb⟩
+  refine ⟨(wellLabelled_append _ _ _).2 ⟨hatb, ?_⟩, ?_⟩
+  · simp only [WellLabelled, Event.Admissible, and_true]
+    exact hU
+  · rw [labRun_append]
+    simp [labRun, Event.lab]
+
+variable [Semiring K] {M : Type*} [AddCommMonoid M] [Module K M] [Fintype ι]
+
+/-- **(C) for a hyperplane end.**  In frame labels (no wrappers), a helper with a unit row whose
+label runs from `E` to `U` ends as `T_U T_E⁻¹` of its own input, for any frame `U`. -/
+theorem residual_block (T : Fr → M ≃ₗ[K] M) (rec : Fr → Fr → M → M) (es : List (Event ι Fr K))
+    (l : ι → Fr) (x : ι → M) (hrec : RecipesExact T rec es) (hw : WellLabelled es l) (j : ι)
+    (hS : ∀ s, S es j s = if s = j then 1 else 0) (E U : Fr) (hE : l j = E)
+    (hU : labRun es l j = U) :
+    physRun rec es x j = T U ((T E).symm (x j)) := by
+  rw [row_unit T rec es l x hrec hw j hS, hE, hU]
+
+end HyperplaneEnd
diff --git a/research/hyperplane-end-lean/LICENSE b/research/hyperplane-end-lean/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/hyperplane-end-lean/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/research/hyperplane-end-lean/NOTICE.md b/research/hyperplane-end-lean/NOTICE.md
new file mode 100644
index 0000000000..573f3b8022
--- /dev/null
+++ b/research/hyperplane-end-lean/NOTICE.md
@@ -0,0 +1,13 @@
+Apache-2.0 (see `LICENSE`). Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2.
+
+The Lean sources in `HyperplaneEnd/` are new. They generalize the Lemma A package `../e8-lemma-a-lean` and the Lemma G
+package `../e8-lemma-g-lean` (both by DreamingOfClouds, prepared with Claude Opus 5.5 via Claude Code), which they use
+unchanged through Lake path dependencies. Their extended labels, wrapper reading and realization theorems are those
+packages' work; this package only lets the terminal frame of an entering helper be any frame `U`, keys the wrappers by
+`(E, U)`, and instantiates Lemma A.
+
+Lemma A formalizes the realization part of Lemma A of PR #484 (DreamingOfClouds), which PR #484 adopted from PR #458 §3
+(chafreaky), with PR #471/#500's footprint rule (Dugongue, rohanarun), PR #505's asynchronous borrowing (Dugongue) and
+PR #442's stream model (DaysSky). The event semantics are PR #425's conjugation lemma (jacklightChen / Zhihao Chen). The
+nested-children factorization `T_U T_E⁻¹ = L (C ⊗ I) R` is from `notes/general-clifford-frames.tex`. Lean conventions
+follow the `formal/lean` pin on main and #487/#488 (jamesyc).
diff --git a/research/hyperplane-end-lean/PROOF.md b/research/hyperplane-end-lean/PROOF.md
new file mode 100644
index 0000000000..248723a99c
--- /dev/null
+++ b/research/hyperplane-end-lean/PROOF.md
@@ -0,0 +1,172 @@
+# Hyperplane-ended helpers: Lemma A with an arbitrary terminal frame
+
+A dirty entering helper may end at a hyperplane frame `U` (dim 8) instead of `FULL` (dim 9): its single cleanup gate
+`h -= p` runs right after part B, in a `cleanup_tail` phase, at the join `U` of the frames of `h` and its partner `p`.
+This package proves in Lean 4 that Lemma A's realization still applies. The wrapped residual of such a helper is exactly
+`C ⊗ id`, global phase included, whenever the exact factorization `T_U T_E⁻¹ = L (C ⊗ id) R` holds for its pair
+`(E, U)`. For the 38 helpers of the c8 words, `C = C_[7]` with `7 = |U| − |E|`.
+
+The package reuses Lemma A's and Lemma G's definitions (`Event`, `physRun`, `labRun`, `WellLabelled`, `RecipesExact`,
+`S`, `Hosting`, `realizeRun`, `streamOwner`, `Frame`) through Lake path dependencies. It restates none of them. Lean
+names are in brackets.
+
+## 1. Why a generalization is enough
+
+Lemma A (`../e8-lemma-a-lean/PROOF.md` §2) is stated for an arbitrary label family `T : Λ → M ≃ M`. Its hypothesis (F)
+is `T_{λ¹_j} T_{λ⁰_j}⁻¹ = C ⊗ id` on Lemma G's extended labels `λ⁰_j = (prew, j)`, `λ¹_j = (done, j)`. `FULL` occurs
+only in how Lemma G's PROOF.md §1.3 defines the operator of `(done, j)`: `T_(done,j) = L_E⁻¹ T_FULL`. So the work is to:
+
+1. define the extended labels with an arbitrary terminal frame `U_j`, and wrappers keyed by the pair `(E_j, U_j)`;
+2. show that the wrappers then execute exactly `R_{E,U}⁻¹` and `L_{E,U}⁻¹`, so the HPE word is still an instance of
+   Lemma G's event model with exact recipes;
+3. derive (F) from the exact factorization (N), and show that the HPE word's labels are well formed;
+4. apply Lemma A unchanged.
+
+## 2. Definitions (`HyperplaneEnd/Labels.lean`)
+
+* **Extended labels** [`XLab ι Fr`]: `frame F`, `prew j` or `done j`.
+* **Their operators** [`Text T ent term Lw Rw`], for the word's frame family `T`, entrance frames `ent j`, terminal
+  frames `term j` and wrapper monomials `Lw E U`, `Rw E U`:
+  * `T_(frame F) = T_F`;
+  * `T_(prew,j) = R_{E_j,U_j} T_{E_j}`;
+  * `T_(done,j) = L_{E_j,U_j}⁻¹ T_{U_j}`.
+
+  With `term j = FULL` and `Lw E FULL = L_E`, `Rw E FULL = R_E`, this is Lemma G's §1.3 definition verbatim. So the
+  FULL-ended helpers of #484 are the instance `term j = ⊤`.
+
+## 3. Statements and proofs
+
+**Wrapper recipes** [`pre_recipe`, `post_recipe`]. The pre wrapper `relabel j (prew j) (E_j)` executes
+`T_E T_(prew,j)⁻¹ = R_{E,U}⁻¹`. The post wrapper `relabel j (U_j) (done j)` executes `T_(done,j) T_U⁻¹ = L_{E,U}⁻¹`.
+*Proof:* unfold `Text` and cancel.
+
+**Wrapped block** [`wrapped_block`]. `T_(done,j) T_(prew,j)⁻¹ = L⁻¹ T_U T_E⁻¹ R⁻¹`.
+
+**(N) ⇒ (F)** [`factor_of_exact`]. If `T_U T_E⁻¹ = L (C ⊗ id) R` holds exactly for `(E_j, U_j)`, then
+`T_(done,j) T_(prew,j)⁻¹ = C ⊗ id`. *Proof:* rewrite with `wrapped_block` and (N); `L⁻¹ L` and `R R⁻¹` cancel. The
+equality is between linear maps, so no phase is dropped.
+
+**The pre wrapper must be the `(E, U)` recipe** [`factor_iff_pre`]. Let (N) hold with `L, R` and an invertible `C`.
+Suppose the pre wrapper that ran executed `R'⁻¹`. Then `L⁻¹ T_U T_E⁻¹ R'⁻¹ = C ⊗ id` if and only if `R' = R`.
+*Proof:* the left side is `(C ⊗ id) R R'⁻¹`, and `C ⊗ id` is injective (`LinearEquiv.rTensor`). This is the formal
+content of the review's finding F1: a pre wrapper decoded against `R_{E,FULL}` instead of `R_{E,U}` breaks (F).
+
+**The `cleanup_tail` segment** [`tail`, `tail_labels`] (`HyperplaneEnd/Tail.lean`). The tail
+`[relabel h A_h U, relabel p A_p U, add h p q]` is well labelled: the gate runs with both operands at `U`, which is G0.
+It leaves `h` and `p` at `U` and every other register's label unchanged.
+
+**The HPE word's labels** [`hpe_labels`]. Take the word `a ++ tail ++ b ++ [relabel h U (done h)]`, where:
+* `a` is well labelled and brings `h` to `A_h` and `p` to `A_p`, with `h ≠ p`;
+* `b` (the rest of the cleanup, at FULL) is well labelled and never relabels `h`.
+
+Then the whole word is well labelled, and `h` ends at `(done, h)`. *Proof:* `labRun_untouched` (Lemma G) keeps `h` at `U`
+through `b`, so the post wrapper is admissible. Composition is `wellLabelled_append` and `labRun_append`.
+
+**(C) for a hyperplane end** [`residual_block`]. In frame labels without wrappers, a helper with a unit row running
+from `E` to `U` ends as `T_U T_E⁻¹` of its own input, for any frame `U`. *Proof:* Lemma G's `row_unit`.
+
+**Main theorems** (`HyperplaneEnd/Main.lean`). Assume the following:
+* exact recipes in the labels `Text`;
+* the invocation is well labelled;
+* the helper `j` has a unit row (Lemma G H3), starts at `(prew, j)` and ends at `(done, j)`;
+* (N) holds for the pair `(ent j, term j)`, with any terminal frame `term j`.
+
+Then the following hold.
+* [`hpe_block`] The register ends as `(C ⊗ id) h_j`.
+* [`hpe_family`] Under one owner per family, the helper's family ends as `χ⁻¹ (C ⊗ id) χ` of its own initial value.
+* [`hpe_streams`] The same holds on the physical streams `(fam r, d·σ_r⁻¹)` when registers that share a family have
+  disjoint nonempty footprints. This is `LemmaA.lemmaA_streams` with (F) discharged.
+* [`hpe_word`] The same holds for the concrete word of `hpe_labels`, with `U = term h`. Its label hypotheses are those of
+  `hpe_labels`, so the start/end tags need not be assumed separately.
+
+*Proof:* apply `LemmaA.helper_block`, `lemmaA_family` and `lemmaA_streams` with `T := Text …`, and supply (F) from
+`factor_of_exact` after rewriting the start and end labels.
+
+Lemma A's other conclusions are stated for an arbitrary label family. So they hold for the labels `Text` without change:
+* no other reader (`endpoint_indep`, which needs the helper's zero column);
+* single-unit piece (`lemmaA_piece`);
+* split-off and asynchronous borrowing (`split_off`, `lemmaA_async`);
+* pieces on disjoint blocks commute and gather (`pieces_commute`, `pieces_product`).
+
+**Width on frames** [`hyperplane_width`]. Let `E ≤ U` be frames of `F₂⁹` with `dim E = 1` and `dim U = 8`. Then the
+residual width is `dim U − dim E = 7`, the hosted chart has `9 − 7 = 2` spectators, and `U ≠ FULL` (`dim ⊤ = 9`).
+
+## 4. What is not proved in Lean, and where it is checked
+
+The theorems take the following as hypotheses. They are checked on the emitted words by the HPE tools
+(`scratch/HostingShapeScout/hpe/`, reviewed in `HyperplaneReviewer/FINAL-REPORT.md`), not in Lean.
+
+| hypothesis | meaning | checked by |
+| --- | --- | --- |
+| (N) `hN` | `T_U T_E⁻¹ = L_{E,U} (C_[7] ⊗ I) R_{E,U}` exactly, global phase included, for every `(E, U)` pair of the word | `hpe/code/adapters_local.py` (recipes keyed `"E:U"`), wrapper check "L^-1 S_E R^-1 = C_[w] x I for 39 entrance frames, global phase included", 10 wrapper mutations rejected (`runs/v2/L_ck38.wrap.log`); review: 38/38 helpers, a width-8 claim rejected |
+| `hrec` | every climb executes `T_B T_A⁻¹`; the wrappers execute `R_{E,U}⁻¹`, `L_{E,U}⁻¹` (by `pre_recipe`/`post_recipe`, exactly when the emitted wrapper is the `"E:U"` recipe) | independent emitted replay forward and backward; the 5th wrapper field `U` (review F1 fix); controls `hpe_pre_wrapper_resolved_to_full_recipe` etc. |
+| `hw`, tail shape, `hmv` | G0 in `cleanup_tail`; no later gate relabels `h` | `audit_local.py` (`cur[r] == f` for both operands; `cur[h] = U ≠ FULL`), `audit_and_transport.py` assert, controls `hpe_tail_gate_at_full_frame`, `hpe_tail_gate_moved_into_full_cleanup` |
+| `hS` | unit helper row (and zero column for `endpoint_indep`) | exact forward and inverse-transpose replay on all 728 columns (`audit_and_transport.py`) |
+| (O′), (W) | disjoint footprints; whole invocations | unchanged from Lemma A (`../e8-lemma-a-lean/code/`) |
+
+**No instance enumeration in Lean.** Like the Lemma A and Lemma G packages, this package uses no `decide` or
+`native_decide`. The exact factorization over `ℂ^{2⁹}` for each `(E, U)` pair is a numerical-exact check in the HPE
+tools. Lean proves that this hypothesis, together with the label discipline above, implies the realized endpoint
+`χ⁻¹ (C_[7] ⊗ I₂) χ`.
+
+**Instance check** (`code/check_hpe_pairs.py`, standard library, independent of the HPE tools). For every gate of the
+word's `tail` it checks the following over `F₂⁹`, using the word's frame bases:
+* the hypotheses of `hyperplane_width`: `dim E = 1`, `dim U = 8`, `E ≤ U` and `U ≠ FULL`;
+* the shape used by `tail`/`hpe_labels`:
+  * the gate is `h -= p` with `h ≠ p`, and each helper has exactly one tail gate;
+  * `final[h] = U`, so the post wrapper names `U`;
+  * no gate of the remaining cleanup touches `h`;
+* that (N) was checked exactly for the pair: `WRAPPER-CHECKS.json` passes, and lists `(E, U)` with width `dim U − dim E`.
+
+Six mutants must be rejected, and are: `U = FULL`; the gate `h += p`; a post wrapper naming FULL; the gate left in the
+FULL cleanup; a pair missing from the exact check; width 8 reported. Results on the HPE local runs
+(`hpe/runs/v2/L_*`):
+
+| word | HPE helpers | distinct `(E, U)` pairs (helpers each) | result |
+| --- | --- | --- | --- |
+| ck (`L_ck38`) | 38 | 3 (24, 8, 6) | PASS, 6/6 mutants rejected |
+| atm3 (`L_atm338`) | 38 | 3 (24, 8, 6) | PASS, 6/6 mutants rejected |
+| jp8 (`L_jp838`) | 38 | 3 (24, 8, 6) | PASS, 6/6 mutants rejected |
+
+`python3 verify.py --instances RUN_DIR ...` runs it after the Lean checks.
+
+## 5. Trust base
+
+* Lean 4.21.0, Mathlib v4.21.0 (rev `308445d`), and the axioms `propext`, `Classical.choice`, `Quot.sound`. All 27
+  named results depend on a subset of these (`PrintAxioms.lean`).
+* The Lemma A and Lemma G packages, built here from source.
+* The HPE tools' exact checks of the hypotheses in §4.
+
+## 6. Run
+
+```sh
+python3 research/hyperplane-end-lean/verify.py                       # source scan, cache get, lake build, axioms
+python3 research/hyperplane-end-lean/verify.py --instances RUN_DIR…  # plus code/check_hpe_pairs.py on HPE local runs
+```
+
+`lake build` also builds `../e8-lemma-a-lean` and `../e8-lemma-g-lean` (Lake path dependencies, same Lean and Mathlib
+pin).
+
+## 7. Addendum: multi-gate tails and cold helpers (`HyperplaneEnd/Multi.lean`)
+
+`Tail.lean` treats one helper with one cleanup gate `h -= p`. `Multi.lean` models a general `cleanup_tail`. Each tail gate `t += q • s` (or `t *= q`) runs at its own frame `F`, after every operand not already at
+`F` climbs to it (one relabel).
+
+- **Hypotheses.** The last tail gate touching a helper `j` runs at `term j`. The remaining cleanup `b` never relabels a
+  hyperplane-ended helper. The entrance frame of `j` is arbitrary.
+- `mtail_wellLabelled`, `labRun_mtail`: the tail is well labelled for any gate list, and afterwards each register sits at
+  the frame of the last gate touching it.
+- `hpe_labels_multi`: the word `a ++ mtail ++ b ++ posts` is well labelled, and every helper in the list ends at
+  `(done, j)`. Helpers may be targets or partners of any number of tail gates and may be interleaved.
+- `hpe_labels_tail`: the single-gate word of `Tail.lean` is the one-gate instance when both operands start away
+  from `U`. The shipped hyperplane-ended helpers of #591/#592 are one-gate; multi-gate and `scale` tails are not
+  checked here against emitted words.
+- `hpe_word_multi`: Lemma A on streams for every such helper, given the per-helper (N) as in §3.
+- `exact_cold`, `cold_hyperplane_width`: the cold specialisation. Given `T_E = id` (true of the canonical frame of
+  `E = ⊥`), (N) reads `T_U = L (C ⊗ id) R`, and `⊥ ≤ U` with `dim U = 8` gives width 8 (rank arithmetic). #593's
+  `hpe_word` already takes an arbitrary entrance frame, so the Lean content specific to `E = ⊥` is this
+  specialisation.
+
+As in §4, (N) for each pair (E, U) used, the unit row hS, hrec, and (O′)/(W) are hypotheses checked outside Lean. For
+E = ⊥, (N) was checked locally on all 511 hyperplanes of F₂⁹ with `clifford_exact` from main's
+`direct-delivery504-global/vendor` (tableau and global phase); that script is not shipped in this package.
diff --git a/research/hyperplane-end-lean/PrintAxioms.lean b/research/hyperplane-end-lean/PrintAxioms.lean
new file mode 100644
index 0000000000..38d5b88ff0
--- /dev/null
+++ b/research/hyperplane-end-lean/PrintAxioms.lean
@@ -0,0 +1,28 @@
+import HyperplaneEnd
+#print axioms HyperplaneEnd.pre_recipe
+#print axioms HyperplaneEnd.post_recipe
+#print axioms HyperplaneEnd.wrapped_block
+#print axioms HyperplaneEnd.factor_of_exact
+#print axioms HyperplaneEnd.factor_iff_pre
+#print axioms HyperplaneEnd.tail_labels
+#print axioms HyperplaneEnd.hpe_labels
+#print axioms HyperplaneEnd.residual_block
+#print axioms HyperplaneEnd.hpe_block
+#print axioms HyperplaneEnd.hpe_family
+#print axioms HyperplaneEnd.hpe_streams
+#print axioms HyperplaneEnd.hpe_word
+#print axioms HyperplaneEnd.hyperplane_width
+#print axioms HyperplaneEnd.labRun_climb
+#print axioms HyperplaneEnd.wellLabelled_climb
+#print axioms HyperplaneEnd.labRun_block
+#print axioms HyperplaneEnd.wellLabelled_block
+#print axioms HyperplaneEnd.mtail_wellLabelled
+#print axioms HyperplaneEnd.labRun_mtail
+#print axioms HyperplaneEnd.labRun_mtail_last
+#print axioms HyperplaneEnd.posts_spec
+#print axioms HyperplaneEnd.hpe_labels_multi
+#print axioms HyperplaneEnd.tail_eq_mtail
+#print axioms HyperplaneEnd.hpe_labels_tail
+#print axioms HyperplaneEnd.hpe_word_multi
+#print axioms HyperplaneEnd.exact_cold
+#print axioms HyperplaneEnd.cold_hyperplane_width
diff --git a/research/hyperplane-end-lean/code/check_hpe_pairs.py b/research/hyperplane-end-lean/code/check_hpe_pairs.py
new file mode 100644
index 0000000000..5b5abbb2fc
--- /dev/null
+++ b/research/hyperplane-end-lean/code/check_hpe_pairs.py
@@ -0,0 +1,87 @@
+# Apache-2.0.  Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2.
+"""Instance check for the hyperplane-end theorems on an emitted HPE word.
+
+usage: python3 check_hpe_pairs.py RUN_DIR [--mutants]
+  RUN_DIR holds CANONICAL-WORD.json.gz and WRAPPER-CHECKS.json of an HPE local run (hpe/code emit + wrap).
+
+For every gate ['add', h, p, q, _, U] of the word's `tail` (the `cleanup_tail` phase) it checks, over F_2^9 with
+frames given as lists of 9-bit basis rows:
+  * the hypotheses of `hyperplane_width`: E = start[h] has dim 1, U has dim 8, E <= U, U != FULL;
+  * the shape of `tail`/`hpe_labels`: q = -1, h != p, each helper has one tail gate, final[h] = U (the post wrapper
+    names U), and no gate of the remaining cleanup touches h;
+  * (N) was checked exactly for the pair: WRAPPER-CHECKS.json has status PASS_RESIDUAL_WRAPPERS_ARE_EXACT, and its
+    hyperplane_end_pairs lists (start[h], U) with residual_width = dim U - dim E.
+Python 3.9+, standard library only."""
+import copy, gzip, json, sys
+from pathlib import Path
+
+
+def rank(rows):
+    basis = []                                   # reduced rows, distinct leading bits
+    for r in rows:
+        for b in basis:
+            r = min(r, r ^ b)
+        if r:
+            basis.append(r)
+    return len(basis)
+
+
+def check(word, wrap):
+    viol = []
+    frames, start, final = word['frames'], word['start'], word['final']
+    dim = lambda f: rank(frames[f])
+    full = [f for f, rows in enumerate(frames) if rank(rows) == 9]
+    if wrap.get('status') != 'PASS_RESIDUAL_WRAPPERS_ARE_EXACT':
+        viol.append(f"wrapper status {wrap.get('status')}")
+    checked = {(p['frame'], p['terminal']): p for p in wrap.get('hyperplane_end_pairs', [])}
+    helpers, pairs = set(), {}
+    for g in word['tail']:
+        op, h, p, q, U = g[0], g[1], g[2], g[3], g[-1]
+        E = start[h]
+        if op != 'add' or q != -1 or h == p: viol.append(f'tail gate {g}: not h -= p')
+        if h in helpers: viol.append(f'helper {h}: two tail gates')
+        helpers.add(h)
+        if dim(E) != 1: viol.append(f'helper {h}: dim E = {dim(E)}')
+        if dim(U) != 8: viol.append(f'helper {h}: dim U = {dim(U)}')
+        if rank(frames[E] + frames[U]) != dim(U): viol.append(f'helper {h}: E not in U')
+        if U in full: viol.append(f'helper {h}: U is FULL')
+        if final[h] != U: viol.append(f'helper {h}: final {final[h]} != U {U}')
+        c = checked.get((E, U))
+        if c is None: viol.append(f'helper {h}: pair ({E},{U}) not checked exactly')
+        elif c.get('residual_width') != dim(U) - dim(E): viol.append(f'helper {h}: width {c.get("residual_width")}')
+        pairs.setdefault((E, U), []).append(h)
+    for g in word['cleanup']:
+        if g[1] in helpers or g[2] in helpers: viol.append(f'cleanup gate {g} touches an HPE helper')
+    return viol, helpers, pairs
+
+
+def main():
+    run = Path(sys.argv[1])
+    word = json.load(gzip.open(run / 'CANONICAL-WORD.json.gz'))
+    if not word.get('tail'):
+        print(f'{run.name}: no cleanup_tail gates (not an HPE word)'); print('FAIL'); sys.exit(1)
+    wrap = json.loads((run / 'WRAPPER-CHECKS.json').read_text())
+    viol, helpers, pairs = check(word, wrap)
+    print(f'{run.name}: {len(helpers)} hyperplane-ended helpers, {len(pairs)} distinct (E, U) pairs')
+    for (E, U), hs in sorted(pairs.items()):
+        print(f'  E={E} (dim 1) <= U={U} (dim 8), width 7: {len(hs)} helpers')
+    if '--mutants' in sys.argv:
+        g0 = word['tail'][0]
+        muts = {}
+        w = copy.deepcopy(word); w['tail'][0] = g0[:-1] + [1]; w['final'][g0[1]] = 1; muts['U = FULL'] = (w, wrap)
+        w = copy.deepcopy(word); w['tail'][0] = g0[:3] + [1] + g0[4:]; muts['gate h += p'] = (w, wrap)
+        w = copy.deepcopy(word); w['final'][g0[1]] = 1; muts['post wrapper names FULL'] = (w, wrap)
+        w = copy.deepcopy(word); w['cleanup'] = w['cleanup'] + [['add', g0[1], g0[2], -1, 1, 1]]; muts['gate left in FULL cleanup'] = (w, wrap)
+        x = copy.deepcopy(wrap); x['hyperplane_end_pairs'] = x['hyperplane_end_pairs'][1:]; muts['pair not checked exactly'] = (word, x)
+        x = copy.deepcopy(wrap); x['hyperplane_end_pairs'][0]['residual_width'] = 8; muts['width 8 reported'] = (word, x)
+        for name, (w, x) in muts.items():
+            v, _, _ = check(w, x)
+            print(f'  mutant {name!r}: {"REJECTED" if v else "ACCEPTED"}')
+            if not v: viol.append(f'mutant {name} accepted')
+    if viol:
+        print('FAIL'); [print('  ', v) for v in viol[:50]]; sys.exit(1)
+    print('PASS')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/hyperplane-end-lean/lake-manifest.json b/research/hyperplane-end-lean/lake-manifest.json
new file mode 100644
index 0000000000..b840746047
--- /dev/null
+++ b/research/hyperplane-end-lean/lake-manifest.json
@@ -0,0 +1,134 @@
+{
+ "version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [
+  {
+   "type": "path",
+   "scope": "",
+   "name": "LemmaG",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../e8-lemma-g-lean",
+   "configFile": "lakefile.toml"
+  },
+  {
+   "type": "path",
+   "scope": "",
+   "name": "LemmaA",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../e8-lemma-a-lean",
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.21.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.62",
+   "inherited": true,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  }
+ ],
+ "name": "HyperplaneEnd",
+ "lakeDir": ".lake"
+}
diff --git a/research/hyperplane-end-lean/lakefile.toml b/research/hyperplane-end-lean/lakefile.toml
new file mode 100644
index 0000000000..327a8db12d
--- /dev/null
+++ b/research/hyperplane-end-lean/lakefile.toml
@@ -0,0 +1,18 @@
+name = "HyperplaneEnd"
+defaultTargets = ["HyperplaneEnd"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.21.0"
+
+[[require]]
+name = "LemmaG"
+path = "../e8-lemma-g-lean"
+
+[[require]]
+name = "LemmaA"
+path = "../e8-lemma-a-lean"
+
+[[lean_lib]]
+name = "HyperplaneEnd"
diff --git a/research/hyperplane-end-lean/lean-toolchain b/research/hyperplane-end-lean/lean-toolchain
new file mode 100644
index 0000000000..980709bbba
--- /dev/null
+++ b/research/hyperplane-end-lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.21.0
diff --git a/research/hyperplane-end-lean/verify.py b/research/hyperplane-end-lean/verify.py
new file mode 100644
index 0000000000..26a5b6546a
--- /dev/null
+++ b/research/hyperplane-end-lean/verify.py
@@ -0,0 +1,72 @@
+# Apache-2.0.  Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2.
+"""Verify the Lean formalisation of the hyperplane-end generalization of Lemma A.
+
+usage: python3 verify.py [--no-cache] [--instances RUN_DIR ...]
+  1. the Lean sources (this package, ../e8-lemma-a-lean, ../e8-lemma-g-lean) contain no `sorry`, `admit`, `axiom`,
+     `native_decide`, `implemented_by`, `extern`, `unsafe`, `opaque` and no `set_option` other than the heartbeat limits;
+  2. `lake exe cache get` (Mathlib's pinned build, skipped with --no-cache) and `lake build` (builds LemmaA and LemmaG);
+  3. `lake env lean PrintAxioms.lean`: every named result depends only on propext, Classical.choice, Quot.sound;
+  4. with --instances RUN_DIR ... (HPE local runs holding CANONICAL-WORD.json.gz and WRAPPER-CHECKS.json):
+     code/check_hpe_pairs.py --mutants on each run.
+Python 3.9+, standard library only; `lake` from elan on PATH (the toolchain is pinned by lean-toolchain)."""
+import re, subprocess, sys
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ALLOWED = {'propext', 'Classical.choice', 'Quot.sound'}
+FORBIDDEN = re.compile(r'\b(sorry|admit|axiom|native_decide|implemented_by|extern|unsafe|opaque)\b|set_option\s+(?!maxHeartbeats|maxRecDepth)')
+
+
+def fail(msg):
+    print('FAIL', msg, flush=True); sys.exit(1)
+
+
+def run(cmd, timeout):
+    print('$', ' '.join(cmd), flush=True)
+    p = subprocess.run(cmd, cwd=HERE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, text=True, timeout=timeout)
+    if p.returncode:
+        print(p.stdout[-4000:]); fail(f'{cmd[0]} {cmd[1]} exited {p.returncode}')
+    return p.stdout
+
+
+def strip_comments(src):
+    src = re.sub(r'/-.*?-/', ' ', src, flags=re.S)
+    return re.sub(r'--[^\n]*', ' ', src)
+
+
+def main():
+    args = sys.argv[1:]
+    A, G = HERE.parent / 'e8-lemma-a-lean', HERE.parent / 'e8-lemma-g-lean'
+    lean_files = (sorted(HERE.glob('HyperplaneEnd/*.lean')) + [HERE / 'HyperplaneEnd.lean', HERE / 'PrintAxioms.lean'] +
+                  sorted(A.glob('LemmaA/*.lean')) + [A / 'LemmaA.lean'] + sorted(G.glob('LemmaG/*.lean')) + [G / 'LemmaG.lean'])
+    for p in lean_files:
+        m = FORBIDDEN.search(strip_comments(p.read_text(encoding='utf-8')))
+        if m: fail(f'forbidden token {m.group(0)!r} in {p.name}')
+    print('sources: no sorry / admit / axiom / native_decide / unsafe / opaque / extern in %d files' % len(lean_files), flush=True)
+
+    if '--no-cache' not in args:
+        run(['lake', 'exe', 'cache', 'get'], 3600)
+    out = run(['lake', 'build'], 3600)
+    print('\n'.join(l for l in out.splitlines() if 'warning' in l or 'error' in l or 'Build completed' in l), flush=True)
+
+    out = run(['lake', 'env', 'lean', 'PrintAxioms.lean'], 1200)
+    wanted = [l.split()[2] for l in (HERE / 'PrintAxioms.lean').read_text().splitlines() if l.startswith('#print axioms')]
+    seen = {}
+    for m in re.finditer(r"'([\w.']+)' depends on axioms: \[([^\]]*)\]", out):
+        seen[m.group(1)] = [a.strip() for a in m.group(2).split(',') if a.strip()]
+    for m in re.finditer(r"'([\w.']+)' does not depend on any axioms", out):
+        seen[m.group(1)] = []
+    print(out.strip(), flush=True)
+    for name in wanted:
+        if name not in seen: fail(f'no axiom report for {name}')
+        extra = set(seen[name]) - ALLOWED
+        if extra: fail(f'{name} uses {sorted(extra)}')
+    print(f'axioms: {len(wanted)} results, all within {sorted(ALLOWED)}')
+    if '--instances' in args:
+        for run_dir in args[args.index('--instances') + 1:]:
+            print(run([sys.executable, str(HERE / 'code' / 'check_hpe_pairs.py'), run_dir, '--mutants'], 600).strip())
+    print('PASS')
+
+
+if __name__ == '__main__':
+    main()