[Lean] Hyperplane-ended helpers: Lemma A with an arbitrary terminal frame (no κ claim)

research/hyperplane-end-lean/.gitignore

@@ -0,0 +1 @@
+.lake

research/hyperplane-end-lean/HyperplaneEnd.lean

@@ -0,0 +1,5 @@
+import HyperplaneEnd.Labels
+import HyperplaneEnd.Tail
+import HyperplaneEnd.Main
+import HyperplaneEnd.Clifford
+import HyperplaneEnd.Exact

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

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

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