From 7bc75aec50ff808a8781620729c02efdf1ff2e7c Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 20:12:01 -0400 Subject: [PATCH] =?UTF-8?q?refactor(treeeval):=20derive=20the=20binary=20C?= =?UTF-8?q?ook=E2=80=93Mertz=20procedure=20from=20fan-in=20d?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove the step-exact bridge `Cslib.TreeEval.Ary.proc_ofBinary`: on a binary tree embedded with fan-in 2, the fan-in-d procedure `Ary.proc us` is the binary procedure `proc us` (an equality of functions on the same state type, since `Ary.State K 2 ℓ` and `State K ℓ` are both `Fin 3 → Fin ℓ → K`). The rounds agree definitionally except for the gate update, where the two multilinear extensions differ only by a renaming of their variables; this uses the new general lemma `Cslib.BitString.rename_multilinearExtension`. The binary `proc_eq`, `proc_zero` and `embed_eval_eq_proc` are now the case d = 2 of their fan-in-d versions through the bridge, with unchanged statements. The binary mask-cancellation proof and its private helpers (`add_one_ne`, `add_two_ne`, `add_two_ne_add_one`, `gateRound_eq`, `foldl_gateRound_eq`) are removed. `Cslib.TreeEval.embed` moves (same name and signature) from TreeEval/CookMertz.lean to TreeEval/Ary/CookMertz.lean, which now imports MultilinearExtension and UnitSum directly instead of the binary file; the binary file imports the fan-in-d file. The binary definitions (`State`, `gatePoly`, `scale`, `gateUpdate`, `gateRound`, `proc`) are unchanged, since the iterative procedure and the read machine are specified by them. ROADMAP marks the bridge as done; TreeEvalAry tests apply it to a concrete instance and guard its axioms. Line delta: +113/-97 (binary CookMertz 195 -> 171 lines). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Computability/TreeEval/Ary/CookMertz.lean | 27 +++- .../Computability/TreeEval/CookMertz.lean | 138 ++++++++---------- .../BooleanAnalysis/MultilinearExtension.lean | 16 +- ComplexityTests/TreeEvalAry.lean | 20 ++- ROADMAP.md | 9 +- 5 files changed, 113 insertions(+), 97 deletions(-) diff --git a/Complexity/Computability/TreeEval/Ary/CookMertz.lean b/Complexity/Computability/TreeEval/Ary/CookMertz.lean index 9a15a04681..65a7d2643e 100644 --- a/Complexity/Computability/TreeEval/Ary/CookMertz.lean +++ b/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 diff --git a/Complexity/Computability/TreeEval/CookMertz.lean b/Complexity/Computability/TreeEval/CookMertz.lean index 9447787fa2..544f0a9e7c 100644 --- a/Complexity/Computability/TreeEval/CookMertz.lean +++ b/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 diff --git a/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean b/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean index 9493db3b68..5de569b8aa 100644 --- a/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean +++ b/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 diff --git a/ComplexityTests/TreeEvalAry.lean b/ComplexityTests/TreeEvalAry.lean index b561e5c003..4eb19c9c23 100644 --- a/ComplexityTests/TreeEvalAry.lean +++ b/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 diff --git a/ROADMAP.md b/ROADMAP.md index 12b60c1c85..7a1b4443c0 100644 --- a/ROADMAP.md +++ b/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