refactor(treeeval): derive the binary Cook–Mertz procedure from fan-in d

Complexity/Computability/TreeEval/Ary/CookMertz.lean

@@ -8,16 +8,19 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.TreeEval.Ary.Basic
-public import Complexity.Computability.TreeEval.CookMertz
+public import Complexity.Foundations.BooleanAnalysis.MultilinearExtension
+public import Complexity.Foundations.FieldTheory.Finite.UnitSum
 
 /-!
 # The Cook–Mertz procedure for Tree Evaluation with fan-in `d`
 
-This generalizes `Cslib.TreeEval.proc` from fan-in `2` to fan-in `d`. The procedure keeps `d + 1`
-registers, each holding `ℓ` elements of a finite field `K`, as global storage shared by all levels
-of the recursion. Called on a subtree, a coefficient `c` and a target register `t`, it adds `c`
-times the value of the subtree (read as `0`/`1` field elements) to register `t` and leaves the
-other `d` registers unchanged, whatever their contents.
+This generalizes the binary procedure `Cslib.TreeEval.proc` to fan-in `d`; at `d = 2` it is that
+procedure step for step (`Cslib.TreeEval.Ary.proc_ofBinary`, proved beside the binary procedure,
+which derives its correctness from this file). The procedure keeps `d + 1` registers, each
+holding `ℓ` elements of a finite field `K`, as global storage shared by all levels of the
+recursion. Called on a subtree, a coefficient `c` and a target register `t`, it adds `c` times the
+value of the subtree (read as `0`/`1` field elements) to register `t` and leaves the other `d`
+registers unchanged, whatever their contents.
 
 The child `j` of a target `t` uses the register `reg t j = t + (j + 1)`, so the `d` children use
 exactly the registers other than `t`; for `d = 2` these are the registers `t + 1` and `t + 2` of
@@ -32,6 +35,7 @@ This file proves correctness only; space bounds are separate.
 
 ## Main definitions
 
+* `Cslib.TreeEval.embed`: an `ℓ`-bit value read as `0`/`1` field elements, for any fan-in.
 * `Cslib.TreeEval.Ary.reg`: the register of a child.
 * `Cslib.TreeEval.Ary.gatePoly`: the multilinear extension of an output bit of a gate.
 * `Cslib.TreeEval.Ary.proc`: the procedure, parametrized by an enumeration of the units of `K`.
@@ -56,10 +60,15 @@ This file proves correctness only; space bounds are separate.
 
 open MvPolynomial Cslib.BitString
 
-namespace Cslib.TreeEval.Ary
+namespace Cslib.TreeEval
 
 variable {K : Type*} [Field K] {d ℓ : ℕ}
 
+/-- An `ℓ`-bit value read as `0`/`1` field elements. -/
+def embed (v : Fin ℓ → Bool) : Fin ℓ → K := fun i => bitVal K (v i)
+
+namespace Ary
+
 /-- The global storage: `d + 1` registers of `ℓ` field elements. -/
 abbrev State (K : Type*) (d ℓ : ℕ) := Fin (d + 1) → Fin ℓ → K
 
