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..ad6fd00889 --- /dev/null +++ b/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 diff --git a/research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean b/research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean new file mode 100644 index 0000000000..5970d81439 --- /dev/null +++ b/research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean @@ -0,0 +1,586 @@ +/- +Exact Clifford circuits on `n` qubits and a kernel-checkable equality test for them. + +The HPE tools (`hpe/vendor/clifford/clifford_exact.py`) represent every operator of hypothesis +(N) as a literal circuit of five gate kinds acting on state vectors indexed by `x < 2 ^ n` +(bit `i` of `x` is qubit `i`): +* `P G` `v'(G x) = v(x)` for an invertible `G` over `F₂` (rows as bitmasks); +* `D Q α` `v'(x) = i ^ q(x) v(x)`, `q(x) = Σ_{i ∈ x} α_i + 2 Σ_{i ∈ x} ⟨Q_i ≫ (i+1), x ≫ (i+1)⟩ mod 4`; +* `C q s` `v'(x) = ((1 + s i) v(x) + (1 - s i) v(x ⊕ q)) / 2`, `s = ±1`; +* `X b` `v'(x) = v(x ⊕ b)`; +* `phase p` `v' = i ^ p v`. +This file gives the same gates exact semantics over `ℂ` (`gC`, `gL`, `cL`), proves that the +inverse gates invert them (`cE`), and proves `cL_eq_of_check`: if the Boolean `check c₁ c₂` +evaluates to `true` then the two circuits are equal linear maps on `ℂ^512`, global phase included. + +`check` runs both circuits once, over `ℤ[i]` with the `1/2` of every `C` gate dropped, on the single +vector `u(x) = B ^ x` (`B = 4 ^ (#C(c₁) + 1)`); by linearity this computes every column of both +matrices at once, packed in base `B`, and the entry bound `|entry| ≤ 4 ^ #C` makes the packing +injective. The packed integers are a few thousand bits, so the kernel evaluates `check` with its +GMP-backed `Nat` operations; no `native_decide` is used. +Apache-2.0. Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2. +-/ +import Mathlib.LinearAlgebra.TensorProduct.Basis +import Mathlib.LinearAlgebra.StdBasis +import Mathlib.Data.Complex.Basic +import Mathlib.Algebra.Order.Group.Unbundled.Int +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +namespace HyperplaneEnd.Clifford + +/-! ## Bit helpers (ports of `clifford_exact.py`; all data are 9-bit masks) -/ + +/-- Parity of the low `k` bits of `x`. -/ +def par : ℕ → ℕ → Bool + | 0, _ => false + | k + 1, x => (x % 2 == 1) ^^ par k (x / 2) + +/-- `parity` of `clifford_exact.py` for arguments below `2 ^ 12` (every argument here is a 9-bit +mask): `x ^ (x >> 4) ^ (x >> 8)` folds the low 12 bits into a nibble with the same parity, and +`0x6996` is the parity table of nibbles. This uses only GMP-backed kernel operations; `par9_spec` +checks it against the bit-by-bit `par 9` on 9-bit arguments. -/ +def par9 (x : ℕ) : Bool := (0x6996 >>> ((x ^^^ (x >>> 4) ^^^ (x >>> 8)) &&& 15)) % 2 == 1 + +theorem par9_spec : ∀ x : Fin 512, par9 x.val = par 9 x.val := by decide +kernel + +def mvAux : List ℕ → ℕ → ℕ → ℕ + | [], _, _ => 0 + | r :: rs, x, w => (if par9 (r &&& x) then w else 0) + mvAux rs x (2 * w) + +/-- `mv(rows, x) = Σ_i parity(rows[i] & x) << i`: the `F₂`-linear map with the given rows. -/ +def mv (rows : List ℕ) (x : ℕ) : ℕ := mvAux rows x 1 + +def qvAux : List ℕ → List ℕ → ℕ → ℕ → ℕ + | q :: qs, a :: as, x, i => + (if (x >>> i) % 2 = 1 then + a + 2 * (if par9 ((q >>> (i + 1)) &&& (x >>> (i + 1))) then 1 else 0) else 0) + + qvAux qs as x (i + 1) + | _, _, _, _ => 0 + +/-- `qvalue(Q, alpha, x)` of `clifford_exact.py`: the `ℤ/4` exponent of a diagonal gate. -/ +def qv (Q α : List ℕ) (x : ℕ) : ℕ := qvAux Q α x 0 % 4 + +/-! ## Gates and circuits -/ + +/-- The circuit elements of `clifford_exact.Op.circuit`. `pm G Gi` is `P G` together with the +inverse matrix `Gi`; it is read as `v'(y) = v(Gi y)`, which is `P G` whenever `Gi = G⁻¹` +(checked by `Gate.ok`). `cg q s` is `C q (if s then 1 else -1)`. -/ +inductive Gate + | pm (G Gi : List ℕ) + | dg (Q α : List ℕ) + | cg (q : ℕ) (s : Bool) + | xg (b : ℕ) + | ph (p : ℕ) + deriving Repr, DecidableEq + +/-- The inverse gate, as `Op.adjoint` builds it. -/ +def Gate.adj : Gate → Gate + | .pm G Gi => .pm Gi G + | .dg Q α => .dg Q (α.map fun a => (4 - a % 4) % 4) + | .cg q s => .cg q (!s) + | .xg b => .xg b + | .ph p => .ph ((4 - p % 4) % 4) + +/-- `Op.adjoint` on circuits (circuits run left to right). -/ +def adjC (c : List Gate) : List Gate := (c.map Gate.adj).reverse + +/-- Number of `C` gates. -/ +def ncg : List Gate → ℕ + | [] => 0 + | .cg _ _ :: c => ncg c + 1 + | _ :: c => ncg c + +/-- Decidable side conditions under which `Gate.adj` inverts a gate on `N` basis states. -/ +def Gate.ok (N : ℕ) : Gate → Bool + | .pm G Gi => (List.range N).all fun x => + mv Gi (mv G x % N) % N == x && mv G (mv Gi x % N) % N == x + | .dg Q α => (List.range N).all fun x => + (qv Q α x + qv Q (α.map fun a => (4 - a % 4) % 4) x) % 4 == 0 + | .cg q _ => (List.range N).all fun x => ((x ^^^ q) % N ^^^ q) % N == x + | .xg b => (List.range N).all fun x => ((x ^^^ b) % N ^^^ b) % N == x + | .ph _ => true + +def cOk (N : ℕ) (c : List Gate) : Bool := c.all (Gate.ok N) + +/-! ## Integer semantics: `ℤ[i]` as `ℤ × ℤ`, `C` gates without their `1/2` -/ + +/-- Multiplication by `i ^ k`. -/ +def ipow (k : ℕ) (z : ℤ × ℤ) : ℤ × ℤ := + match k % 4 with + | 0 => z + | 1 => (-z.2, z.1) + | 2 => (-z.1, -z.2) + | _ => (z.2, -z.1) + +/-- `(1 + s i) a + (1 - s i) c`. -/ +def cgz (s : Bool) (a c : ℤ × ℤ) : ℤ × ℤ := + if s then (a.1 - a.2 + c.1 + c.2, a.2 + a.1 + c.2 - c.1) + else (a.1 + a.2 + c.1 - c.2, a.2 - a.1 + c.2 + c.1) + +/-- One gate on `ℕ`-indexed vectors (`2 ^ #C`-scaled for `C` gates). -/ +def gz (N : ℕ) : Gate → (ℕ → ℤ × ℤ) → ℕ → ℤ × ℤ + | .pm _ Gi, v, x => v (mv Gi x % N) + | .dg Q α, v, x => ipow (qv Q α x) (v x) + | .cg q s, v, x => cgz s (v x) (v ((x ^^^ q) % N)) + | .xg b, v, x => v ((x ^^^ b) % N) + | .ph p, v, x => ipow p (v x) + +def runZ (N : ℕ) (c : List Gate) (v : ℕ → ℤ × ℤ) : ℕ → ℤ × ℤ := c.foldl (fun v g => gz N g v) v + +/-! ## Kernel evaluation: perfect binary trees -/ + +inductive Tr + | lf (a : ℤ × ℤ) + | nd (l r : Tr) + +def Tr.ofFn (f : ℕ → ℤ × ℤ) : ℕ → Tr + | 0 => .lf (f 0) + | d + 1 => .nd (Tr.ofFn (fun i => f (2 * i)) d) (Tr.ofFn (fun i => f (2 * i + 1)) d) + +def Tr.get : Tr → ℕ → ℤ × ℤ + | .lf a, _ => a + | .nd l r, x => if x % 2 = 0 then l.get (x / 2) else r.get (x / 2) + +/-- `t₁ = k • t₂` entrywise, on trees of the same shape. -/ +def Tr.beqS (k : ℤ) : Tr → Tr → Bool + | .lf a, .lf b => a.1 == k * b.1 && a.2 == k * b.2 + | .nd l r, .nd l' r' => Tr.beqS k l l' && Tr.beqS k r r' + | _, _ => false + +/-- A circuit on `512 = 2 ^ 9` basis states, one materialized tree per gate. -/ +def runT (c : List Gate) (t : Tr) : Tr := c.foldl (fun t g => Tr.ofFn (gz 512 g t.get) 9) t + +/-- The packed equality test: `c₁` and `c₂` (with `#C(c₂) ≤ #C(c₁)`) agree on `ℂ^512` iff +`2^{#C(c₁)} M₁ = 2^{#C(c₁) - #C(c₂)} · 2^{#C(c₂)} M₂` over `ℤ[i]`; both sides are evaluated on +`u(x) = B ^ x`. -/ +def check (c₁ c₂ : List Gate) : Bool := + let B : ℤ := 4 ^ (ncg c₁ + 1) + let t := Tr.ofFn (fun k => (B ^ k, 0)) 9 + ncg c₂ ≤ ncg c₁ && Tr.beqS (2 ^ (ncg c₁ - ncg c₂)) (runT c₁ t) (runT c₂ t) + +/-! ## Exact semantics over `ℂ` -/ + +open Complex + +/-- The basis state `k mod N`. -/ +def fx (N : ℕ) [NeZero N] (k : ℕ) : Fin N := ⟨k % N, Nat.mod_lt _ (NeZero.pos N)⟩ + +def sg (s : Bool) : ℂ := if s then 1 else -1 + +variable (N : ℕ) [NeZero N] + +/-- One gate on `ℂ^N`. -/ +noncomputable def gC : Gate → (Fin N → ℂ) → Fin N → ℂ + | .pm _ Gi, v, x => v (fx N (mv Gi x.val)) + | .dg Q α, v, x => I ^ qv Q α x.val * v x + | .cg q s, v, x => ((1 + sg s * I) * v x + (1 - sg s * I) * v (fx N (x.val ^^^ q))) / 2 + | .xg b, v, x => v (fx N (x.val ^^^ b)) + | .ph p, v, x => I ^ p * v x + +/-- One gate as a `ℂ`-linear map. -/ +noncomputable def gL (g : Gate) : (Fin N → ℂ) →ₗ[ℂ] (Fin N → ℂ) where + toFun := gC N g + map_add' v w := by funext x; cases g <;> simp [gC] <;> ring + map_smul' a v := by funext x; cases g <;> simp [gC] <;> ring + +/-- A circuit as a `ℂ`-linear map; the head gate is applied first. -/ +noncomputable def cL : List Gate → (Fin N → ℂ) →ₗ[ℂ] (Fin N → ℂ) + | [] => LinearMap.id + | g :: c => cL c ∘ₗ gL N g + +variable {N} + +theorem gL_apply (g : Gate) (v : Fin N → ℂ) : gL N g v = gC N g v := rfl + +theorem cL_nil : cL N [] = LinearMap.id := rfl + +theorem cL_cons (g : Gate) (c : List Gate) : cL N (g :: c) = cL N c ∘ₗ gL N g := rfl + +theorem cL_append (c d : List Gate) : cL N (c ++ d) = cL N d ∘ₗ cL N c := by + induction c with + | nil => simp [cL_nil] + | cons g c ih => simp [cL_cons, ih, LinearMap.comp_assoc] + +theorem cL_append_apply (c d : List Gate) (w : Fin N → ℂ) : cL N (c ++ d) w = cL N d (cL N c w) := by + rw [cL_append, LinearMap.comp_apply] + +/-! ### Inverses -/ + +theorem I_pow_of_mod (k : ℕ) (h : k % 4 = 0) : I ^ k = 1 := by + obtain ⟨m, rfl⟩ : ∃ m, k = 4 * m := ⟨k / 4, by omega⟩ + rw [pow_mul, show I ^ 4 = 1 by rw [show (4 : ℕ) = 2 * 2 from rfl, pow_mul, I_sq]; norm_num, one_pow] + +theorem I_pow_mod (k : ℕ) : I ^ k = I ^ (k % 4) := by + conv_lhs => rw [← Nat.div_add_mod k 4, pow_add, pow_mul] + rw [show I ^ 4 = 1 by rw [show (4 : ℕ) = 2 * 2 from rfl, pow_mul, I_sq]; norm_num, one_pow, one_mul] + +theorem fx_val (k : ℕ) : (fx N k).val = k % N := rfl + +theorem fx_of_lt {k : ℕ} (x : Fin N) (h : k % N = x.val) : fx N k = x := Fin.ext h + +theorem all_range {N : ℕ} {p : ℕ → Bool} (h : (List.range N).all p = true) (x : Fin N) : + p x.val = true := by + rw [List.all_eq_true] at h + exact h _ (List.mem_range.2 x.isLt) + +theorem sg_not (s : Bool) : sg (!s) = - sg s := by cases s <;> simp [sg] + +theorem sg_sq (s : Bool) : sg s * sg s = 1 := by cases s <;> simp [sg] + +/-- `Gate.adj` is a two-sided inverse under `Gate.ok`. -/ +theorem gL_adj (g : Gate) (h : g.ok N = true) : + gL N g.adj ∘ₗ gL N g = LinearMap.id ∧ gL N g ∘ₗ gL N g.adj = LinearMap.id := by + cases g with + | pm G Gi => + constructor <;> refine LinearMap.ext fun v => funext fun x => ?_ <;> + simp only [Gate.adj, LinearMap.comp_apply, gL_apply, gC, LinearMap.id_apply] <;> + have hx := all_range h x <;> simp only [Bool.and_eq_true, beq_iff_eq] at hx <;> + congr 1 <;> apply fx_of_lt <;> simp only [fx_val] <;> [exact hx.1; exact hx.2] + | dg Q α => + constructor <;> refine LinearMap.ext fun v => funext fun x => ?_ <;> + simp only [Gate.adj, LinearMap.comp_apply, gL_apply, gC, LinearMap.id_apply] <;> + have hx := all_range h x <;> simp only [beq_iff_eq] at hx <;> + rw [← mul_assoc, ← pow_add, I_pow_of_mod _ (by omega), one_mul] + | cg q s => + have hx : ∀ x : Fin N, fx N ((fx N (x.val ^^^ q)).val ^^^ q) = x := fun x => + fx_of_lt x (by simpa [fx_val] using all_range h x) + constructor <;> refine LinearMap.ext fun v => funext fun x => ?_ <;> + simp only [Gate.adj, LinearMap.comp_apply, gL_apply, gC, LinearMap.id_apply, hx, sg_not] <;> + ring_nf <;> simp only [I_sq, sg_sq, show sg s ^ 2 = 1 by rw [sq, sg_sq]] <;> ring + | xg b => + have hx : ∀ x : Fin N, fx N ((fx N (x.val ^^^ b)).val ^^^ b) = x := fun x => + fx_of_lt x (by simpa [fx_val] using all_range h x) + constructor <;> refine LinearMap.ext fun v => funext fun x => ?_ <;> + simp [Gate.adj, gL_apply, gC, hx] + | ph p => + constructor <;> refine LinearMap.ext fun v => funext fun x => ?_ <;> + simp only [Gate.adj, LinearMap.comp_apply, gL_apply, gC, LinearMap.id_apply] <;> + rw [← mul_assoc, ← pow_add, I_pow_of_mod _ (by omega), one_mul] + +theorem adjC_cons (g : Gate) (c : List Gate) : adjC (g :: c) = adjC c ++ [g.adj] := by + simp [adjC] + +theorem cL_adjC (c : List Gate) (h : cOk N c = true) : + cL N (adjC c) ∘ₗ cL N c = LinearMap.id ∧ cL N c ∘ₗ cL N (adjC c) = LinearMap.id := by + induction c with + | nil => simp [adjC, cL_nil] + | cons g c ih => + simp only [cOk, List.all_cons, Bool.and_eq_true] at h + obtain ⟨ih1, ih2⟩ := ih h.2 + obtain ⟨h1, h2⟩ := gL_adj g h.1 + rw [adjC_cons, cL_append, cL_cons, cL_cons, cL_nil, LinearMap.id_comp] + constructor + · refine LinearMap.ext fun v => ?_ + have e1 := LinearMap.congr_fun ih1 (gL N g v) + have e2 := LinearMap.congr_fun h1 v + simp only [LinearMap.comp_apply, LinearMap.id_apply] at e1 e2 ⊢ + rw [e1, e2] + · refine LinearMap.ext fun v => ?_ + have e1 := LinearMap.congr_fun h2 (cL N (adjC c) v) + have e2 := LinearMap.congr_fun ih2 v + simp only [LinearMap.comp_apply, LinearMap.id_apply] at e1 e2 ⊢ + rw [e1, e2] + +/-- A circuit with valid inverses as a linear equivalence; its inverse is `cL (adjC c)`. -/ +noncomputable def cE (c : List Gate) (h : cOk N c = true) : (Fin N → ℂ) ≃ₗ[ℂ] (Fin N → ℂ) := + LinearEquiv.ofLinear (cL N c) (cL N (adjC c)) (cL_adjC c h).2 (cL_adjC c h).1 + +theorem cE_apply (c : List Gate) (h : cOk N c = true) (v : Fin N → ℂ) : cE c h v = cL N c v := rfl + +theorem cE_symm_apply (c : List Gate) (h : cOk N c = true) (v : Fin N → ℂ) : + (cE c h).symm v = cL N (adjC c) v := rfl + +/-! ### `ℂ` semantics versus integer semantics -/ + +/-- `ℤ[i] → ℂ`. -/ +noncomputable def φ (z : ℤ × ℤ) : ℂ := (z.1 : ℂ) + (z.2 : ℂ) * I + +/-- An `ℕ`-indexed integer vector, read on `ℂ^N`. -/ +noncomputable def emb (N : ℕ) (v : ℕ → ℤ × ℤ) : Fin N → ℂ := fun x => φ (v x.val) + +theorem φ_ipow (k : ℕ) (z : ℤ × ℤ) : φ (ipow k z) = I ^ k * φ z := by + rw [I_pow_mod] + unfold ipow + have : k % 4 < 4 := Nat.mod_lt _ (by norm_num) + interval_cases h : k % 4 <;> simp only [h] <;> apply Complex.ext <;> simp [φ, pow_succ] + +theorem φ_cgz (s : Bool) (a c : ℤ × ℤ) : + φ (cgz s a c) = (1 + sg s * I) * φ a + (1 - sg s * I) * φ c := by + cases s <;> apply Complex.ext <;> simp [φ, cgz, sg] <;> ring + +/-- The scalar a gate loses in the integer semantics. -/ +noncomputable def sc : Gate → ℂ + | .cg _ _ => 1 / 2 + | _ => 1 + +theorem gC_emb (g : Gate) (v : ℕ → ℤ × ℤ) : gC N g (emb N v) = sc g • emb N (gz N g v) := by + funext x + cases g <;> simp only [gC, emb, gz, sc, fx_val, φ_ipow, φ_cgz, Pi.smul_apply, smul_eq_mul, + one_mul] + all_goals ring + +omit [NeZero N] in +theorem runZ_cons (g : Gate) (c : List Gate) (v : ℕ → ℤ × ℤ) : + runZ N (g :: c) v = runZ N c (gz N g v) := rfl + +theorem cL_emb (c : List Gate) (v : ℕ → ℤ × ℤ) : + cL N c (emb N v) = ((1 / 2 : ℂ) ^ ncg c) • emb N (runZ N c v) := by + induction c generalizing v with + | nil => simp [cL_nil, ncg, runZ] + | cons g c ih => + rw [cL_cons, LinearMap.comp_apply, gL_apply, gC_emb, map_smul, ih, runZ_cons, smul_smul] + congr 1 + cases g <;> simp [sc, ncg, pow_succ] + all_goals ring + +/-! ### Linearity, congruence and bounds of the integer semantics -/ + +theorem ipow_add (k : ℕ) (a b : ℤ × ℤ) : ipow k (a + b) = ipow k a + ipow k b := by + unfold ipow; split <;> ext <;> simp <;> ring + +theorem ipow_smul (k : ℕ) (n : ℤ) (a : ℤ × ℤ) : ipow k (n • a) = n • ipow k a := by + unfold ipow; split <;> ext <;> simp + +theorem cgz_add (s : Bool) (a b c d : ℤ × ℤ) : cgz s (a + b) (c + d) = cgz s a c + cgz s b d := by + cases s <;> ext <;> simp [cgz] <;> ring + +theorem cgz_smul (s : Bool) (n : ℤ) (a c : ℤ × ℤ) : cgz s (n • a) (n • c) = n • cgz s a c := by + cases s <;> ext <;> simp [cgz] <;> ring + +/-- One gate as a `ℤ`-linear map. -/ +def gzL (N : ℕ) (g : Gate) : (ℕ → ℤ × ℤ) →ₗ[ℤ] (ℕ → ℤ × ℤ) where + toFun := gz N g + map_add' v w := by funext x; cases g <;> simp [gz, ipow_add, cgz_add] + map_smul' n v := by + funext x; cases g <;> simp only [gz, Pi.smul_apply, RingHom.id_apply, ipow_smul, cgz_smul] + +def runZL (N : ℕ) : List Gate → (ℕ → ℤ × ℤ) →ₗ[ℤ] (ℕ → ℤ × ℤ) + | [] => LinearMap.id + | g :: c => runZL N c ∘ₗ gzL N g + +omit [NeZero N] in +theorem runZL_apply (c : List Gate) (v : ℕ → ℤ × ℤ) : runZL N c v = runZ N c v := by + induction c generalizing v with + | nil => rfl + | cons g c ih => simp only [runZL, LinearMap.comp_apply, ih]; rfl + +theorem gz_congr (g : Gate) {v w : ℕ → ℤ × ℤ} (h : ∀ k < N, v k = w k) : + ∀ x < N, gz N g v x = gz N g w x := by + have hN := NeZero.pos N + intro x hx + cases g <;> simp only [gz, h x hx, h _ (Nat.mod_lt _ hN)] + +theorem runZ_congr (c : List Gate) {v w : ℕ → ℤ × ℤ} (h : ∀ k < N, v k = w k) : + ∀ x < N, runZ N c v x = runZ N c w x := by + induction c generalizing v w with + | nil => exact h + | cons g c ih => exact ih (gz_congr g h) + +/-- Entrywise bound on both coordinates. -/ +def Bnd (M : ℤ) (v : ℕ → ℤ × ℤ) : Prop := ∀ k, |(v k).1| ≤ M ∧ |(v k).2| ≤ M + +theorem ipow_bnd (k : ℕ) {M : ℤ} {z : ℤ × ℤ} (h : |z.1| ≤ M ∧ |z.2| ≤ M) : + |(ipow k z).1| ≤ M ∧ |(ipow k z).2| ≤ M := by + unfold ipow; split <;> simp [abs_neg, h.1, h.2] + +/-- The growth factor of a gate in the integer semantics. -/ +def gw : Gate → ℤ + | .cg _ _ => 4 + | _ => 1 + +omit [NeZero N] in +theorem gz_bnd (g : Gate) {M : ℤ} {v : ℕ → ℤ × ℤ} (h : Bnd M v) : Bnd (gw g * M) (gz N g v) := by + intro x + cases g with + | cg q s => + obtain ⟨h1, h2⟩ := h x + obtain ⟨h3, h4⟩ := h ((x ^^^ q) % N) + rw [abs_le] at h1 h2 h3 h4 + cases s <;> simp only [gz, cgz, gw, if_true, Bool.false_eq_true, if_false] <;> + constructor <;> rw [abs_le] <;> constructor <;> linarith + | pm G Gi => simpa [gz, gw] using h _ + | dg Q α => simpa [gz, gw] using ipow_bnd _ (h x) + | xg b => simpa [gz, gw] using h _ + | ph p => simpa [gz, gw] using ipow_bnd _ (h x) + +omit [NeZero N] in +theorem runZ_bnd (c : List Gate) {M : ℤ} {v : ℕ → ℤ × ℤ} (h : Bnd M v) : + Bnd (4 ^ ncg c * M) (runZ N c v) := by + induction c generalizing M v with + | nil => simpa [ncg, runZ] using h + | cons g c ih => + rw [runZ_cons] + have := ih (gz_bnd (N := N) g h) + cases g <;> simp only [ncg, gw, one_mul] at this ⊢ <;> [skip; skip; rwa [pow_succ, mul_assoc]; skip; skip] <;> exact this + +/-! ### Packing -/ + +/-- A base-`B` expansion with digits `|d i| < B` vanishes only if every digit does. -/ +theorem digits_eq_zero {B : ℤ} (hB : 0 < B) : + ∀ (n : ℕ) (d : ℕ → ℤ), (∀ i < n, |d i| < B) → + ∑ i ∈ Finset.range n, B ^ i * d i = 0 → ∀ i < n, d i = 0 := by + intro n + induction n with + | zero => intro d _ _ i hi; omega + | succ n ih => + intro d hd hs + rw [Finset.sum_range_succ'] at hs + simp only [pow_succ, pow_zero, one_mul] at hs + have hs' : B * ∑ i ∈ Finset.range n, B ^ i * d (i + 1) + d 0 = 0 := by + rw [Finset.mul_sum]; rw [← hs]; congr 1; apply Finset.sum_congr rfl; intro i _; ring + have h0 : d 0 = 0 := by + apply Int.eq_zero_of_abs_lt_dvd _ (hd 0 (by omega)) + exact ⟨-∑ i ∈ Finset.range n, B ^ i * d (i + 1), by linarith⟩ + rw [h0, add_zero] at hs' + have hrest := ih (fun i => d (i + 1)) (fun i hi => hd (i + 1) (by omega)) + ((mul_eq_zero.1 hs').resolve_left hB.ne') + intro i hi + rcases i with _ | i + · exact h0 + · exact hrest i (by omega) + +theorem Tr.get_ofFn (f : ℕ → ℤ × ℤ) (d x : ℕ) : (Tr.ofFn f d).get x = f (x % 2 ^ d) := by + induction d generalizing f x with + | zero => simp [Tr.ofFn, Tr.get, Nat.mod_one] + | succ d ih => + have hm : x % 2 ^ (d + 1) = x % 2 + 2 * (x / 2 % 2 ^ d) := by + rw [pow_succ', Nat.mod_mul] + simp only [Tr.ofFn, Tr.get, ih, hm] + split <;> congr 1 <;> omega + +theorem Tr.beqS_get {k : ℤ} : ∀ {t₁ t₂ : Tr}, Tr.beqS k t₁ t₂ = true → + ∀ x, t₁.get x = k • t₂.get x + | .lf a, .lf b, h, x => by + simp only [Tr.beqS, Bool.and_eq_true, beq_iff_eq] at h + ext <;> simp [Tr.get, h.1, h.2] + | .nd l r, .nd l' r', h, x => by + simp only [Tr.beqS, Bool.and_eq_true] at h + simp only [Tr.get] + split + · exact Tr.beqS_get h.1 _ + · exact Tr.beqS_get h.2 _ + | .lf _, .nd _ _, h, _ => by simp [Tr.beqS] at h + | .nd _ _, .lf _, h, _ => by simp [Tr.beqS] at h + +theorem runT_get (c : List Gate) (t : Tr) : ∀ x < 512, (runT c t).get x = runZ 512 c t.get x := by + induction c generalizing t with + | nil => intro x _; rfl + | cons g c ih => + intro x hx + change (runT c (Tr.ofFn (gz 512 g t.get) 9)).get x = runZ 512 c (gz 512 g t.get) x + rw [ih _ x hx] + refine runZ_congr c (fun k hk => ?_) x hx + rw [Tr.get_ofFn, Nat.mod_eq_of_lt (by simpa using hk)] + +/-- The unit vector `e_y`. -/ +def eI (y : ℕ) : ℕ → ℤ × ℤ := fun k => if k = y then (1, 0) else 0 + +theorem eI_bnd (y : ℕ) : Bnd 1 (eI y) := by + intro k; unfold eI; split <;> simp + +/-- Vector digits: `Σ_{y (z y).1) (fun y hy => (hz y hy).1) (by + have := congrArg Prod.fst hs + simpa [Prod.fst_sum, smul_eq_mul] using this) + have h2 := digits_eq_zero hB n (fun y => (z y).2) (fun y hy => (hz y hy).2) (by + have := congrArg Prod.snd hs + simpa [Prod.snd_sum, smul_eq_mul] using this) + intro y hy + exact Prod.ext (h1 y hy) (h2 y hy) + +theorem pow_two_mul_pow_four_le {n₁ n₂ : ℕ} (h : n₂ ≤ n₁) : + (2 : ℤ) ^ (n₁ - n₂) * 4 ^ n₂ ≤ 4 ^ n₁ := by + have : (4 : ℤ) ^ n₁ = 2 ^ (n₁ - n₂) * 4 ^ n₂ * 2 ^ (n₁ - n₂) := by + rw [show (4 : ℤ) = 2 ^ 2 by norm_num, ← pow_mul, ← pow_mul, ← pow_add, ← pow_add] + congr 1; omega + rw [this] + exact le_mul_of_one_le_right (by positivity) (one_le_pow₀ (by norm_num)) + +theorem single_eq_emb (y : Fin 512) (a : ℂ) : Pi.single y a = a • emb 512 (eI y.val) := by + funext x + by_cases hxy : x = y + · subst hxy; simp [emb, eI, φ] + · have : x.val ≠ y.val := fun h => hxy (Fin.ext h) + simp [emb, eI, φ, hxy, this] + +/-- **The packed check is sound.** If `check c₁ c₂` evaluates to `true`, the circuits are the +same linear map on `ℂ^512`. -/ +theorem cL_eq_of_check (c₁ c₂ : List Gate) (h : check c₁ c₂ = true) : cL 512 c₁ = cL 512 c₂ := by + simp only [check, Bool.and_eq_true, decide_eq_true_eq] at h + obtain ⟨hle, hT⟩ := h + have hB : (0 : ℤ) < 4 ^ (ncg c₁ + 1) := by positivity + -- the packed vector is `Σ_y B^y e_y` on `[0, 512)` + have ht : ∀ k < 512, (Tr.ofFn (fun k => (((4 : ℤ) ^ (ncg c₁ + 1)) ^ k, (0 : ℤ))) 9).get k = + (∑ y ∈ Finset.range 512, (((4 : ℤ) ^ (ncg c₁ + 1)) ^ y) • eI y) k := by + intro k hk + rw [Tr.get_ofFn, Nat.mod_eq_of_lt (by simpa using hk), Finset.sum_apply] + simp only [eI, Pi.smul_apply, smul_ite, smul_zero] + rw [Finset.sum_ite_eq (Finset.range 512) k, if_pos (Finset.mem_range.2 hk)] + ext <;> simp + have hpack : ∀ c : List Gate, ∀ x < 512, + runZ 512 c (Tr.ofFn (fun k => (((4 : ℤ) ^ (ncg c₁ + 1)) ^ k, (0 : ℤ))) 9).get x = + ∑ y ∈ Finset.range 512, (((4 : ℤ) ^ (ncg c₁ + 1)) ^ y) • runZ 512 c (eI y) x := by + intro c x hx + rw [runZ_congr c ht x hx, ← runZL_apply, map_sum, Finset.sum_apply] + refine Finset.sum_congr rfl fun y _ => ?_ + rw [map_smul, Pi.smul_apply, runZL_apply] + -- entrywise identity of the integer matrices + have hent : ∀ x < 512, ∀ y < 512, + runZ 512 c₁ (eI y) x = (2 : ℤ) ^ (ncg c₁ - ncg c₂) • runZ 512 c₂ (eI y) x := by + intro x hx + have hx' := Tr.beqS_get hT x + rw [runT_get _ _ x hx, runT_get _ _ x hx, hpack _ x hx, hpack _ x hx, Finset.smul_sum] at hx' + have hz := vec_digits hB 512 + (fun y => runZ 512 c₁ (eI y) x - (2 : ℤ) ^ (ncg c₁ - ncg c₂) • runZ 512 c₂ (eI y) x) + (fun y _ => by + obtain ⟨a1, a2⟩ := runZ_bnd (N := 512) c₁ (eI_bnd y) x + obtain ⟨b1, b2⟩ := runZ_bnd (N := 512) c₂ (eI_bnd y) x + have hk := pow_two_mul_pow_four_le hle + have h4 : (0 : ℤ) < 4 ^ ncg c₁ := by positivity + have h2 : (0 : ℤ) < 2 ^ (ncg c₁ - ncg c₂) := by positivity + rw [mul_one] at a1 a2 b1 b2 + rw [pow_succ] + simp only [Prod.fst_sub, Prod.snd_sub, Prod.smul_fst, Prod.smul_snd, smul_eq_mul] + constructor + · calc |_| ≤ |(runZ 512 c₁ (eI y) x).1| + |2 ^ (ncg c₁ - ncg c₂) * (runZ 512 c₂ (eI y) x).1| := + abs_sub _ _ + _ ≤ 4 ^ ncg c₁ + 2 ^ (ncg c₁ - ncg c₂) * 4 ^ ncg c₂ := by + rw [abs_mul, abs_of_pos h2]; gcongr + _ < 4 ^ ncg c₁ * 4 := by linarith + · calc |_| ≤ |(runZ 512 c₁ (eI y) x).2| + |2 ^ (ncg c₁ - ncg c₂) * (runZ 512 c₂ (eI y) x).2| := + abs_sub _ _ + _ ≤ 4 ^ ncg c₁ + 2 ^ (ncg c₁ - ncg c₂) * 4 ^ ncg c₂ := by + rw [abs_mul, abs_of_pos h2]; gcongr + _ < 4 ^ ncg c₁ * 4 := by linarith) + (by + simp only [smul_sub, Finset.sum_sub_distrib, hx'] + rw [sub_eq_zero] + exact Finset.sum_congr rfl fun y _ => smul_comm _ _ _) + intro y hy + exact sub_eq_zero.1 (hz y hy) + -- back to `ℂ` + apply LinearMap.pi_ext + intro y a + rw [single_eq_emb, map_smul, map_smul, cL_emb, cL_emb] + congr 1 + funext x + simp only [Pi.smul_apply, emb, smul_eq_mul] + rw [hent x.val x.isLt y.val y.isLt] + have h2 : ((1 / 2 : ℂ) ^ ncg c₁) * (2 : ℂ) ^ (ncg c₁ - ncg c₂) = (1 / 2 : ℂ) ^ ncg c₂ := by + obtain ⟨k, hk⟩ : ∃ k, ncg c₁ = ncg c₂ + k := ⟨ncg c₁ - ncg c₂, by omega⟩ + rw [hk, Nat.add_sub_cancel_left, pow_add, mul_assoc, ← mul_pow] + norm_num + rw [← h2, mul_assoc] + congr 1 + simp only [φ, Prod.smul_fst, Prod.smul_snd, smul_eq_mul] + push_cast + ring + +end HyperplaneEnd.Clifford diff --git a/research/hyperplane-end-lean/HyperplaneEnd/Exact.lean b/research/hyperplane-end-lean/HyperplaneEnd/Exact.lean new file mode 100644 index 0000000000..1af33a206a --- /dev/null +++ b/research/hyperplane-end-lean/HyperplaneEnd/Exact.lean @@ -0,0 +1,592 @@ +/- +Hypothesis (N) proved for the hyperplane-end pairs of the HPE words, and `hpe_word` without (N). + +(N) for a pair `(E, U)` is the exact identity `T_U T_E⁻¹ = L_{E,U} (C ⊗ id) R_{E,U}` on +`ℂ^128 ⊗ ℂ^4 ≅ ℂ^512` (9 qubits; the `C` factor acts on qubits 0–6, the spectators are 7, 8): +* `T_F` is `canonical_frame(9, F)` of `hpe/vendor/clifford/clifford_exact.py` (`canon`, a port of + `basis_extend`, `inv` and the quadratic form `Q`), for a frame given by its basis rows; +* `L_{E,U}`, `R_{E,U}` are `monomial_op` of the `"E:U"` recipe in `RESIDUAL-ADAPTERS.json` + (`Mono.gates`: diagonal, permutation, `X`, phase); +* `C = C₇ = fourier(7)`, the product of the seven `C` gates. +Every HPE word (ck, atm3, jp8 of the v2 local runs; the same three recipes appear in every +`RESIDUAL-ADAPTERS.json` of the HPE runs) uses the same three `(E, U)` pairs, so the nine +word/pair identities are the three theorems `exact_N_pair1/2/3` (`exact_N_nine`). Each is +checked by the kernel with `Clifford.check` (`decide +kernel`, no `native_decide`). + +`hpe_word_exact` is `hpe_word` for these operators with (N) discharged: its only extra hypothesis +is that the helper's `(entrance, terminal)` pair is one of the certified pairs. +Apache-2.0. Prepared with Claude Opus 5.5 (Anthropic) in omp; submitted by jeremykothe2. +-/ +import HyperplaneEnd.Clifford +import HyperplaneEnd.Main + +namespace HyperplaneEnd.Exact + +open HyperplaneEnd.Clifford TensorProduct Complex + +/-! ## Ports of `canonical_frame` and `monomial_op` (`clifford_exact.py`, `adapters_local.py`) -/ + +/-- `transpose(rows, n)`, column `i`. -/ +def colBits (i : ℕ) : List ℕ → ℕ → ℕ + | [], _ => 0 + | r :: rs, w => (if (r >>> i) % 2 = 1 then w else 0) + colBits i rs (2 * w) + +def transpose (rows : List ℕ) (n : ℕ) : List ℕ := (List.range n).map fun i => colBits i rows 1 + +/-- `x.bit_length() - 1` for `0 < x < 2 ^ 64`. -/ +def lead : ℕ → ℕ → ℕ + | 0, _ => 0 + | f + 1, x => if x < 2 then 0 else lead f (x / 2) + 1 + +/-- One step of `rank`: insert `x` into the pivot table (leading bit ↦ row). -/ +def insPiv : ℕ → List (ℕ × ℕ) → ℕ → List (ℕ × ℕ) + | 0, p, _ => p + | f + 1, p, x => + if x = 0 then p else + match p.lookup (lead 64 x) with + | none => (lead 64 x, x) :: p + | some r => insPiv f p (x ^^^ r) + +def rank (rows : List ℕ) : ℕ := (rows.foldl (insPiv 64) []).length + +def basisExtend (cols : List ℕ) (n : ℕ) : List ℕ := + (cols ++ (List.range n).map (2 ^ ·)).foldl + (fun out x => if rank (out ++ [x]) > out.length then out ++ [x] else out) [] + +/-- `inv(rows, n)`: Gauss–Jordan over `F₂` (the result is certified by `Gate.ok`). -/ +def invRows (n : ℕ) (rows : List ℕ) : List ℕ := + let a0 := (List.range n).map fun i => rows.getD i 0 ||| (2 ^ (n + i)) + let a := (List.range n).foldl (fun a j => + match (List.range n).find? (fun i => decide (j ≤ i) && (a.getD i 0 >>> j) % 2 == 1) with + | none => a + | some k => + let a := (a.set j (a.getD k 0)).set k (a.getD j 0) + let pj := a.getD j 0 + (List.range n).map fun i => + let ai := a.getD i 0 + if i ≠ j ∧ (ai >>> j) % 2 = 1 then ai ^^^ pj else ai) a0 + a.map (· >>> n) + +/-- `fourier(n, range(r))`. -/ +def fourierC (r : ℕ) : List Gate := (List.range r).map fun i => .cg (2 ^ i) true + +/-- `canonical_frame(n, U)`: `K⁻¹ · fourier(r) · K` with `K = perm(G) then diag(Q)`. -/ +def canon (n : ℕ) (U : List ℕ) : List Gate := + let r := U.length + if r = 0 then [] else if r = n then fourierC n else + let G := transpose (basisExtend U n) n + let Gi := invRows n G + let gt := transpose Gi n + let Q := (List.range n).map fun i => + 2 ^ i ^^^ ((List.range n).map fun j => if par9 (gt.getD i 0 &&& gt.getD j 0) then 2 ^ j else 0).sum + let α := (List.range n).map fun i => (Q.getD i 0 >>> i) % 2 + let K := [Gate.pm G Gi, Gate.dg Q α] + adjC K ++ fourierC r ++ K + +/-- A serialized wrapper monomial: `quadratic_rows`, `linear_Z4`, `matrix_rows`, `offset`, `phase`. -/ +structure Mono where + Q : List ℕ + α : List ℕ + G : List ℕ + b : ℕ + p : ℕ + deriving DecidableEq + +/-- `monomial_op(rec)`: `diag(Q, α)`, then `perm(G)`, then `X(offset)`, then the phase. -/ +def Mono.gates (r : Mono) : List Gate := [.dg r.Q r.α, .pm r.G (invRows 9 r.G), .xg r.b, .ph r.p] + +/-- An `(E, U)` pair with its `"E:U"` recipe (`left` = `L`, `right` = `R`). -/ +structure Pair where + E : List ℕ + U : List ℕ + L : Mono + R : Mono + deriving DecidableEq + +/-! ## The certified pairs (from `RESIDUAL-ADAPTERS.json`) -/ + +/-- `(E, U)` pair 1 (ck frames 437:1079). -/ +def pair1 : Pair := ⟨[45], [256, 128, 64, 33, 16, 9, 5, 2], + ⟨[5, 0, 5, 0, 0, 0, 0, 0, 0], [3, 2, 3, 2, 2, 2, 2, 0, 0], [128, 2, 261, 1, 8, 4, 16, 32, 64], 0, 0⟩, + ⟨[12, 0, 1, 41, 0, 40, 0, 0, 0], [2, 2, 0, 3, 2, 3, 2, 2, 2], [44, 2, 4, 16, 64, 128, 256, 13, 32], 511, 1⟩⟩ + +/-- `(E, U)` pair 2 (ck frames 438:1080). -/ +def pair2 : Pair := ⟨[51], [256, 128, 64, 33, 17, 8, 4, 3], + ⟨[3, 3, 0, 0, 0, 0, 0, 0, 0], [3, 3, 2, 2, 2, 2, 2, 0, 0], [128, 259, 4, 8, 1, 2, 16, 32, 64], 0, 0⟩, + ⟨[18, 1, 0, 0, 49, 48, 0, 0, 0], [2, 0, 2, 2, 3, 3, 2, 2, 2], [50, 2, 4, 8, 64, 128, 256, 19, 32], 511, 1⟩⟩ + +/-- `(E, U)` pair 3 (ck frames 439:1081). -/ +def pair3 : Pair := ⟨[30], [256, 128, 64, 32, 18, 10, 6, 1], + ⟨[0, 6, 6, 0, 0, 0, 0, 0, 0], [2, 3, 3, 2, 2, 2, 2, 0, 0], [1, 128, 262, 2, 4, 8, 16, 32, 64], 0, 0⟩, + ⟨[0, 12, 2, 26, 24, 0, 0, 0, 0], [2, 2, 0, 3, 3, 2, 2, 2, 2], [1, 28, 4, 32, 64, 128, 256, 14, 16], 511, 1⟩⟩ + +def pairs : List Pair := [pair1, pair2, pair3] + +/-- The `(E, U)` pairs of the three HPE words: `(word, E index, U index, E rows, U rows)`. -/ +def nineInstances : List (String × ℕ × ℕ × List ℕ × List ℕ) := + [("ck", 437, 1079, pair1.E, pair1.U), ("ck", 438, 1080, pair2.E, pair2.U), + ("ck", 439, 1081, pair3.E, pair3.U), ("atm3", 437, 1079, pair1.E, pair1.U), + ("atm3", 438, 1080, pair2.E, pair2.U), ("atm3", 439, 1081, pair3.E, pair3.U), + ("jp8", 421, 998, pair1.E, pair1.U), ("jp8", 422, 999, pair2.E, pair2.U), + ("jp8", 423, 1000, pair3.E, pair3.U)] + +def findPair (E U : List ℕ) : Option Pair := pairs.find? fun p => p.E == E && p.U == U + +/-! ## The operators on `ℂ^512` -/ + +/-- `canonical_frame(9, F)` as a linear equivalence (identity if its gate data were invalid, +which `cOk` rules out for every frame used below). -/ +noncomputable def frameOp (F : List ℕ) : (Fin 512 → ℂ) ≃ₗ[ℂ] (Fin 512 → ℂ) := + if h : cOk 512 (canon 9 F) = true then cE _ h else LinearEquiv.refl ℂ _ + +noncomputable def monoOp (r : Mono) : (Fin 512 → ℂ) ≃ₗ[ℂ] (Fin 512 → ℂ) := + if h : cOk 512 r.gates = true then cE _ h else LinearEquiv.refl ℂ _ + +noncomputable def lwOp (E U : List ℕ) : (Fin 512 → ℂ) ≃ₗ[ℂ] (Fin 512 → ℂ) := + match findPair E U with + | some p => monoOp p.L + | none => LinearEquiv.refl ℂ _ + +noncomputable def rwOp (E U : List ℕ) : (Fin 512 → ℂ) ≃ₗ[ℂ] (Fin 512 → ℂ) := + match findPair E U with + | some p => monoOp p.R + | none => LinearEquiv.refl ℂ _ + +/-! ## Transport to `A ⊗ B` (`A` = qubits 0–6, `B` = qubits 7–8) -/ + +abbrev A := Fin 128 → ℂ +abbrev B := Fin 4 → ℂ + +/-- `x ↦ (x mod 128, x / 128)`. -/ +def split : Fin 512 ≃ Fin 128 × Fin 4 where + toFun x := (fx 128 x.val, fx 4 (x.val / 128)) + invFun p := ⟨p.1.val + 128 * p.2.val, by omega⟩ + left_inv x := by ext; simp [fx]; omega + right_inv p := by + ext <;> simp [fx] + all_goals omega + +/-- `A ⊗ B ≅ ℂ^512`, `a ⊗ b ↦ (x ↦ a(x mod 128) b(x / 128))`. -/ +noncomputable def eT : (A ⊗[ℂ] B) ≃ₗ[ℂ] (Fin 512 → ℂ) := + ((Pi.basisFun ℂ (Fin 128)).tensorProduct (Pi.basisFun ℂ (Fin 4))).equivFun.trans + (LinearEquiv.funCongrLeft ℂ ℂ split) + +theorem eT_tmul (a : A) (b : B) (x : Fin 512) : eT (a ⊗ₜ b) x = a (split x).1 * b (split x).2 := by + simp only [eT, LinearEquiv.trans_apply, LinearEquiv.funCongrLeft_apply, LinearMap.funLeft_apply, + Basis.equivFun_apply] + rw [show split x = ((split x).1, (split x).2) from rfl, Basis.tensorProduct_repr_tmul_apply, + Pi.basisFun_repr, Pi.basisFun_repr, smul_eq_mul, mul_comm] + +/-- An operator on `ℂ^512` read on `A ⊗ B`. -/ +noncomputable def conj (f : (Fin 512 → ℂ) ≃ₗ[ℂ] (Fin 512 → ℂ)) : (A ⊗[ℂ] B) ≃ₗ[ℂ] (A ⊗[ℂ] B) := + eT.trans (f.trans eT.symm) + +/-- The frame family `T_F = canonical_frame(9, F)` on `A ⊗ B`. -/ +noncomputable def T (F : List ℕ) : (A ⊗[ℂ] B) ≃ₗ[ℂ] (A ⊗[ℂ] B) := conj (frameOp F) + +/-- The wrapper monomials `L_{E,U}` and `R_{E,U}` on `A ⊗ B`. -/ +noncomputable def Lw (E U : List ℕ) : (A ⊗[ℂ] B) ≃ₗ[ℂ] (A ⊗[ℂ] B) := conj (lwOp E U) +noncomputable def Rw (E U : List ℕ) : (A ⊗[ℂ] B) ≃ₗ[ℂ] (A ⊗[ℂ] B) := conj (rwOp E U) + +/-- The residual `C₇ = fourier(7)` on the 7 coordinate qubits. -/ +noncomputable def C7 : A →ₗ[ℂ] A := cL 128 (fourierC 7) + +/-- Bit facts for a `C` gate on qubit `i < 7` of 9 qubits. -/ +theorem split_xor : ∀ i : Fin 7, ∀ x : Fin 512, + (x.val ^^^ 2 ^ i.val) % 512 % 128 = (x.val % 128 ^^^ 2 ^ i.val) % 128 ∧ + (x.val ^^^ 2 ^ i.val) % 512 / 128 % 4 = x.val / 128 % 4 := by + decide +kernel + +theorem rTensor_cg (i : Fin 7) (t : A ⊗[ℂ] B) : + eT ((gL 128 (.cg (2 ^ i.val) true)).rTensor B t) = gL 512 (.cg (2 ^ i.val) true) (eT t) := by + induction t using TensorProduct.induction_on with + | zero => simp + | tmul a b => + rw [LinearMap.rTensor_tmul] + funext x + obtain ⟨h1, h2⟩ := split_xor i x + simp only [eT_tmul, gL_apply, gC, split, Equiv.coe_fn_mk] + have e1 : fx 128 (fx 512 (x.val ^^^ 2 ^ i.val)).val = fx 128 ((fx 128 x.val).val ^^^ 2 ^ i.val) := + Fin.ext (by simpa [fx] using h1) + have e2 : fx 4 ((fx 512 (x.val ^^^ 2 ^ i.val)).val / 128) = fx 4 (x.val / 128) := + Fin.ext (by simpa [fx] using h2) + rw [e1, e2] + ring + | add s t hs ht => simp [map_add, hs, ht] + +theorem rTensor_C7 (t : A ⊗[ℂ] B) : eT (C7.rTensor B t) = cL 512 (fourierC 7) (eT t) := by + suffices ∀ c : List Gate, (∀ g ∈ c, ∃ i : Fin 7, g = .cg (2 ^ i.val) true) → + ∀ t, eT ((cL 128 c).rTensor B t) = cL 512 c (eT t) by + refine this _ (fun g hg => ?_) t + simp only [fourierC, List.mem_map, List.mem_range] at hg + obtain ⟨i, hi, rfl⟩ := hg + exact ⟨⟨i, hi⟩, rfl⟩ + intro c hc + induction c with + | nil => intro t; simp [cL_nil] + | cons g c ih => + intro t + obtain ⟨i, rfl⟩ := hc g (List.mem_cons_self ..) + rw [cL_cons, LinearMap.rTensor_comp, LinearMap.comp_apply, ih (fun g hg => hc g + (List.mem_cons_of_mem _ hg)), rTensor_cg, cL_cons, LinearMap.comp_apply] + +/-! ## (N) from the kernel checks -/ + +theorem frameOp_of_ok (F : List ℕ) (h : cOk 512 (canon 9 F) = true) : frameOp F = cE _ h := by + unfold frameOp; rw [dif_pos h] + +theorem monoOp_of_ok (r : Mono) (h : cOk 512 r.gates = true) : monoOp r = cE _ h := by + unfold monoOp; rw [dif_pos h] + +/-- The two sides of (N) as circuits: `T_E⁻¹` then `T_U`, versus `R`, `C₇ ⊗ id`, `L`. -/ +def lhsC (p : Pair) : List Gate := adjC (canon 9 p.E) ++ canon 9 p.U +def rhsC (p : Pair) : List Gate := p.R.gates ++ fourierC 7 ++ p.L.gates + +/-- (N) for a pair whose gate data are valid and whose two circuits pass `check`. -/ +theorem exact_N_of_check (p : Pair) (hf : findPair p.E p.U = some p) + (hE : cOk 512 (canon 9 p.E) = true) (hU : cOk 512 (canon 9 p.U) = true) + (hL : cOk 512 p.L.gates = true) (hR : cOk 512 p.R.gates = true) + (hc : check (lhsC p) (rhsC p) = true) (v : A ⊗[ℂ] B) : + T p.U ((T p.E).symm v) = Lw p.E p.U (C7.rTensor B (Rw p.E p.U v)) := by + have key := LinearMap.congr_fun (cL_eq_of_check _ _ hc) (eT v) + rw [lhsC, rhsC, cL_append_apply, cL_append_apply, cL_append_apply] at key + have hl : lwOp p.E p.U = monoOp p.L := by unfold lwOp; rw [hf] + have hr : rwOp p.E p.U = monoOp p.R := by unfold rwOp; rw [hf] + unfold T Lw Rw conj + rw [hl, hr, frameOp_of_ok _ hE, frameOp_of_ok _ hU, monoOp_of_ok _ hL, monoOp_of_ok _ hR] + simp only [LinearEquiv.trans_apply, LinearEquiv.symm_trans_apply, LinearEquiv.symm_symm, + LinearEquiv.apply_symm_apply, cE_apply, cE_symm_apply, rTensor_C7] + rw [key] + +/-! ### The kernel checks + +`canon`, `invRows` and `Mono.gates` are evaluated once into gate literals (`fE1 … rhsLit3`, +generated from `clifford_exact.py` and proved equal by the kernel); `cOk` and `check` then run on +the literals, so the kernel never re-evaluates a frame computation per basis state. -/ + +/-- `canon 9 pair1.E`, evaluated. -/ +def fE1 : List Gate := + [.dg [32, 0, 32, 32, 0, 45, 0, 0, 0] [0, 0, 0, 0, 0, 3, 0, 0, 0], + .pm [32, 33, 2, 36, 40, 16, 64, 128, 256] [3, 4, 9, 17, 32, 1, 64, 128, 256], + .cg 1 true, + .pm [3, 4, 9, 17, 32, 1, 64, 128, 256] [32, 33, 2, 36, 40, 16, 64, 128, 256], + .dg [32, 0, 32, 32, 0, 45, 0, 0, 0] [0, 0, 0, 0, 0, 1, 0, 0, 0]] + +/-- `canon 9 pair1.U`, evaluated. -/ +def fU1 : List Gate := + [.dg [44, 0, 45, 45, 0, 45, 0, 0, 0] [0, 0, 3, 3, 0, 3, 0, 0, 0], + .pm [256, 128, 64, 32, 16, 8, 4, 2, 45] [360, 128, 64, 32, 16, 8, 4, 2, 1], + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .cg 128 true, + .pm [360, 128, 64, 32, 16, 8, 4, 2, 1] [256, 128, 64, 32, 16, 8, 4, 2, 45], + .dg [44, 0, 45, 45, 0, 45, 0, 0, 0] [0, 0, 1, 1, 0, 1, 0, 0, 0]] + +/-- `pair1.L.gates`, evaluated. -/ +def wL1 : List Gate := + [.dg [5, 0, 5, 0, 0, 0, 0, 0, 0] [3, 2, 3, 2, 2, 2, 2, 0, 0], + .pm [128, 2, 261, 1, 8, 4, 16, 32, 64] [8, 2, 32, 16, 64, 128, 256, 1, 44], + .xg 0, + .ph 0] + +/-- `pair1.R.gates`, evaluated. -/ +def wR1 : List Gate := + [.dg [12, 0, 1, 41, 0, 40, 0, 0, 0] [2, 2, 0, 3, 2, 3, 2, 2, 2], + .pm [44, 2, 4, 16, 64, 128, 256, 13, 32] [385, 2, 4, 261, 8, 256, 16, 32, 64], + .xg 511, + .ph 1] + +/-- `lhsC pair1`, evaluated. -/ +def lhsLit1 : List Gate := + [.dg [32, 0, 32, 32, 0, 45, 0, 0, 0] [0, 0, 0, 0, 0, 3, 0, 0, 0], + .pm [32, 33, 2, 36, 40, 16, 64, 128, 256] [3, 4, 9, 17, 32, 1, 64, 128, 256], + .cg 1 false, + .pm [3, 4, 9, 17, 32, 1, 64, 128, 256] [32, 33, 2, 36, 40, 16, 64, 128, 256], + .dg [32, 0, 32, 32, 0, 45, 0, 0, 0] [0, 0, 0, 0, 0, 1, 0, 0, 0], + .dg [44, 0, 45, 45, 0, 45, 0, 0, 0] [0, 0, 3, 3, 0, 3, 0, 0, 0], + .pm [256, 128, 64, 32, 16, 8, 4, 2, 45] [360, 128, 64, 32, 16, 8, 4, 2, 1], + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .cg 128 true, + .pm [360, 128, 64, 32, 16, 8, 4, 2, 1] [256, 128, 64, 32, 16, 8, 4, 2, 45], + .dg [44, 0, 45, 45, 0, 45, 0, 0, 0] [0, 0, 1, 1, 0, 1, 0, 0, 0]] + +/-- `rhsC pair1`, evaluated. -/ +def rhsLit1 : List Gate := + [.dg [12, 0, 1, 41, 0, 40, 0, 0, 0] [2, 2, 0, 3, 2, 3, 2, 2, 2], + .pm [44, 2, 4, 16, 64, 128, 256, 13, 32] [385, 2, 4, 261, 8, 256, 16, 32, 64], + .xg 511, + .ph 1, + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .dg [5, 0, 5, 0, 0, 0, 0, 0, 0] [3, 2, 3, 2, 2, 2, 2, 0, 0], + .pm [128, 2, 261, 1, 8, 4, 16, 32, 64] [8, 2, 32, 16, 64, 128, 256, 1, 44], + .xg 0, + .ph 0] + +/-- `canon 9 pair2.E`, evaluated. -/ +def fE2 : List Gate := + [.dg [32, 32, 0, 0, 32, 51, 0, 0, 0] [0, 0, 0, 0, 0, 3, 0, 0, 0], + .pm [32, 33, 34, 4, 8, 48, 64, 128, 256] [3, 5, 8, 16, 33, 1, 64, 128, 256], + .cg 1 true, + .pm [3, 5, 8, 16, 33, 1, 64, 128, 256] [32, 33, 34, 4, 8, 48, 64, 128, 256], + .dg [32, 32, 0, 0, 32, 51, 0, 0, 0] [0, 0, 0, 0, 0, 1, 0, 0, 0]] + +/-- `canon 9 pair2.U`, evaluated. -/ +def fU2 : List Gate := + [.dg [50, 51, 0, 0, 51, 51, 0, 0, 0] [0, 3, 0, 0, 3, 3, 0, 0, 0], + .pm [256, 128, 64, 32, 16, 8, 4, 2, 51] [408, 128, 64, 32, 16, 8, 4, 2, 1], + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .cg 128 true, + .pm [408, 128, 64, 32, 16, 8, 4, 2, 1] [256, 128, 64, 32, 16, 8, 4, 2, 51], + .dg [50, 51, 0, 0, 51, 51, 0, 0, 0] [0, 1, 0, 0, 1, 1, 0, 0, 0]] + +/-- `pair2.L.gates`, evaluated. -/ +def wL2 : List Gate := + [.dg [3, 3, 0, 0, 0, 0, 0, 0, 0] [3, 3, 2, 2, 2, 2, 2, 0, 0], + .pm [128, 259, 4, 8, 1, 2, 16, 32, 64] [16, 32, 4, 8, 64, 128, 256, 1, 50], + .xg 0, + .ph 0] + +/-- `pair2.R.gates`, evaluated. -/ +def wR2 : List Gate := + [.dg [18, 1, 0, 0, 49, 48, 0, 0, 0] [2, 0, 2, 2, 3, 3, 2, 2, 2], + .pm [50, 2, 4, 8, 64, 128, 256, 19, 32] [385, 2, 4, 8, 259, 256, 16, 32, 64], + .xg 511, + .ph 1] + +/-- `lhsC pair2`, evaluated. -/ +def lhsLit2 : List Gate := + [.dg [32, 32, 0, 0, 32, 51, 0, 0, 0] [0, 0, 0, 0, 0, 3, 0, 0, 0], + .pm [32, 33, 34, 4, 8, 48, 64, 128, 256] [3, 5, 8, 16, 33, 1, 64, 128, 256], + .cg 1 false, + .pm [3, 5, 8, 16, 33, 1, 64, 128, 256] [32, 33, 34, 4, 8, 48, 64, 128, 256], + .dg [32, 32, 0, 0, 32, 51, 0, 0, 0] [0, 0, 0, 0, 0, 1, 0, 0, 0], + .dg [50, 51, 0, 0, 51, 51, 0, 0, 0] [0, 3, 0, 0, 3, 3, 0, 0, 0], + .pm [256, 128, 64, 32, 16, 8, 4, 2, 51] [408, 128, 64, 32, 16, 8, 4, 2, 1], + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .cg 128 true, + .pm [408, 128, 64, 32, 16, 8, 4, 2, 1] [256, 128, 64, 32, 16, 8, 4, 2, 51], + .dg [50, 51, 0, 0, 51, 51, 0, 0, 0] [0, 1, 0, 0, 1, 1, 0, 0, 0]] + +/-- `rhsC pair2`, evaluated. -/ +def rhsLit2 : List Gate := + [.dg [18, 1, 0, 0, 49, 48, 0, 0, 0] [2, 0, 2, 2, 3, 3, 2, 2, 2], + .pm [50, 2, 4, 8, 64, 128, 256, 19, 32] [385, 2, 4, 8, 259, 256, 16, 32, 64], + .xg 511, + .ph 1, + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .dg [3, 3, 0, 0, 0, 0, 0, 0, 0] [3, 3, 2, 2, 2, 2, 2, 0, 0], + .pm [128, 259, 4, 8, 1, 2, 16, 32, 64] [16, 32, 4, 8, 64, 128, 256, 1, 50], + .xg 0, + .ph 0] + +/-- `canon 9 pair3.E`, evaluated. -/ +def fE3 : List Gate := + [.dg [0, 16, 16, 16, 30, 0, 0, 0, 0] [0, 0, 0, 0, 3, 0, 0, 0, 0], + .pm [16, 1, 18, 20, 24, 32, 64, 128, 256] [2, 5, 9, 17, 1, 32, 64, 128, 256], + .cg 1 true, + .pm [2, 5, 9, 17, 1, 32, 64, 128, 256] [16, 1, 18, 20, 24, 32, 64, 128, 256], + .dg [0, 16, 16, 16, 30, 0, 0, 0, 0] [0, 0, 0, 0, 1, 0, 0, 0, 0]] + +/-- `canon 9 pair3.U`, evaluated. -/ +def fU3 : List Gate := + [.dg [0, 28, 30, 30, 30, 0, 0, 0, 0] [0, 0, 3, 3, 3, 0, 0, 0, 0], + .pm [256, 128, 64, 32, 16, 8, 4, 1, 30] [128, 368, 64, 32, 16, 8, 4, 2, 1], + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .cg 128 true, + .pm [128, 368, 64, 32, 16, 8, 4, 2, 1] [256, 128, 64, 32, 16, 8, 4, 1, 30], + .dg [0, 28, 30, 30, 30, 0, 0, 0, 0] [0, 0, 1, 1, 1, 0, 0, 0, 0]] + +/-- `pair3.L.gates`, evaluated. -/ +def wL3 : List Gate := + [.dg [0, 6, 6, 0, 0, 0, 0, 0, 0] [2, 3, 3, 2, 2, 2, 2, 0, 0], + .pm [1, 128, 262, 2, 4, 8, 16, 32, 64] [1, 8, 16, 32, 64, 128, 256, 2, 28], + .xg 0, + .ph 0] + +/-- `pair3.R.gates`, evaluated. -/ +def wR3 : List Gate := + [.dg [0, 12, 2, 26, 24, 0, 0, 0, 0] [2, 2, 0, 3, 3, 2, 2, 2, 2], + .pm [1, 28, 4, 32, 64, 128, 256, 14, 16] [1, 386, 4, 262, 256, 8, 16, 32, 64], + .xg 511, + .ph 1] + +/-- `lhsC pair3`, evaluated. -/ +def lhsLit3 : List Gate := + [.dg [0, 16, 16, 16, 30, 0, 0, 0, 0] [0, 0, 0, 0, 3, 0, 0, 0, 0], + .pm [16, 1, 18, 20, 24, 32, 64, 128, 256] [2, 5, 9, 17, 1, 32, 64, 128, 256], + .cg 1 false, + .pm [2, 5, 9, 17, 1, 32, 64, 128, 256] [16, 1, 18, 20, 24, 32, 64, 128, 256], + .dg [0, 16, 16, 16, 30, 0, 0, 0, 0] [0, 0, 0, 0, 1, 0, 0, 0, 0], + .dg [0, 28, 30, 30, 30, 0, 0, 0, 0] [0, 0, 3, 3, 3, 0, 0, 0, 0], + .pm [256, 128, 64, 32, 16, 8, 4, 1, 30] [128, 368, 64, 32, 16, 8, 4, 2, 1], + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .cg 128 true, + .pm [128, 368, 64, 32, 16, 8, 4, 2, 1] [256, 128, 64, 32, 16, 8, 4, 1, 30], + .dg [0, 28, 30, 30, 30, 0, 0, 0, 0] [0, 0, 1, 1, 1, 0, 0, 0, 0]] + +/-- `rhsC pair3`, evaluated. -/ +def rhsLit3 : List Gate := + [.dg [0, 12, 2, 26, 24, 0, 0, 0, 0] [2, 2, 0, 3, 3, 2, 2, 2, 2], + .pm [1, 28, 4, 32, 64, 128, 256, 14, 16] [1, 386, 4, 262, 256, 8, 16, 32, 64], + .xg 511, + .ph 1, + .cg 1 true, + .cg 2 true, + .cg 4 true, + .cg 8 true, + .cg 16 true, + .cg 32 true, + .cg 64 true, + .dg [0, 6, 6, 0, 0, 0, 0, 0, 0] [2, 3, 3, 2, 2, 2, 2, 0, 0], + .pm [1, 128, 262, 2, 4, 8, 16, 32, 64] [1, 8, 16, 32, 64, 128, 256, 2, 28], + .xg 0, + .ph 0] + +theorem find1 : findPair pair1.E pair1.U = some pair1 := by decide +kernel +theorem find2 : findPair pair2.E pair2.U = some pair2 := by decide +kernel +theorem find3 : findPair pair3.E pair3.U = some pair3 := by decide +kernel + +theorem lits1 : canon 9 pair1.E = fE1 ∧ canon 9 pair1.U = fU1 ∧ pair1.L.gates = wL1 ∧ + pair1.R.gates = wR1 ∧ lhsC pair1 = lhsLit1 ∧ rhsC pair1 = rhsLit1 := by decide +kernel +theorem lits2 : canon 9 pair2.E = fE2 ∧ canon 9 pair2.U = fU2 ∧ pair2.L.gates = wL2 ∧ + pair2.R.gates = wR2 ∧ lhsC pair2 = lhsLit2 ∧ rhsC pair2 = rhsLit2 := by decide +kernel +theorem lits3 : canon 9 pair3.E = fE3 ∧ canon 9 pair3.U = fU3 ∧ pair3.L.gates = wL3 ∧ + pair3.R.gates = wR3 ∧ lhsC pair3 = lhsLit3 ∧ rhsC pair3 = rhsLit3 := by decide +kernel + +theorem ok1 : cOk 512 fE1 = true ∧ cOk 512 fU1 = true ∧ cOk 512 wL1 = true ∧ cOk 512 wR1 = true := by + decide +kernel +theorem ok2 : cOk 512 fE2 = true ∧ cOk 512 fU2 = true ∧ cOk 512 wL2 = true ∧ cOk 512 wR2 = true := by + decide +kernel +theorem ok3 : cOk 512 fE3 = true ∧ cOk 512 fU3 = true ∧ cOk 512 wL3 = true ∧ cOk 512 wR3 = true := by + decide +kernel + +theorem check1 : check lhsLit1 rhsLit1 = true := by decide +kernel +theorem check2 : check lhsLit2 rhsLit2 = true := by decide +kernel +theorem check3 : check lhsLit3 rhsLit3 = true := by decide +kernel + +/-- (N) from the literal checks of a pair. -/ +theorem exact_N_of_lits (p : Pair) (hf : findPair p.E p.U = some p) {fE fU wL wR lhs rhs : List Gate} + (hl : canon 9 p.E = fE ∧ canon 9 p.U = fU ∧ p.L.gates = wL ∧ p.R.gates = wR ∧ lhsC p = lhs ∧ + rhsC p = rhs) + (hok : cOk 512 fE = true ∧ cOk 512 fU = true ∧ cOk 512 wL = true ∧ cOk 512 wR = true) + (hc : check lhs rhs = true) (v : A ⊗[ℂ] B) : + T p.U ((T p.E).symm v) = Lw p.E p.U (C7.rTensor B (Rw p.E p.U v)) := by + obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hl + obtain ⟨k1, k2, k3, k4⟩ := hok + exact exact_N_of_check p hf (h1 ▸ k1) (h2 ▸ k2) (h3 ▸ k3) (h4 ▸ k4) (h5 ▸ h6 ▸ hc) v + +/-- **(N) for pair 1**, exactly, global phase included. -/ +theorem exact_N_pair1 (v : A ⊗[ℂ] B) : + T pair1.U ((T pair1.E).symm v) = Lw pair1.E pair1.U (C7.rTensor B (Rw pair1.E pair1.U v)) := + exact_N_of_lits pair1 find1 lits1 ok1 check1 v + +theorem exact_N_pair2 (v : A ⊗[ℂ] B) : + T pair2.U ((T pair2.E).symm v) = Lw pair2.E pair2.U (C7.rTensor B (Rw pair2.E pair2.U v)) := + exact_N_of_lits pair2 find2 lits2 ok2 check2 v + +theorem exact_N_pair3 (v : A ⊗[ℂ] B) : + T pair3.U ((T pair3.E).symm v) = Lw pair3.E pair3.U (C7.rTensor B (Rw pair3.E pair3.U v)) := + exact_N_of_lits pair3 find3 lits3 ok3 check3 v + +/-- (N) for every certified pair. -/ +theorem exact_N {E U : List ℕ} (h : (E, U) ∈ pairs.map fun p => (p.E, p.U)) (v : A ⊗[ℂ] B) : + T U ((T E).symm v) = Lw E U (C7.rTensor B (Rw E U v)) := by + simp only [pairs, List.map_cons, List.map_nil, List.mem_cons, Prod.mk.injEq, + List.not_mem_nil, or_false] at h + rcases h with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact exact_N_pair1 v + · exact exact_N_pair2 v + · exact exact_N_pair3 v + +/-- Every word/pair instance is a certified pair. -/ +theorem nine_mem : ∀ q ∈ nineInstances, (q.2.2.2.1, q.2.2.2.2) ∈ pairs.map fun p => (p.E, p.U) := by + decide +kernel + +/-- **The nine word/pair identities** of the HPE words ck, atm3 and jp8. -/ +theorem exact_N_nine : ∀ q ∈ nineInstances, ∀ v : A ⊗[ℂ] B, + T q.2.2.2.2 ((T q.2.2.2.1).symm v) = + Lw q.2.2.2.1 q.2.2.2.2 (C7.rTensor B (Rw q.2.2.2.1 q.2.2.2.2 v)) := + fun q hq v => exact_N (nine_mem q hq) v + +/-! ## `hpe_word` without (N) -/ + +open LemmaG LemmaG.Stream LemmaA + +/-- **The HPE word, with (N) proved.** `hpe_word` for the tools' operators: frames are basis +lists, `T_F = canonical_frame(9, F)`, the wrappers are the `"E:U"` recipes and the residual is +`C₇ ⊗ id`. The exact factorization is no longer a hypothesis; the helper's pair only has to be +one of the certified pairs (`exact_N`). -/ +theorem hpe_word_exact {ι : Type*} [DecidableEq ι] [Fintype ι] + {Fam G Cc W : Type*} [DecidableEq Fam] [Group G] [DecidableEq G] + [AddCommMonoid W] [Module ℂ W] (ent term : ι → List ℕ) + (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 ≃ₗ[ℂ] (A ⊗[ℂ] B)) + (rec : XLab ι (List ℕ) → XLab ι (List ℕ) → A ⊗[ℂ] B → A ⊗[ℂ] B) + (h p : ι) (hp : h ≠ p) (Ah Ap : List ℕ) (q : ℂ) (l : ι → XLab ι (List ℕ)) + (a b : List (Event ι (XLab ι (List ℕ)) ℂ)) (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) + (hpair : (ent h, term h) ∈ pairs.map fun p => (p.E, p.U)) : + 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 (C7.rTensor B (chart h (y (streamOwner fam σ d h)))) := + hpe_word T ent term Lw Rw fam σ d fp hne hdis chart rec h p hp Ah Ap q l a b y ha lh lp hb hmv + hrec hS hstart C7 (exact_N hpair) + +end HyperplaneEnd.Exact 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/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..2afcca845b --- /dev/null +++ b/research/hyperplane-end-lean/NOTICE.md @@ -0,0 +1,19 @@ +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). + +`HyperplaneEnd/Clifford.lean` and `HyperplaneEnd/Exact.lean` prove hypothesis (N) for the HPE words' `(E, U)` pairs. Their +gate semantics, `canonical_frame` (`basis_extend`, `inv`, the quadratic form) and `parity`/`mv`/`qvalue` are ports of +`clifford_exact.py` (as vendored in `research/split-centres-global`, icekylinx); `monomial_op` and the `"E:U"` recipe +data are from the HPE wrapper tool `adapters_local.py` (DreamingOfClouds, following PR #458, chafreaky). The packed +kernel check is new; the balanced-split/packed-`Nat` approach to kernel-only checking follows the LeanRoadmap probe. diff --git a/research/hyperplane-end-lean/PROOF.md b/research/hyperplane-end-lean/PROOF.md new file mode 100644 index 0000000000..5778e630f1 --- /dev/null +++ b/research/hyperplane-end-lean/PROOF.md @@ -0,0 +1,168 @@ +# 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|`. (N) itself is proved in Lean for the +three `(E, U)` pairs those words use (§4a), so `hpe_word_exact` states the HPE word theorem without it. + +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 | **proved in Lean** for the three pairs of the HPE words (§4a, `Exact.exact_N`); `hpe_word_exact` has no (N) hypothesis | +| `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/`) | + +## 4a. (N) in Lean (`HyperplaneEnd/Clifford.lean`, `HyperplaneEnd/Exact.lean`) + +The ck, atm3 and jp8 words have 3 `(E, U)` pairs each, and the nine pairs are the same three frame pairs with the same +three `"E:U"` recipes (every `RESIDUAL-ADAPTERS.json` of the HPE runs carries exactly these three). (N) is proved +for them, exactly over `ℂ`, global phase included. + +* **Operators.** `clifford_exact.py` builds every operator as a literal circuit of five gates on `ℂ^{2⁹}`: + `P G` (`v'(Gx) = v(x)`), `D Q α` (`i^{q(x)}`), `C q s` (`((1 + s i) v(x) + (1 − s i) v(x ⊕ q)) / 2`), `X b`, + and a global phase. [`Clifford.gC`, `gL`, `cL`] give them exact `ℂ`-linear semantics; [`gL_adj`, `cE`] prove that + `Op.adjoint`'s gate inverses invert them (side conditions `Gate.ok`, decided by the kernel). [`Exact.canon`] ports + `canonical_frame` (`basis_extend`, `inv`, the quadratic form), [`Mono.gates`] ports `monomial_op`, and + [`Exact.T`, `Lw`, `Rw`] are these operators on `A ⊗ B = ℂ^128 ⊗ ℂ^4` (qubits 0–6, spectators 7–8) via + [`eT`]; the residual is [`C7`] `= fourier(7)` and [`rTensor_C7`] shows `C7 ⊗ id` is `fourier(9, range 7)`. +* **The packed check** [`Clifford.check`, `cL_eq_of_check`]. Dropping the `1/2` of each `C` gate gives integer + semantics over `ℤ[i]` [`gz`] with `gC (φ ∘ v) = (1/2)^{#C} φ ∘ gz v` [`cL_emb`]. `check c₁ c₂` runs both circuits once + on `u(x) = B^x`, `B = 4^{#C(c₁)+1}`; by linearity this is `Σ_y B^y M(e_y)`, every column at once. Entries are bounded + by `4^{#C}` [`runZ_bnd`], so base-`B` digits are unique [`digits_eq_zero`] and `check = true` gives + `M₁ = 2^{#C(c₁)−#C(c₂)} M₂` entrywise, hence `cL c₁ = cL c₂` on `ℂ^512`. +* **Kernel facts** (`decide +kernel`; no `native_decide`): `canon`/`Mono.gates` evaluate to the gate literals + `fE1 … rhsLit3` [`lits1/2/3`], all gates satisfy `Gate.ok` [`ok1/2/3`], and [`check1/2/3`] pass. +* **Results.** [`exact_N_pair1/2/3`], [`exact_N`] (any certified pair), [`exact_N_nine`] (the nine word/pair + instances), and [`hpe_word_exact`]: `hpe_word` for these operators with (N) discharged; its only extra hypothesis is + that `(ent h, term h)` is a certified pair, which `code/check_hpe_pairs.py` and the tools' frame data establish. + +**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 + named results depend on a subset of these (`PrintAxioms.lean`); the kernel checks use `decide +kernel` only. +* The Lemma A and Lemma G packages, built here from source. +* The HPE tools' exact checks of the remaining hypotheses in §4 (all but (N)). + +## 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). diff --git a/research/hyperplane-end-lean/PrintAxioms.lean b/research/hyperplane-end-lean/PrintAxioms.lean new file mode 100644 index 0000000000..3150cd1deb --- /dev/null +++ b/research/hyperplane-end-lean/PrintAxioms.lean @@ -0,0 +1,29 @@ +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.Clifford.par9_spec +#print axioms HyperplaneEnd.Clifford.cE +#print axioms HyperplaneEnd.Clifford.cL_emb +#print axioms HyperplaneEnd.Clifford.cL_eq_of_check +#print axioms HyperplaneEnd.Exact.rTensor_C7 +#print axioms HyperplaneEnd.Exact.exact_N_of_check +#print axioms HyperplaneEnd.Exact.check1 +#print axioms HyperplaneEnd.Exact.check2 +#print axioms HyperplaneEnd.Exact.check3 +#print axioms HyperplaneEnd.Exact.exact_N_pair1 +#print axioms HyperplaneEnd.Exact.exact_N_pair2 +#print axioms HyperplaneEnd.Exact.exact_N_pair3 +#print axioms HyperplaneEnd.Exact.exact_N +#print axioms HyperplaneEnd.Exact.exact_N_nine +#print axioms HyperplaneEnd.Exact.hpe_word_exact 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..05aaa23905 --- /dev/null +++ b/research/hyperplane-end-lean/code/check_hpe_pairs.py @@ -0,0 +1,95 @@ +# 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; + * (N) is proved in Lean for the pair: its basis rows (frames[E], frames[U]) are one of LEAN_PAIRS, the pairs of + `HyperplaneEnd.Exact.pairs` (`exact_N`, `hpe_word_exact`). +Python 3.9+, standard library only.""" +import copy, gzip, json, sys +from pathlib import Path + + +# (E rows, U rows) of HyperplaneEnd/Exact.lean `pair1`, `pair2`, `pair3` +LEAN_PAIRS = {((45,), (256, 128, 64, 33, 16, 9, 5, 2)), ((51,), (256, 128, 64, 33, 17, 8, 4, 3)), + ((30,), (256, 128, 64, 32, 18, 10, 6, 1))} + + +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")}') + if (tuple(frames[E]), tuple(frames[U])) not in LEAN_PAIRS: viol.append(f'helper {h}: pair ({E},{U}) not proved in Lean') + 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..4323aaa9fa --- /dev/null +++ b/research/hyperplane-end-lean/verify.py @@ -0,0 +1,73 @@ +# 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; + HyperplaneEnd.Exact runs the kernel checks of (N) with `decide +kernel`, several minutes and several GB); + 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()