@@ -243,4 +252,6 @@ theorem embed_eval_eq_proc [DecidableEq K] (hK : d * ℓ < Fintype.card K - 1) {
   (proc_zero (Finset.nodup_toList _) (fun _ => Finset.mem_toList.mpr (Finset.mem_univ _)) hK T
     t).symm
 
-end Cslib.TreeEval.Ary
+end Ary
+
+end Cslib.TreeEval

Complexity/Computability/TreeEval/CookMertz.lean

@@ -7,9 +7,7 @@ Authors: Christian Reitwiessner
 module
 -- upstream: candidate
 
-public import Complexity.Computability.TreeEval.Basic
-public import Complexity.Foundations.BooleanAnalysis.MultilinearExtension
-public import Complexity.Foundations.FieldTheory.Finite.UnitSum
+public import Complexity.Computability.TreeEval.Ary.CookMertz
 
 /-!
 # The Cook–Mertz procedure for Tree Evaluation
@@ -27,8 +25,12 @@ scaling. Summed over all units, the masks cancel (`FiniteField.sum_units_eval_mu
 the extension has degree at most `2ℓ < |K| - 1`, and register `t` has gained `c • f v₀ v₁`.
 
 Only the recursion depth, the round counter and the stage within a round are local to a level;
-this is what makes the procedure space-efficient. This file proves its correctness; space bounds
-are separate.
+this is what makes the procedure space-efficient. It is the fan-in-`d` procedure
+`Cslib.TreeEval.Ary.proc` at `d = 2`, step for step, on the embedded tree: child `0` uses register
+`t + 1` and child `1` register `t + 2`, and the extensions of a binary gate and of its fan-in-`2`
+reading differ only by the naming of their variables. Its correctness is therefore the case
+`d = 2` of `Cslib.TreeEval.Ary.proc_eq`. This file proves correctness only; space bounds are
+separate.
 
 ## Main definitions
 
@@ -37,6 +39,8 @@ are separate.
 
 ## Main results
 
+* `Cslib.TreeEval.Ary.proc_ofBinary`: on an embedded binary tree, the fan-in-`d` procedure at
+  `d = 2` is the binary procedure.
 * `Cslib.TreeEval.proc_eq`: the procedure adds `c` times the value of the tree to the target
   register and leaves the other registers unchanged.
 * `Cslib.TreeEval.proc_zero`: started from zero registers, it leaves the value of the tree in the
@@ -62,9 +66,6 @@ variable {K : Type*} [Field K] {ℓ : ℕ}
 /-- The global storage: three registers of `ℓ` field elements. -/
 abbrev State (K : Type*) (ℓ : ℕ) := Fin 3 → Fin ℓ → K
 
-/-- An `ℓ`-bit value read as `0`/`1` field elements. -/
-def embed (v : Fin ℓ → Bool) : Fin ℓ → K := fun i => bitVal K (v i)
-
 /-- The multilinear extension of output bit `i` of a gate, in the bits of both inputs. -/
 noncomputable def gatePoly (f : Gate ℓ) (i : Fin ℓ) :
     MvPolynomial (Fin ℓ ⊕ Fin ℓ) K :=
@@ -98,56 +99,50 @@ noncomputable def proc (us : List Kˣ) :
   | _, .leaf v, c, t, S => Function.update S t (S t + c • embed v)
   | _, .node f l r, c, t, S => us.foldl (fun S u => gateRound (proc us l) (proc us r) f c t u S) S
 
-private theorem add_one_ne (t : Fin 3) : t + 1 ≠ t := by revert t; decide
-private theorem add_two_ne (t : Fin 3) : t + 2 ≠ t := by revert t; decide
-private theorem add_two_ne_add_one (t : Fin 3) : t + 2 ≠ t + 1 := by revert t; decide
-
-/-- A round, when both subtree procedures meet their specification, changes only the target
-register, subtracting `c` times the gate's extension at the masked children's values. -/
-private theorem gateRound_eq {pl pr : K → Fin 3 → State K ℓ → State K ℓ} {vl vr : Fin ℓ → K}
-    (hl : ∀ c t S, pl c t S = Function.update S t (S t + c • vl))
-    (hr : ∀ c t S, pr c t S = Function.update S t (S t + c • vr))
-    (f : Gate ℓ) (c : K) (t : Fin 3) (u : Kˣ)
-    (S : State K ℓ) :
-    gateRound pl pr f c t u S = Function.update S t fun i =>
-      S t i - c * eval (Sum.elim ((u : K) • S (t + 1) + vl) ((u : K) • S (t + 2) + vr))
-        (gatePoly f i) := by
-  have h1 := add_one_ne t
-  have h2 := add_two_ne t
-  have h21 := add_two_ne_add_one t
-  funext r i
-  simp only [gateRound, gateUpdate, hl, hr, scale, Function.update_apply]
-  by_cases hrt : r = t
-  · subst hrt
-    simp [h1.symm, h2.symm, h21, h21.symm]
-  by_cases hr1 : r = t + 1
-  · subst hr1
-    simp [h1, h21.symm]
-  by_cases hr2 : r = t + 2
-  · subst hr2
-    simp [h2, h21]
-  simp [hrt, hr1, hr2]
-
-/-- The rounds for all units in `us` change only the target register, subtracting `c` times
-the sum of the gate's extension at the masked children's values. -/
-private theorem foldl_gateRound_eq {pl pr : K → Fin 3 → State K ℓ → State K ℓ} {vl vr : Fin ℓ → K}
-    (hl : ∀ c t S, pl c t S = Function.update S t (S t + c • vl))
-    (hr : ∀ c t S, pr c t S = Function.update S t (S t + c • vr))
-    (f : Gate ℓ) (c : K) (t : Fin 3) (us : List Kˣ)
-    (S : State K ℓ) :
-    us.foldl (fun S u => gateRound pl pr f c t u S) S = Function.update S t fun i =>
-      S t i - c * (us.map fun u : Kˣ =>
-        eval (Sum.elim ((u : K) • S (t + 1) + vl) ((u : K) • S (t + 2) + vr))
-          (gatePoly f i)).sum := by
-  induction us generalizing S with
-  | nil => simp
-  | cons u us ih =>
-    rw [List.foldl_cons, gateRound_eq hl hr, ih, Function.update_of_ne (add_one_ne t),
-      Function.update_of_ne (add_two_ne t), Function.update_idem, Function.update_self]
-    congr 1
-    funext i
-    simp only [List.map_cons, List.sum_cons]
-    ring
+/-- The coordinates of the two inputs of a binary gate as the coordinates of the two children of
+a gate of fan-in `2`. -/
+private def sumEquivProd (ℓ : ℕ) : Fin ℓ ⊕ Fin ℓ ≃ Fin 2 × Fin ℓ :=
+  (Equiv.boolProdEquivSum _).symm.trans (finTwoEquiv.symm.prodCongr (Equiv.refl _))
+
+/-- The extension of a binary gate is that of its fan-in-`2` reading, up to naming the
+variables. -/
+private theorem rename_gatePoly (f : Gate ℓ) (i : Fin ℓ) :
+    rename (sumEquivProd ℓ) (gatePoly (K := K) f i) = Ary.gatePoly (Ary.Gate.ofBinary f) i := by
+  rw [gatePoly, rename_multilinearExtension]
+  rfl
+
+/-- The update of a round of fan-in `2` is the binary update. -/
+private theorem gateUpdate_ofBinary (f : Gate ℓ) (c : K) (t : Fin 3) (S : State K ℓ) :
+    Ary.gateUpdate (Ary.Gate.ofBinary f) c t S = gateUpdate f c t S := by
+  have hS : (fun q => S (Ary.reg t q.1) q.2) ∘ sumEquivProd ℓ =
+      Sum.elim (S (t + 1)) (S (t + 2)) := by
+    funext x
+    cases x <;> rfl
+  simp only [Ary.gateUpdate, gateUpdate, ← rename_gatePoly, eval_rename, hS]
+
+/-- A round of fan-in `2` performs the calls, the update and the scalings of a binary round, in
+the same order. -/
+private theorem gateRound_ofBinary (pl pr : K → Fin 3 → State K ℓ → State K ℓ) (f : Gate ℓ)
+    (c : K) (t : Fin 3) (u : Kˣ) (S : State K ℓ) :
+    Ary.gateRound ![pl, pr] (Ary.Gate.ofBinary f) c t u S = gateRound pl pr f c t u S := by
+  simp only [Ary.gateRound, gateRound, gateUpdate_ofBinary]
+  rfl
+
+/-- **The binary procedure is the fan-in-`d` procedure at `d = 2`.** On a binary tree embedded
+with fan-in `2`, the fan-in-`d` procedure is the binary procedure, step for step: it acts on the
+same three registers (`Fin (2 + 1)` is `Fin 3`), calls the children in the same order with the
+same coefficients and target registers, and performs the same updates and scalings. -/
+theorem Ary.proc_ofBinary (us : List Kˣ) {h : ℕ} (T : TreeEval.Tree ℓ h) :
+    Ary.proc us (Ary.Tree.ofBinary T) = TreeEval.proc us T := by
+  induction T with
+  | leaf v => rfl
+  | node f l r ihl ihr =>
+    funext c t S
+    have hch : (fun j => Ary.proc us (![Ary.Tree.ofBinary l, Ary.Tree.ofBinary r] j)) =
+        ![TreeEval.proc us l, TreeEval.proc us r] := by
+      funext j
+      fin_cases j <;> assumption
+    simp only [Ary.Tree.ofBinary, Ary.proc, TreeEval.proc, hch, gateRound_ofBinary]
 
 variable [Fintype K]
 
@@ -157,39 +152,20 @@ target register and leaves the other registers unchanged, whatever their initial
 theorem proc_eq {us : List Kˣ} (hnd : us.Nodup) (hmem : ∀ u, u ∈ us)
     (hK : 2 * ℓ < Fintype.card K - 1) {h : ℕ} (T : Tree ℓ h) (c : K) (t : Fin 3)
     (S : State K ℓ) : proc us T c t S = Function.update S t (S t + c • embed T.eval) := by
-  classical
-  induction T generalizing c t S with
-  | leaf v => rfl
-  | node f l r ihl ihr =>
-    rw [proc, foldl_gateRound_eq ihl ihr]
-    congr 1
-    funext i
-    have hdeg : (gatePoly (K := K) f i).totalDegree < Fintype.card K - 1 :=
-      (totalDegree_multilinearExtension_le _).trans_lt <| by simpa [two_mul] using hK
-    rw [← List.sum_toFinset _ hnd, show us.toFinset = Finset.univ by ext; simp [hmem]]
-    have hsum := FiniteField.sum_units_eval_mul_add hdeg
-      (Sum.elim (S (t + 1)) (S (t + 2))) (fun j => bitVal K (Sum.elim l.eval r.eval j))
-    have hpt (u : Kˣ) : Sum.elim ((u : K) • S (t + 1) + embed l.eval)
-        ((u : K) • S (t + 2) + embed r.eval) = fun j => (u : K) *
-          Sum.elim (S (t + 1)) (S (t + 2)) j + bitVal K (Sum.elim l.eval r.eval j) := by
-      funext j; cases j <;> rfl
-    simp only [hpt]
-    rw [hsum, gatePoly, eval_multilinearExtension]
-    simp [embed]
+  rw [← Ary.proc_ofBinary, Ary.proc_eq hnd hmem hK, Ary.Tree.eval_ofBinary]
 
 /-- Started from zero registers, the procedure leaves the value of the tree in the target
 register. -/
 theorem proc_zero {us : List Kˣ} (hnd : us.Nodup) (hmem : ∀ u, u ∈ us)
     (hK : 2 * ℓ < Fintype.card K - 1) {h : ℕ} (T : Tree ℓ h) (t : Fin 3) :
     proc us T 1 t 0 t = embed T.eval := by
-  simp [proc_eq hnd hmem hK]
+  rw [← Ary.proc_ofBinary, Ary.proc_zero hnd hmem hK, Ary.Tree.eval_ofBinary]
 
 /-- **Tree Evaluation by the Cook–Mertz procedure.** Run over the units of `K` in any order with
 `2ℓ < |K| - 1`, from zero registers, the procedure computes the value of the tree into the
 target register. -/
 theorem embed_eval_eq_proc [DecidableEq K] (hK : 2 * ℓ < Fintype.card K - 1) {h : ℕ} (T : Tree ℓ h)
-    (t : Fin 3) : embed T.eval = proc (Finset.univ : Finset Kˣ).toList T 1 t 0 t :=
-  (proc_zero (Finset.nodup_toList _) (fun _ => Finset.mem_toList.mpr (Finset.mem_univ _)) hK T
-    t).symm
+    (t : Fin 3) : embed T.eval = proc (Finset.univ : Finset Kˣ).toList T 1 t 0 t := by
+  rw [← Ary.proc_ofBinary, ← Ary.embed_eval_eq_proc hK, Ary.Tree.eval_ofBinary]
 
 end Cslib.TreeEval

Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean

@@ -30,6 +30,8 @@ Its total degree is at most the dimension.
 * `Cslib.BitString.eval_multilinearExtension`: the extension agrees with the function on the cube.
 * `Cslib.BitString.totalDegree_multilinearExtension_le`: its total degree is at most the
   dimension.
+* `Cslib.BitString.rename_multilinearExtension`: renaming the coordinates along an equivalence
+  gives the multilinear extension of the function read through the equivalence.
 
 ## References
 
@@ -43,7 +45,7 @@ open MvPolynomial
 
 namespace Cslib.BitString
 
-variable {ι R : Type*} [CommRing R]
+variable {ι κ R : Type*} [CommRing R]
 
 /-- The indicator polynomial of a point `a` of the cube: the product of `X i` where `a i` is true
 and of `1 - X i` where it is false. -/
@@ -96,4 +98,16 @@ theorem totalDegree_multilinearExtension_le [Fintype ι] [DecidableEq ι] (g : (
   exact (totalDegree_mul _ _).trans <| by
     simpa using totalDegree_indicatorPoly_le (R := R) a
 
+/-- Renaming the coordinates along an equivalence `e` turns the multilinear extension of `g` into
+the multilinear extension of `g` read through `e`. -/
+theorem rename_multilinearExtension [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
+    (e : ι ≃ κ) (g : (ι → Bool) → R) :
+    rename e (multilinearExtension g) = multilinearExtension fun z => g (z ∘ e) := by
+  simp only [multilinearExtension, indicatorPoly, map_sum, map_mul, rename_C, map_prod,
+    apply_ite (rename e), rename_X, map_sub, map_one]
+  refine Fintype.sum_equiv (e.arrowCongr (Equiv.refl Bool)) _ _ fun a => ?_
+  congr 1
+  · simp [Equiv.arrowCongr, Function.comp_assoc]
+  · exact Fintype.prod_equiv e _ _ fun i => by simp [Equiv.arrowCongr]
+
 end Cslib.BitString

ComplexityTests/TreeEvalAry.lean

@@ -4,15 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Reitwiessner
 -/
 
-import Complexity.Computability.TreeEval.Ary.CookMertz
+import Complexity.Computability.TreeEval.CookMertz
 
 /-!
 # Tree Evaluation with fan-in `d`
 
 A ternary instance evaluated directly, and the Cook–Mertz procedure over `ZMod 11` on two-bit
 values: the field-size hypothesis `d * ℓ < |K| - 1` holds, as `3 * 2 < 10`, so the correctness
-theorem is not vacuous. A binary instance embedded with fan-in `2` keeps its value, and the
-fan-in-`2` procedure over `ZMod 7` computes it.
+theorem is not vacuous. A binary instance embedded with fan-in `2` keeps its value, the
+fan-in-`2` procedure over `ZMod 7` computes it, and on it the fan-in-`2` procedure is the binary
+procedure.
 -/
 
 namespace ComplexityTests.TreeEvalAry
@@ -67,6 +68,13 @@ example : Ary.proc (Finset.univ : Finset (ZMod 7)ˣ).toList (Ary.Tree.ofBinary b
   congr 1
   decide
 
+/-- On the embedded binary instance, the fan-in-`2` procedure over `ZMod 7` is the binary
+procedure, for every coefficient, target register and contents of the registers. -/
+example (c : ZMod 7) (t : Fin 3) (S : Cslib.TreeEval.State (ZMod 7) 2) :
+    Ary.proc (Finset.univ : Finset (ZMod 7)ˣ).toList (Ary.Tree.ofBinary binarySample) c t S =
+      Cslib.TreeEval.proc (Finset.univ : Finset (ZMod 7)ˣ).toList binarySample c t S := by
+  rw [Ary.proc_ofBinary]
+
 /--
 info: 'Cslib.TreeEval.Ary.proc_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -79,4 +87,10 @@ info: 'Cslib.TreeEval.Ary.embed_eval_eq_proc' depends on axioms: [propext, Class
 #guard_msgs in
 #print axioms Cslib.TreeEval.Ary.embed_eval_eq_proc
 
+/--
+info: 'Cslib.TreeEval.Ary.proc_ofBinary' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms Cslib.TreeEval.Ary.proc_ofBinary
+
 end ComplexityTests.TreeEvalAry

ROADMAP.md

@@ -1418,12 +1418,13 @@ space bounds. Further class-level work needs resource certificates for the actua
   `1 ≤ H`); malformed-input handling and the refined `O(ℓ + H log(ℓ + 2))` parameter bound
   remain outstanding. Toward Williams's `TIME[t] ⊆ SPACE[√(t log t)]` (#361), the
   [fan-in-`d` procedure](Complexity/Computability/TreeEval/Ary/CookMertz.lean) is proved correct
-  over `d + 1` registers when `d · ℓ < |K| - 1` (milestone M1), and implicit Tree Evaluation (#367)
-  starts from
+  over `d + 1` registers when `d · ℓ < |K| - 1` (milestone M1); at `d = 2` it is the binary
+  procedure step for step, whose correctness is derived from it
+  ([`Ary.proc_ofBinary`](Complexity/Computability/TreeEval/CookMertz.lean)). Implicit Tree
+  Evaluation (#367) starts from
   [query machines in the space of their states](Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean),
   which charge neither the input nor the output; the fan-in-`d` space bound, subroutine calls for
-  implicit gates and leaves, a step-exact bridge to the binary procedure at `d = 2` (or deprecating
-  the binary copy), padding of non-perfect trees, and the remaining milestones are open;
+  implicit gates and leaves, padding of non-perfect trees, and the remaining milestones are open;
 * the space hierarchy below linear space: the
   [space hierarchy](Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean) and
   `L ⊊ PSPACE` are proved for space-constructible bounds `g` with `n ≤ g n`, and the textbook