From f3be9f4f73c7c61ceb7ef1d460bad0d6610a8274 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 00:55:50 -0400 Subject: [PATCH 1/6] feat(combinatorics): enumerate the tuples of bounded weight with a successor MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `budgetTuples ws p` lists the tuples of weight below `p` in lexicographic order and `budgetNext` is the successor that walks it from the zero tuple: the polynomial-delay enumeration of the mode exponents in §D.4.5 (p. 63) of the Boolean tensor contraction proof. `sum_filter_weight_lt_eq` turns a sum over the mode budget into a sum along the list. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Combinatorics/BudgetTuples.lean | 320 ++++++++++++++++++ .../Combinatorics/BudgetTuples.lean | 40 +++ 3 files changed, 361 insertions(+) create mode 100644 Complexity/Foundations/Combinatorics/BudgetTuples.lean create mode 100644 ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean diff --git a/Complexity.lean b/Complexity.lean index a501a6239..e4ec57b7e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2547,6 +2547,7 @@ public import Complexity.Foundations.Combinatorics.AffineDisperser.IndependentSo public import Complexity.Foundations.Combinatorics.AffineDisperser.Threshold public import Complexity.Foundations.Combinatorics.BalancedSchedules public import Complexity.Foundations.Combinatorics.BinomialTail +public import Complexity.Foundations.Combinatorics.BudgetTuples public import Complexity.Foundations.Combinatorics.CentralBinomial public import Complexity.Foundations.Combinatorics.DepthReduction public import Complexity.Foundations.Combinatorics.Expander.AffineFamily diff --git a/Complexity/Foundations/Combinatorics/BudgetTuples.lean b/Complexity/Foundations/Combinatorics/BudgetTuples.lean new file mode 100644 index 000000000..d520039bd --- /dev/null +++ b/Complexity/Foundations/Combinatorics/BudgetTuples.lean @@ -0,0 +1,320 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.Fintype.Pi +public import Mathlib.Data.List.Chain +import Mathlib.Algebra.BigOperators.Group.List.Basic +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Data.List.GetD +import Mathlib.Data.List.Nodup + +/-! +# Enumerating the tuples of bounded weight + +Give the coordinates of a tuple of natural numbers positive weights `ws`. The tuples of total +weight `∑ j, ws[j] * β[j] < p` (`weight`) are the exponent tuples of the modes in the proof of the +Boolean tensor contraction theorem of [OpenAI2026ETH] (§D.4.5, p. 63), where `p` is the +precision. The source enumerates them "with polynomial delay and space by ordering the variables +and successively choosing each exponent subject to the remaining budget". This file makes that +enumeration explicit: + +* `budgetTuples ws p` lists the tuples in lexicographic order, the first coordinate most + significant, by choosing each coordinate subject to the remaining budget; +* `budgetNext ws p β` is the successor of `β`: it advances the tail if it can, and otherwise + increments the coordinate and resets the tail to zero, which is feasible since every feasible + partial choice has the all-zero continuation. + +The list holds exactly the tuples of weight below `p` (`mem_budgetTuples`), each once +(`nodup_budgetTuples`). It starts at the zero tuple (`head?_budgetTuples`), each entry is followed +by its successor (`isChain_budgetTuples`), and the last one has none (`budgetNext_getLast?`). So +iterating `budgetNext` from zero visits every tuple once, with one successor computation, linear +in the number of coordinates, between consecutive tuples. + +## Main definitions + +* `Cslib.BudgetTuples.weight`: the weight of a tuple. +* `Cslib.BudgetTuples.headCount`: the number of feasible values of a coordinate. +* `Cslib.BudgetTuples.budgetTuples`: the tuples of weight below a budget, in lexicographic order. +* `Cslib.BudgetTuples.budgetNext`: the successor of a tuple. + +## Main results + +* `Cslib.BudgetTuples.mem_budgetTuples`, `Cslib.BudgetTuples.nodup_budgetTuples`: the list holds + each tuple of weight below the budget once. +* `Cslib.BudgetTuples.head?_budgetTuples`, `Cslib.BudgetTuples.isChain_budgetTuples`, + `Cslib.BudgetTuples.budgetNext_getLast?`: the successor walks the list from the zero tuple. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5, the enumeration + after (D.15), p. 63. +-/ + +public section + +namespace Cslib.BudgetTuples + +/-- The weight `∑ j, ws[j] * β[j]` of a tuple `β` for the weights `ws`. -/ +@[expose] def weight : List ℕ → List ℕ → ℕ + | w :: ws, b :: β => w * b + weight ws β + | _, _ => 0 + +/-- The number of values `b` of a coordinate of weight `w` with `w * b < p`, that is +`⌈p / w⌉` for `w > 0`. -/ +@[expose] def headCount (w p : ℕ) : ℕ := (p + w - 1) / w + +/-- A value fits the budget exactly when it is below `headCount`. -/ +theorem lt_headCount_iff {w p b : ℕ} (hw : 0 < w) : b < headCount w p ↔ w * b < p := by + rw [headCount, Nat.lt_iff_add_one_le, Nat.le_div_iff_mul_le hw, Nat.add_mul, Nat.one_mul, + Nat.mul_comm b w] + omega + +/-- **The tuples of weight below `p`**, in lexicographic order: the first coordinate takes each +value `b` with `w * b < p` in increasing order, and the rest is a tuple of weight below +`p - w * b`. -/ +@[expose] def budgetTuples : List ℕ → ℕ → List (List ℕ) + | [], p => if 0 < p then [[]] else [] + | w :: ws, p => (List.range (headCount w p)).flatMap fun b => + (budgetTuples ws (p - w * b)).map (b :: ·) + +/-- **The successor of a tuple**: advance the tail within its remaining budget if possible, and +otherwise increment the first coordinate and reset the tail to zero. -/ +@[expose] def budgetNext : List ℕ → ℕ → List ℕ → Option (List ℕ) + | w :: ws, p, b :: β => + match budgetNext ws (p - w * b) β with + | some β' => some (b :: β') + | none => if w * (b + 1) < p then some ((b + 1) :: List.replicate ws.length 0) else none + | _, _, _ => none + +/-! ### The tuples in the list -/ + +@[simp] theorem budgetTuples_nil (p : ℕ) : budgetTuples [] p = if 0 < p then [[]] else [] := rfl + +theorem budgetTuples_cons (w : ℕ) (ws : List ℕ) (p : ℕ) : + budgetTuples (w :: ws) p = (List.range (headCount w p)).flatMap fun b => + (budgetTuples ws (p - w * b)).map (b :: ·) := rfl + +@[simp] theorem weight_nil (β : List ℕ) : weight [] β = 0 := rfl + +@[simp] theorem weight_cons_cons (w : ℕ) (ws : List ℕ) (b : ℕ) (β : List ℕ) : + weight (w :: ws) (b :: β) = w * b + weight ws β := rfl + +/-- **The list holds exactly the tuples of weight below `p`**, for positive weights. -/ +theorem mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} {β : List ℕ} : + β ∈ budgetTuples ws p ↔ β.length = ws.length ∧ weight ws β < p := by + induction ws generalizing p β with + | nil => + simp only [budgetTuples_nil, weight_nil, List.length_nil, List.length_eq_zero_iff] + split_ifs with hp <;> simp [hp] + | cons w ws ih => + have hw0 : 0 < w := hw w List.mem_cons_self + have ih' := @ih (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) + rw [budgetTuples_cons] + simp only [List.mem_flatMap, List.mem_range, lt_headCount_iff hw0, List.mem_map] + constructor + · rintro ⟨b, hb, γ, hγ, rfl⟩ + rw [ih'] at hγ + simp only [List.length_cons, weight_cons_cons, hγ.1, true_and] + omega + · intro ⟨hlen, hwt⟩ + rcases β with _ | ⟨b, γ⟩ + · simp at hlen + · simp only [List.length_cons, Nat.add_right_cancel_iff, weight_cons_cons] at hlen hwt + exact ⟨b, by omega, γ, ih'.mpr ⟨hlen, by omega⟩, rfl⟩ + +/-- **Each tuple appears once.** -/ +theorem nodup_budgetTuples (ws : List ℕ) (p : ℕ) : (budgetTuples ws p).Nodup := by + induction ws generalizing p with + | nil => + simp only [budgetTuples_nil] + split_ifs <;> simp + | cons w ws ih => + rw [budgetTuples_cons, List.nodup_flatMap] + refine ⟨fun b _ => (ih _).map (List.cons_injective), ?_⟩ + refine (List.nodup_range).imp fun {b b'} hbb' => ?_ + intro x hx hy + simp only [List.mem_map] at hx hy + obtain ⟨γ, -, rfl⟩ := hx + obtain ⟨γ', -, h⟩ := hy + exact hbb' (List.cons.inj h).1.symm + +/-! ### The successor walks the list -/ + +private theorem getLast?_flatMap_range_succ {α : Type*} (f : ℕ → List α) (k : ℕ) + (hk : f k ≠ []) : ((List.range (k + 1)).flatMap f).getLast? = (f k).getLast? := by + rw [List.range_succ, List.flatMap_append, List.flatMap_singleton, List.getLast?_append] + cases h : (f k).getLast? with + | none => exact absurd (List.getLast?_eq_none_iff.mp h) hk + | some x => rfl + +private theorem isChain_flatMap_range {α : Type*} {R : α → α → Prop} (f : ℕ → List α) (n : ℕ) + (hne : ∀ b < n, f b ≠ []) (hblock : ∀ b < n, List.IsChain R (f b)) + (hjoin : ∀ b, b + 1 < n → ∀ x ∈ (f b).getLast?, ∀ y ∈ (f (b + 1)).head?, R x y) : + List.IsChain R ((List.range n).flatMap f) := by + induction n with + | zero => simp + | succ k ih => + rw [List.range_succ, List.flatMap_append, List.flatMap_singleton, List.isChain_append] + refine ⟨ih (fun b hb => hne b (by omega)) (fun b hb => hblock b (by omega)) + (fun b hb => hjoin b (by omega)), hblock k (by omega), ?_⟩ + intro x hx y hy + rcases k with _ | k + · simp at hx + · rw [getLast?_flatMap_range_succ f k (hne k (by omega))] at hx + exact hjoin k (by omega) x hx y hy + +/-- **The list starts at the zero tuple**, for positive weights and a positive budget. -/ +theorem head?_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} (hp : 0 < p) : + (budgetTuples ws p).head? = some (List.replicate ws.length 0) := by + induction ws generalizing p with + | nil => simp [hp] + | cons w ws ih => + have hw0 : 0 < w := hw w List.mem_cons_self + have ih' := @ih (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) + obtain ⟨k, hk⟩ : ∃ k, headCount w p = k + 1 := + Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp ((lt_headCount_iff hw0).mpr + (by simpa using hp))) + rw [budgetTuples_cons, hk, List.range_succ_eq_map, List.flatMap_cons, List.head?_append, + List.head?_map, Nat.mul_zero, Nat.sub_zero, ih' hp] + rfl + +/-- **The last tuple has no successor.** -/ +theorem budgetNext_getLast? {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} : + ∀ x ∈ (budgetTuples ws p).getLast?, budgetNext ws p x = none := by + induction ws generalizing p with + | nil => intro x _; rfl + | cons w ws ih => + have hw0 : 0 < w := hw w List.mem_cons_self + have ih' := @ih (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) + intro x hx + rw [budgetTuples_cons] at hx + rcases hn : headCount w p with _ | k + · rw [hn] at hx; simp at hx + · have hk : w * k < p := (lt_headCount_iff hw0).mp (by omega) + have hne : (budgetTuples ws (p - w * k)).map (k :: ·) ≠ [] := by + rw [Ne, List.map_eq_nil_iff, ← List.head?_eq_none_iff, + head?_budgetTuples (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) (by omega)] + simp + rw [hn, getLast?_flatMap_range_succ _ k hne, List.getLast?_map] at hx + obtain ⟨x', hx', rfl⟩ := Option.map_eq_some_iff.mp hx + have hnot : ¬ w * (k + 1) < p := fun h => by + have := (lt_headCount_iff hw0).mpr h; omega + simp only [budgetNext, ih' x' hx', hnot, ↓reduceIte] + +/-- **Each tuple is followed by its successor.** -/ +theorem isChain_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) (p : ℕ) : + List.IsChain (fun x y => budgetNext ws p x = some y) (budgetTuples ws p) := by + induction ws generalizing p with + | nil => + simp only [budgetTuples_nil] + split_ifs <;> simp + | cons w ws ih => + have hw0 : 0 < w := hw w List.mem_cons_self + have hws : ∀ w' ∈ ws, 0 < w' := fun w' hw' => hw w' (List.mem_cons_of_mem _ hw') + rw [budgetTuples_cons] + refine isChain_flatMap_range _ _ (fun b hb => ?_) (fun b _ => ?_) (fun b hb x hx y hy => ?_) + · have hb' := (lt_headCount_iff hw0).mp hb + rw [Ne, List.map_eq_nil_iff, ← List.head?_eq_none_iff, head?_budgetTuples hws (by omega)] + simp + · rw [List.isChain_map] + refine (ih hws (p - w * b)).imp fun x y hxy => ?_ + simp only [budgetNext, hxy] + · have hb1 := (lt_headCount_iff hw0).mp hb + rw [List.getLast?_map] at hx + obtain ⟨x', hx', rfl⟩ := Option.map_eq_some_iff.mp hx + rw [List.head?_map, head?_budgetTuples hws (by omega)] at hy + simp only [Option.map_some, Option.mem_def, Option.some.injEq] at hy + subst hy + simp only [budgetNext, budgetNext_getLast? hws x' hx', hb1, ↓reduceIte] + +/-! ### Tuples indexed by a finite type -/ + +section Indexed + +variable {M : Type*} [DecidableEq M] (ms : List M) + +/-- The tuple listed by `l` as a function of the coordinates listed by `ms`: coordinate `Z` reads +the entry of `l` at the position of `Z` in `ms`. -/ +@[expose] def ofList (l : List ℕ) (Z : M) : ℕ := l.getD (ms.idxOf Z) 0 + +omit [DecidableEq M] in +/-- The weight of the tuple of the values of `β` at the coordinates `ms`. -/ +private theorem weight_map (w β : M → ℕ) : + weight (ms.map w) (ms.map β) = (ms.map fun Z => w Z * β Z).sum := by + induction ms with + | nil => rfl + | cons Z ms ih => simp only [List.map_cons, weight_cons_cons, ih, List.sum_cons] + +variable {ms} + +/-- Reading back the values of a function at the coordinates `ms`. -/ +private theorem ofList_map (hcover : ∀ Z, Z ∈ ms) (β : M → ℕ) : + ofList ms (ms.map β) = β := by + funext Z + have hi : ms.idxOf Z < ms.length := List.idxOf_lt_length_iff.mpr (hcover Z) + rw [ofList, List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_map, + List.getElem_idxOf hi] + +/-- Listing the values of `ofList ms l` at the coordinates `ms` recovers `l`. -/ +private theorem map_ofList (hms : ms.Nodup) {l : List ℕ} (hl : l.length = ms.length) : + ms.map (ofList ms l) = l := by + apply List.ext_getElem (by simp [hl]) + intro i h₁ h₂ + simp only [List.getElem_map, ofList] + rw [List.Nodup.idxOf_getElem hms i (by simpa using h₁), List.getD_eq_getElem] + +/-- **The sum over the tuples of weight below `p`** is the sum along `budgetTuples`, for positive +weights and any duplicate-free list `ms` of all coordinates. The finite set is the mode budget +`Cslib.Circuits.Frontier.modeBudget w p` of the contraction recursion. -/ +theorem sum_filter_weight_lt_eq [Fintype M] (hms : ms.Nodup) (hcover : ∀ Z, Z ∈ ms) + {w : M → ℕ} (hw : ∀ Z, 0 < w Z) (p : ℕ) {S : Type*} [AddCommMonoid S] (f : (M → ℕ) → S) : + ∑ β ∈ ({β ∈ Fintype.piFinset fun _ => Finset.range p | ∑ Z, w Z * β Z < p} : + Finset (M → ℕ)), f β = + ((budgetTuples (ms.map w) p).map fun l => f (ofList ms l)).sum := by + have hws : ∀ x ∈ ms.map w, 0 < x := by + intro x hx + obtain ⟨Z, -, rfl⟩ := List.mem_map.mp hx + exact hw Z + have hsum (g : M → ℕ) : ∑ Z, g Z = (ms.map g).sum := by + rw [← List.sum_toFinset g hms] + congr 1 + ext Z + simp [hcover Z] + set L := budgetTuples (ms.map w) p + have hlen : ∀ l ∈ L, l.length = ms.length := fun l hl => by + simpa using ((mem_budgetTuples hws).mp hl).1 + have hnodup : (L.map (ofList ms)).Nodup := by + refine (nodup_budgetTuples _ _).map_on fun l hl l' hl' h => ?_ + rw [← map_ofList hms (hlen l hl), ← map_ofList hms (hlen l' hl'), h] + have hset : (L.map (ofList ms)).toFinset = + ({β ∈ Fintype.piFinset fun _ => Finset.range p | ∑ Z, w Z * β Z < p} : + Finset (M → ℕ)) := by + ext β + simp only [List.mem_toFinset, List.mem_map, Finset.mem_filter, Fintype.mem_piFinset, + Finset.mem_range] + constructor + · rintro ⟨l, hl, rfl⟩ + have hwt := ((mem_budgetTuples hws).mp hl).2 + rw [← map_ofList hms (hlen l hl), weight_map, ← hsum] at hwt + refine ⟨fun Z => ?_, hwt⟩ + calc ofList ms l Z ≤ w Z * ofList ms l Z := Nat.le_mul_of_pos_left _ (hw Z) + _ ≤ ∑ Z', w Z' * ofList ms l Z' := + Finset.single_le_sum (f := fun Z' => w Z' * ofList ms l Z') (fun _ _ => Nat.zero_le _) + (Finset.mem_univ Z) + _ < p := hwt + · rintro ⟨-, hβ⟩ + refine ⟨ms.map β, (mem_budgetTuples hws).mpr ⟨by simp, ?_⟩, ofList_map hcover β⟩ + rwa [weight_map, ← hsum] + rw [← hset, List.sum_toFinset _ hnodup, List.map_map] + rfl + +end Indexed + +end Cslib.BudgetTuples diff --git a/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean b/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean new file mode 100644 index 000000000..4754db4b5 --- /dev/null +++ b/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +module + +public import Complexity.Foundations.Combinatorics.BudgetTuples +import Mathlib.Data.Fin.VecNotation +import Mathlib.Data.List.FinRange + +public section + +open Cslib.BudgetTuples + +namespace Cslib.Tests.BudgetTuples + +/-! With weights `(1, 2)` and budget `4`, the tuples `(b₀, b₁)` with `b₀ + 2 b₁ < 4`, in +lexicographic order. -/ + +example : budgetTuples [1, 2] 4 = [[0, 0], [0, 1], [1, 0], [1, 1], [2, 0], [3, 0]] := by + decide +kernel + +/-- The successor walks the list from the zero tuple and stops after the last one. -/ +example : budgetNext [1, 2] 4 [0, 0] = some [0, 1] ∧ budgetNext [1, 2] 4 [0, 1] = some [1, 0] ∧ + budgetNext [1, 2] 4 [1, 1] = some [2, 0] ∧ budgetNext [1, 2] 4 [2, 0] = some [3, 0] ∧ + budgetNext [1, 2] 4 [3, 0] = none := by + decide +kernel + +/-- An empty budget has no tuples, and a positive one has the empty tuple for no coordinates. -/ +example : budgetTuples [3] 0 = [] ∧ budgetTuples [] 1 = [[]] := by decide +kernel + +/-- The six tuples of weight below `4` for the weights `![1, 2]` on `Fin 2`, counted along the +list. -/ +example : ∑ _β ∈ ({β ∈ Fintype.piFinset fun _ => Finset.range 4 | + ∑ Z, ![1, 2] Z * β Z < 4} : Finset (Fin 2 → ℕ)), 1 = 6 := by + rw [sum_filter_weight_lt_eq (List.nodup_finRange 2) (List.mem_finRange) (by decide) 4] + decide +kernel + +end Cslib.Tests.BudgetTuples From bd3e539aafd09e726ce1edcf6782a2fc986ae1d7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 00:59:54 -0400 Subject: [PATCH 2/6] feat(PolyTime): the successor of a tuple of bounded weight in polynomial time `budgetNextScan` computes `budgetNext` by one left scan over the coordinates (`budgetNextScan_eq`), and `computableInPolyTime_budgetNext` certifies it, so the enumeration of the mode exponents has polynomial delay. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Computability/PolyTime/BudgetTuples.lean | 200 ++++++++++++++++++ .../Combinatorics/BudgetTuples.lean | 57 ++++- .../Combinatorics/BudgetTuples.lean | 4 + 4 files changed, 260 insertions(+), 2 deletions(-) create mode 100644 Complexity/Computability/PolyTime/BudgetTuples.lean diff --git a/Complexity.lean b/Complexity.lean index e4ec57b7e..6f8dd26fc 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2009,6 +2009,7 @@ public import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidence public import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceSemantics public import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceStepCert public import Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter +public import Complexity.Computability.PolyTime.BudgetTuples public import Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter public import Complexity.Computability.PolyTime.CNF.GreedyParityContext public import Complexity.Computability.PolyTime.CNF.GreedyParitySearch diff --git a/Complexity/Computability/PolyTime/BudgetTuples.lean b/Complexity/Computability/PolyTime/BudgetTuples.lean new file mode 100644 index 000000000..312db6ff9 --- /dev/null +++ b/Complexity/Computability/PolyTime/BudgetTuples.lean @@ -0,0 +1,200 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +module +-- upstream: candidate + +public import Complexity.Foundations.Combinatorics.BudgetTuples +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops + +/-! +# The successor of a tuple of bounded weight in polynomial time + +`Cslib.BudgetTuples.budgetNext` walks the tuples of weight below a budget, the mode exponents of +the Boolean tensor contraction proof of [OpenAI2026ETH] (§D.4.5, p. 63). This file certifies that +one step is polynomial-time, with the weights, the budget and the tuple in binary +(`computableInPolyTime_budgetNext`), through its left scan `budgetNextScan`. So the enumeration +has polynomial delay. + +## Main definitions + +* `Cslib.BudgetTuples.encScanState`, `Cslib.BudgetTuples.encBudgetInput`: encodings of the scan + state and of the inputs. + +## Main results + +* `Cslib.BudgetTuples.computableInPolyTime_scanStep`: one step of the scan. +* `Cslib.BudgetTuples.computableInPolyTime_budgetNext`: the successor. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5, the enumeration + after (D.15), p. 63. +-/ + +public section + +namespace Cslib.BudgetTuples + +open Turing.MultiTapeTM + +/-- The state of the scan: the remaining budget in binary, the number of remaining weights in +unary, the coordinates read and the successor found so far in binary. -/ +abbrev ScanState : Type := ℕ × ℕ × List ℕ × Option (List ℕ) + +/-- The encoding of `ScanState`. -/ +@[expose] def encScanState : ScanState ↪ List Bool := + encPair encNat (encPair encUnary (encPair (encList encNat) (encOption (encList encNat)))) + +/-- The inputs `(ws, p, β)` of `budgetNext`, in binary. -/ +@[expose] def encBudgetInput : List ℕ × ℕ × List ℕ ↪ List Bool := + encPair (encList encNat) (encPair encNat (encList encNat)) + +/-- **One step of the scan is polynomial-time.** -/ +theorem computableInPolyTime_scanStep : + ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => scanStep q.1 q.2) + (encPair encScanState (encPair encNat encNat)) encScanState := by + let enc := encPair encScanState (encPair encNat encNat) + have hr : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.1.1) enc encNat := by + unfold enc encScanState; fun_prop + have hrest : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.1.2.1) enc encUnary := by + unfold enc encScanState; fun_prop + have hpre : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.1.2.2.1) enc + (encList encNat) := by + unfold enc encScanState; fun_prop + have hbest : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.1.2.2.2) enc + (encOption (encList encNat)) := by + unfold enc encScanState; fun_prop + have hw : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.2.1) enc encNat := by + unfold enc; fun_prop + have hb : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.2.2) enc encNat := by + unfold enc; fun_prop + have hb1 : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => q.2.2 + 1) enc encNat := + ComputableInPolyTime.binary_add.comp (hb.prod (.const 1)) + have hrest1 := ComputableInPolyTime.unary_sub' hrest (.const 1) + have hnew : ComputableInPolyTime (fun q : ScanState × (ℕ × ℕ) => + some (q.1.2.2.1 ++ (q.2.2 + 1) :: List.replicate (q.1.2.1 - 1) 0)) enc + (encOption (encList encNat)) := + (ComputableInPolyTime.optionSome (encList encNat)).comp (ComputableInPolyTime.listAppend' hpre + (ComputableInPolyTime.cons' hb1 (ComputableInPolyTime.replicate hrest1 (.const 0)))) + have hcond := ComputableInPolyTime.binary_lt' (ComputableInPolyTime.binary_mul' hw hb1) hr + have h := ((ComputableInPolyTime.binary_sub' hr (ComputableInPolyTime.binary_mul' hw hb)).prod + (hrest1.prod (((ComputableInPolyTime.snoc encNat).comp (hpre.prod hb)).prod + (hcond.ite' hnew hbest)))) + unfold encScanState + refine h.of_enc_eq fun q => ?_ + simp only [scanStep, decide_eq_true_eq, Function.comp_apply] + +/-- The coordinates of the zipped pairs form a prefix of the tuple. -/ +private theorem map_snd_zip_prefix (ws β : List ℕ) : (ws.zip β).map Prod.snd <+: β := by + induction ws generalizing β with + | nil => exact List.nil_prefix + | cons w ws ih => + cases β with + | nil => exact List.nil_prefix + | cons b β => simpa [List.prefix_cons_inj] using ih β + +/-- A prefix has a shorter encoding. -/ +private theorem length_encList_le_of_prefix {l₁ l₂ : List ℕ} (h : l₁ <+: l₂) : + (encList encNat l₁).length ≤ (encList encNat l₂).length := by + rw [length_encList, length_encList] + exact (h.sublist.map _).sum_le_sum fun _ _ => Nat.zero_le _ + +/-- A successor has at most one more bit. -/ +private theorem length_encNat_succ_le (b : ℕ) : + (encNat (b + 1)).length ≤ (encNat b).length + 1 := by + rw [length_encNat_eq_size, length_encNat_eq_size] + refine Nat.size_le.mpr ?_ + have := Nat.lt_size_self b + rw [pow_succ] + omega + +/-- **The successor is polynomial-time**, with the weights, the budget and the tuple in binary: +the enumeration of the tuples of bounded weight has polynomial delay. -/ +theorem computableInPolyTime_budgetNext : + ComputableInPolyTime (fun x : List ℕ × ℕ × List ℕ => budgetNext x.1 x.2.1 x.2.2) + encBudgetInput (encOption (encList encNat)) := by + have hws : ComputableInPolyTime (fun x : List ℕ × ℕ × List ℕ => x.1) encBudgetInput + (encList encNat) := by unfold encBudgetInput; fun_prop + have hp : ComputableInPolyTime (fun x : List ℕ × ℕ × List ℕ => x.2.1) encBudgetInput encNat := by + unfold encBudgetInput; fun_prop + have hβ : ComputableInPolyTime (fun x : List ℕ × ℕ × List ℕ => x.2.2) encBudgetInput + (encList encNat) := by unfold encBudgetInput; fun_prop + have hlist := (ComputableInPolyTime.zip encNat encNat).comp (hws.prod hβ) + have hinit : ComputableInPolyTime (fun x : List ℕ × ℕ × List ℕ => + ((x.2.1, x.1.length, [], none) : ScanState)) encBudgetInput encScanState := by + unfold encScanState + exact hp.prod (((ComputableInPolyTime.length_list _).comp hws).prod + ((ComputableInPolyTime.const (encOut := encList encNat) []).prod + (ComputableInPolyTime.const (encOut := encOption (encList encNat)) none))) + let size (x : List ℕ × ℕ × List ℕ) : ℕ := 4 * (encBudgetInput x).length + 8 + have hsize : PolyBounded (fun x => (encBudgetInput x).length) size := + ((PolyBounded.const 4).mul .self).add (.const 8) + have hproj : ComputableInPolyTime (fun s : ScanState => s.2.2.2) encScanState + (encOption (encList encNat)) := by unfold encScanState; fun_prop + refine (hproj.comp (ComputableInPolyTime.foldl_spec (step := scanStep) hlist hinit + computableInPolyTime_scanStep + (fun x consumed s => s.1 ≤ x.2.1 ∧ s.2.1 ≤ x.1.length ∧ s.2.2.1 = consumed.map Prod.snd ∧ + ∀ l, s.2.2.2 = some l → + (encList encNat l).length ≤ (encList encNat x.2.2).length + x.1.length + 2) + (fun x => ⟨le_rfl, le_rfl, rfl, fun _ h => by cases h⟩) ?_ hsize ?_).1).of_enc_eq + fun x => ?_ + · -- The invariant is preserved. + rintro ⟨ws, p, β⟩ consumed s ⟨w, b⟩ hpre ⟨hr, hrest, hcons, hbest⟩ + have hprefix : s.2.2.1 ++ [b] <+: β := by + have h1 : (consumed ++ [(w, b)]).map Prod.snd <+: (ws.zip β).map Prod.snd := + hpre.map _ + rw [List.map_append, ← hcons] at h1 + exact h1.trans (map_snd_zip_prefix ws β) + refine ⟨(Nat.sub_le _ _).trans hr, (Nat.sub_le _ _).trans hrest, by + simp [scanStep, hcons], fun l hl => ?_⟩ + simp only [scanStep] at hl + split_ifs at hl with hcond + · cases hl + have hle := length_encList_le_of_prefix hprefix + have hsucc := length_encNat_succ_le b + simp only [length_encList, List.map_append, List.sum_append, List.map_cons, List.sum_cons, + List.map_replicate, List.sum_replicate, List.map_nil, List.sum_nil, smul_eq_mul] at hle ⊢ + have h0 : (encNat 0).length = 0 := rfl + rw [h0] at ⊢ + have : s.2.1 - 1 ≤ ws.length := (Nat.sub_le _ _).trans hrest + omega + · exact hbest l hl + · -- The states are polynomially bounded. + rintro ⟨ws, p, β⟩ consumed s hpre ⟨hr, hrest, hcons, hbest⟩ + obtain ⟨r, rest, pre, best⟩ := s + simp only at hr hrest hcons hbest + have hpreβ : pre <+: β := hcons ▸ (hpre.map _).trans (map_snd_zip_prefix ws β) + have hpl := length_encList_le_of_prefix hpreβ + have hrl := length_encNat_mono hr + have hbl : (encOption (encList encNat) best).length ≤ + (encList encNat β).length + ws.length + 3 := by + cases best with + | none => simp [encOption_none] + | some l => simp only [encOption_some, List.length_cons]; have := hbest l rfl; omega + have hlen : ws.length ≤ (encList encNat ws).length := by + clear hpre hrest hbest hbl + rw [length_encList] + induction ws with + | nil => simp + | cons _ _ ih => simp only [List.length_cons, List.map_cons, List.sum_cons]; omega + simp only [encScanState, encBudgetInput, length_encPair, encUnary_apply, + List.length_replicate, size] + omega + · rw [← budgetNextScan_eq] + rfl + +end Cslib.BudgetTuples diff --git a/Complexity/Foundations/Combinatorics/BudgetTuples.lean b/Complexity/Foundations/Combinatorics/BudgetTuples.lean index d520039bd..ebc78e722 100644 --- a/Complexity/Foundations/Combinatorics/BudgetTuples.lean +++ b/Complexity/Foundations/Combinatorics/BudgetTuples.lean @@ -34,8 +34,13 @@ enumeration explicit: The list holds exactly the tuples of weight below `p` (`mem_budgetTuples`), each once (`nodup_budgetTuples`). It starts at the zero tuple (`head?_budgetTuples`), each entry is followed by its successor (`isChain_budgetTuples`), and the last one has none (`budgetNext_getLast?`). So -iterating `budgetNext` from zero visits every tuple once, with one successor computation, linear -in the number of coordinates, between consecutive tuples. +iterating `budgetNext` from zero visits every tuple once. The successor is also a left scan +(`budgetNextScan_eq`), one pass over the coordinates; its polynomial-time certificate is in +`Complexity/Computability/PolyTime/BudgetTuples.lean`. + +For tuples indexed by a finite type `M`, listed by a duplicate-free list of all coordinates, a sum +over the tuples of weight below `p`, the mode budget of the contraction recursion, is the sum +along `budgetTuples` (`sum_filter_weight_lt_eq`). ## Main definitions @@ -43,6 +48,8 @@ in the number of coordinates, between consecutive tuples. * `Cslib.BudgetTuples.headCount`: the number of feasible values of a coordinate. * `Cslib.BudgetTuples.budgetTuples`: the tuples of weight below a budget, in lexicographic order. * `Cslib.BudgetTuples.budgetNext`: the successor of a tuple. +* `Cslib.BudgetTuples.scanStep`, `Cslib.BudgetTuples.budgetNextScan`: the successor as a left scan. +* `Cslib.BudgetTuples.ofList`: a listed tuple as a function of its coordinates. ## Main results @@ -50,6 +57,8 @@ in the number of coordinates, between consecutive tuples. each tuple of weight below the budget once. * `Cslib.BudgetTuples.head?_budgetTuples`, `Cslib.BudgetTuples.isChain_budgetTuples`, `Cslib.BudgetTuples.budgetNext_getLast?`: the successor walks the list from the zero tuple. +* `Cslib.BudgetTuples.budgetNextScan_eq`: the scan computes the successor. +* `Cslib.BudgetTuples.sum_filter_weight_lt_eq`: a sum over the budget is a sum along the list. ## References @@ -317,4 +326,48 @@ theorem sum_filter_weight_lt_eq [Fintype M] (hms : ms.Nodup) (hcover : ∀ Z, Z end Indexed +/-! ### The successor as a left scan -/ + +/-- One step of the left scan behind `budgetNext`, reading a weight and a coordinate `(w, b)`. The +state holds the remaining budget, the number of remaining weights, the coordinates read so far, +and the successor obtained by incrementing the deepest position read so far that has room. -/ +@[expose] def scanStep (s : ℕ × ℕ × List ℕ × Option (List ℕ)) (q : ℕ × ℕ) : + ℕ × ℕ × List ℕ × Option (List ℕ) := + (s.1 - q.1 * q.2, s.2.1 - 1, s.2.2.1 ++ [q.2], + if q.1 * (q.2 + 1) < s.1 then some (s.2.2.1 ++ (q.2 + 1) :: List.replicate (s.2.1 - 1) 0) + else s.2.2.2) + +/-- **The successor by a left scan**: the deepest position with room is incremented and the +positions after it reset to zero. -/ +@[expose] def budgetNextScan (ws : List ℕ) (p : ℕ) (β : List ℕ) : Option (List ℕ) := + ((ws.zip β).foldl scanStep (p, ws.length, [], none)).2.2.2 + +private theorem foldl_scanStep (ws β : List ℕ) (r : ℕ) (pre : List ℕ) (best : Option (List ℕ)) : + ((ws.zip β).foldl scanStep (r, ws.length, pre, best)).2.2.2 = + match budgetNext ws r β with + | some t => some (pre ++ t) + | none => best := by + induction ws generalizing β r pre best with + | nil => rfl + | cons w ws ih => + rcases β with _ | ⟨b, β⟩ + · rfl + · rw [List.zip_cons_cons, List.foldl_cons] + have hstep : scanStep (r, (w :: ws).length, pre, best) (w, b) = + (r - w * b, ws.length, pre ++ [b], + if w * (b + 1) < r then some (pre ++ (b + 1) :: List.replicate ws.length 0) + else best) := by + simp [scanStep] + rw [hstep, ih] + simp only [budgetNext] + cases budgetNext ws (r - w * b) β with + | some t => simp + | none => split_ifs <;> rfl + +/-- The left scan computes the successor. -/ +theorem budgetNextScan_eq (ws : List ℕ) (p : ℕ) (β : List ℕ) : + budgetNextScan ws p β = budgetNext ws p β := by + rw [budgetNextScan, foldl_scanStep] + cases budgetNext ws p β <;> rfl + end Cslib.BudgetTuples diff --git a/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean b/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean index 4754db4b5..f14bcd5db 100644 --- a/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean +++ b/ComplexityTests/Foundations/Combinatorics/BudgetTuples.lean @@ -27,6 +27,10 @@ example : budgetNext [1, 2] 4 [0, 0] = some [0, 1] ∧ budgetNext [1, 2] 4 [0, 1 budgetNext [1, 2] 4 [3, 0] = none := by decide +kernel +/-- The left scan agrees. -/ +example : budgetNextScan [1, 2] 4 [1, 1] = some [2, 0] ∧ budgetNextScan [1, 2] 4 [3, 0] = none := by + decide +kernel + /-- An empty budget has no tuples, and a positive one has the empty tuple for no coordinates. -/ example : budgetTuples [3] 0 = [] ∧ budgetTuples [] 1 = [[]] := by decide +kernel From 4f2952814b6adc84a7f4719b968e5145537ebcb0 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:17:45 -0400 Subject: [PATCH 3/6] feat(circuit/frontier): the cursor over the children of an active call MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `cursorNext` walks the indices `(t, k, β, g)` of the children of an active call: the next group, else the next exponent tuple (`budgetNext`), else the next point, else the next node. `cursorList` lists them, and the walk from `cursorStart` follows it (`cursorList_walk`). One step is polynomial-time (`computableInPolyTime_cursorStep`), so the children have polynomial delay. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/ChildCursor.lean | 412 ++++++++++++++++++ .../Frontier/TensorNetworkChildCursor.lean | 46 ++ 3 files changed, 459 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean diff --git a/Complexity.lean b/Complexity.lean index 6f8dd26fc..1f7f03258 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -879,6 +879,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ActiveCall public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.CauchyModes +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildCursor public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildSize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean new file mode 100644 index 000000000..3a210ee81 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean @@ -0,0 +1,412 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +module +-- upstream: candidate + +public import Complexity.Foundations.Combinatorics.BudgetTuples +public import Complexity.Computability.PolyTime.BudgetTuples +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives + +/-! +# The cursor over the children of an active call + +An active call of the Boolean tensor contraction recursion of [OpenAI2026ETH] (§D.4.5–§D.4.7, +pp. 62–64) evaluates, for each node `t` of positive multiplicity, each interpolation point `k`, +each exponent tuple `β` of weight below the node's precision and each group `g < r`, one child +network. This file walks these indices with a cursor: the state is `(t, k, β, g)`, and +`cursorNext` advances the group, then the exponents (`Cslib.BudgetTuples.budgetNext`), then the +point, then the node, resetting the inner indices to their first values. The nodes are numbered +`0, …, T - 1`; node `t` has the weights `ws t` and the budget `ps t`. + +`cursorList` lists the indices in this order, nested from the node outwards. Under positive counts, +weights and budgets, the walk from `cursorStart` follows it: the list starts at `cursorStart` +(`head?_cursorList`), each entry is followed by its successor (`isChain_cursorList`) and the last +one has none (`cursorNext_getLast?`). `cursorList_walk` states this by index, in the form a loop +over counted children consumes. One step reads only the current node's weights and budget and the +next node's number of modes (`cursorNext_eq_cursorStep`), and it is polynomial-time +(`computableInPolyTime_cursorStep`), so the children are enumerated with polynomial delay. + +## Main definitions + +* `Cslib.Circuits.Frontier.ChildCursor.cursorList`: the indices `(t, k, β, g)` in order. +* `Cslib.Circuits.Frontier.ChildCursor.cursorStart`, + `Cslib.Circuits.Frontier.ChildCursor.cursorNext`: the cursor. +* `Cslib.Circuits.Frontier.ChildCursor.cursorStep`, + `Cslib.Circuits.Frontier.ChildCursor.encStepInput`: one step from the data of the nodes, and its + input encoding. + +## Main results + +* `Cslib.Circuits.Frontier.ChildCursor.head?_cursorList`, + `Cslib.Circuits.Frontier.ChildCursor.isChain_cursorList`, + `Cslib.Circuits.Frontier.ChildCursor.cursorNext_getLast?`, + `Cslib.Circuits.Frontier.ChildCursor.cursorList_walk`: the cursor walks the list. +* `Cslib.Circuits.Frontier.ChildCursor.isChain_flatMap`: a chain of nonempty chained blocks. +* `Cslib.Circuits.Frontier.ChildCursor.computableInPolyTime_cursorStep`: polynomial delay. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5–§D.4.7, pp. 62–64. +-/ + +public section + +namespace Cslib.Circuits.Frontier.ChildCursor + +open Cslib.BudgetTuples + +/-! ### Chains of blocks -/ + +/-- **A chain of nonempty blocks.** The concatenation of nonempty chains is a chain when the last +entry of each block is related to the first entry of the next. -/ +theorem isChain_flatMap {α β : Type*} {R : β → β → Prop} (f : α → List β) (l : List α) + (hne : ∀ a ∈ l, f a ≠ []) (hblock : ∀ a ∈ l, List.IsChain R (f a)) + (hjoin : List.IsChain (fun a a' => ∀ x ∈ (f a).getLast?, ∀ y ∈ (f a').head?, R x y) l) : + List.IsChain R (l.flatMap f) := by + induction l with + | nil => simp + | cons a l ih => + rw [List.flatMap_cons, List.isChain_append] + refine ⟨hblock a List.mem_cons_self, ih (fun b hb => hne b (List.mem_cons_of_mem _ hb)) + (fun b hb => hblock b (List.mem_cons_of_mem _ hb)) hjoin.tail, ?_⟩ + intro x hx y hy + rcases l with _ | ⟨b, l⟩ + · simp at hy + · rw [List.flatMap_cons, List.head?_append] at hy + obtain ⟨y', hy'⟩ := Option.ne_none_iff_exists'.mp + (fun h => hne b (List.mem_cons_of_mem _ List.mem_cons_self) (List.head?_eq_none_iff.mp h)) + rw [hy', Option.some_or] at hy + exact (List.isChain_cons_cons.mp hjoin).1 x hx y (hy' ▸ hy) + +/-- The last entry of a concatenation of blocks whose last block is nonempty. -/ +theorem getLast?_flatMap_concat {α β : Type*} (f : α → List β) (l : List α) (a : α) + (ha : f a ≠ []) : ((l ++ [a]).flatMap f).getLast? = (f a).getLast? := by + rw [List.flatMap_append, List.flatMap_singleton, List.getLast?_append] + cases h : (f a).getLast? with + | none => exact absurd (List.getLast?_eq_none_iff.mp h) ha + | some x => rfl + +private theorem isChain_range_of {R : ℕ → ℕ → Prop} {n : ℕ} (h : ∀ m, m + 1 < n → R m (m + 1)) : + List.IsChain R (List.range n) := by + rcases n with _ | n + · simp + · exact (List.isChain_range_succ R n).mpr fun m hm => h m (by omega) + +private theorem head?_flatMap_range {β : Type*} (f : ℕ → List β) {n : ℕ} (hn : 0 < n) {x : β} + (hx : (f 0).head? = some x) : ((List.range n).flatMap f).head? = some x := by + obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne' + rw [List.range_succ_eq_map, List.flatMap_cons, List.head?_append, hx, Option.some_or] + +private theorem getLast?_flatMap_range {β : Type*} (f : ℕ → List β) {n : ℕ} (hn : 0 < n) + (hne : f (n - 1) ≠ []) : ((List.range n).flatMap f).getLast? = (f (n - 1)).getLast? := by + obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne' + rw [List.range_succ, getLast?_flatMap_concat f _ _ (by simpa using hne)] + rfl + +/-! ### The cursor -/ + +/-- A state of the cursor: the node, the point, the exponents and the group. -/ +abbrev State : Type := ℕ × ℕ × List ℕ × ℕ + +variable (ws : ℕ → List ℕ) (ps : ℕ → ℕ) (T n r : ℕ) + +/-- The children of one exponent tuple: one per group. -/ +@[expose] def groupBlock (t k : ℕ) (β : List ℕ) : List State := + (List.range r).map fun g => (t, k, β, g) + +/-- The children of one point: the exponent tuples of weight below `ps t`, in lexicographic +order. -/ +@[expose] def pointBlock (t k : ℕ) : List State := + (budgetTuples (ws t) (ps t)).flatMap (groupBlock r t k) + +/-- The children of one node: its `n` points. -/ +@[expose] def nodeBlock (t : ℕ) : List State := + (List.range n).flatMap (pointBlock ws ps r t) + +/-- **The children of an active call**, as indices `(t, k, β, g)`: nested from the node outwards, +for the nodes `t < T`, the points `k < n`, the exponent tuples of weight below `ps t` and the +groups `g < r`. -/ +@[expose] def cursorList : List State := + (List.range T).flatMap (nodeBlock ws ps n r) + +/-- The first index. -/ +@[expose] def cursorStart : State := (0, 0, List.replicate (ws 0).length 0, 0) + +/-- **The successor of an index**: the next group, else the next exponent tuple, else the next +point, else the next node, with the inner indices reset to their first values. -/ +@[expose] def cursorNext (s : State) : Option State := + if s.2.2.2 + 1 < r then some (s.1, s.2.1, s.2.2.1, s.2.2.2 + 1) + else + match budgetNext (ws s.1) (ps s.1) s.2.2.1 with + | some β => some (s.1, s.2.1, β, 0) + | none => + if s.2.1 + 1 < n then some (s.1, s.2.1 + 1, List.replicate (ws s.1).length 0, 0) + else if s.1 + 1 < T then some (s.1 + 1, 0, List.replicate (ws (s.1 + 1)).length 0, 0) + else none + +variable {ws ps T n r} + +section Walk + +variable (hr : 0 < r) (hn : 0 < n) (hps : ∀ t, 0 < ps t) (hws : ∀ t, ∀ w ∈ ws t, 0 < w) +include hr + +theorem head?_groupBlock (t k : ℕ) (β : List ℕ) : + (groupBlock r t k β).head? = some (t, k, β, 0) := by + obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr.ne' + simp [groupBlock, List.range_succ_eq_map] + +theorem getLast?_groupBlock (t k : ℕ) (β : List ℕ) : + (groupBlock r t k β).getLast? = some (t, k, β, r - 1) := by + obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr.ne' + simp [groupBlock, List.range_succ, List.getLast?_map] + +theorem groupBlock_ne_nil (t k : ℕ) (β : List ℕ) : groupBlock r t k β ≠ [] := by + rw [Ne, ← List.head?_eq_none_iff, head?_groupBlock hr] + simp + +include hps hws + +theorem head?_pointBlock (t k : ℕ) : + (pointBlock ws ps r t k).head? = some (t, k, List.replicate (ws t).length 0, 0) := by + rw [pointBlock, List.head?_flatMap] + rw [show budgetTuples (ws t) (ps t) = + List.replicate (ws t).length 0 :: (budgetTuples (ws t) (ps t)).tail from + (List.eq_cons_of_mem_head? (head?_budgetTuples (hws t) (hps t))), List.findSome?_cons, + head?_groupBlock hr] + +theorem getLast?_pointBlock (t k : ℕ) : ∃ β, (pointBlock ws ps r t k).getLast? = + some (t, k, β, r - 1) ∧ budgetNext (ws t) (ps t) β = none := by + obtain ⟨β, hβ⟩ : ∃ β, (budgetTuples (ws t) (ps t)).getLast? = some β := by + refine Option.ne_none_iff_exists'.mp fun h => ?_ + have := head?_budgetTuples (hws t) (hps t) + rw [List.getLast?_eq_none_iff] at h + simp [h] at this + refine ⟨β, ?_, budgetNext_getLast? (hws t) β hβ⟩ + obtain ⟨ys, hys⟩ := List.getLast?_eq_some_iff.mp hβ + rw [pointBlock, hys, getLast?_flatMap_concat _ _ _ (groupBlock_ne_nil hr t k β), + getLast?_groupBlock hr] + +theorem pointBlock_ne_nil (t k : ℕ) : pointBlock ws ps r t k ≠ [] := by + rw [Ne, ← List.head?_eq_none_iff, head?_pointBlock hr hps hws] + simp + +omit hps in +/-- Within one point, the cursor walks the exponent tuples and the groups. -/ +theorem isChain_pointBlock (t k : ℕ) : + List.IsChain (fun x y => cursorNext ws ps T n r x = some y) (pointBlock ws ps r t k) := by + refine isChain_flatMap _ _ (fun β _ => groupBlock_ne_nil hr t k β) (fun β _ => ?_) ?_ + · rw [groupBlock, List.isChain_map] + refine isChain_range_of fun g hg => ?_ + simp [cursorNext, hg] + · refine (isChain_budgetTuples (hws t) (ps t)).imp fun β β' hββ' => ?_ + intro x hx y hy + rw [getLast?_groupBlock hr] at hx + rw [head?_groupBlock hr] at hy + simp only [Option.mem_def, Option.some.injEq] at hx hy + subst hx hy + have : ¬ r - 1 + 1 < r := by omega + simp [cursorNext, this, hββ'] + +include hn + +theorem head?_nodeBlock (t : ℕ) : + (nodeBlock ws ps n r t).head? = some (t, 0, List.replicate (ws t).length 0, 0) := + head?_flatMap_range _ hn (head?_pointBlock hr hps hws t 0) + +theorem nodeBlock_ne_nil (t : ℕ) : nodeBlock ws ps n r t ≠ [] := by + rw [Ne, ← List.head?_eq_none_iff, head?_nodeBlock hr hn hps hws] + simp + +theorem getLast?_nodeBlock (t : ℕ) : ∃ β, (nodeBlock ws ps n r t).getLast? = + some (t, n - 1, β, r - 1) ∧ budgetNext (ws t) (ps t) β = none := by + obtain ⟨β, hβ, hnone⟩ := getLast?_pointBlock hr hps hws t (n - 1) + exact ⟨β, by rw [nodeBlock, getLast?_flatMap_range _ hn (pointBlock_ne_nil hr hps hws t _), hβ], + hnone⟩ + +omit hn in +/-- Within one node, the cursor walks the points, the exponent tuples and the groups. -/ +theorem isChain_nodeBlock (t : ℕ) : + List.IsChain (fun x y => cursorNext ws ps T n r x = some y) (nodeBlock ws ps n r t) := by + refine isChain_flatMap _ _ (fun k _ => pointBlock_ne_nil hr hps hws t k) + (fun k _ => isChain_pointBlock hr hws t k) (isChain_range_of fun k hk => ?_) + intro x hx y hy + obtain ⟨β, hβ, hnone⟩ := getLast?_pointBlock hr hps hws t k + rw [hβ] at hx + rw [head?_pointBlock hr hps hws] at hy + simp only [Option.mem_def, Option.some.injEq] at hx hy + subst hx hy + have : ¬ r - 1 + 1 < r := by omega + simp [cursorNext, this, hnone, hk] + +/-- **The walk starts at `cursorStart`.** -/ +theorem head?_cursorList (hT : 0 < T) : (cursorList ws ps T n r).head? = some (cursorStart ws) := + head?_flatMap_range _ hT (head?_nodeBlock hr hn hps hws 0) + +/-- **Each index is followed by its successor.** -/ +theorem isChain_cursorList : + List.IsChain (fun x y => cursorNext ws ps T n r x = some y) (cursorList ws ps T n r) := by + refine isChain_flatMap _ _ (fun t _ => nodeBlock_ne_nil hr hn hps hws t) + (fun t _ => isChain_nodeBlock hr hps hws t) (isChain_range_of fun t ht => ?_) + intro x hx y hy + obtain ⟨β, hβ, hnone⟩ := getLast?_nodeBlock hr hn hps hws t + rw [hβ] at hx + rw [head?_nodeBlock hr hn hps hws] at hy + simp only [Option.mem_def, Option.some.injEq] at hx hy + subst hx hy + have h1 : ¬ r - 1 + 1 < r := by omega + have h2 : ¬ n - 1 + 1 < n := by omega + simp [cursorNext, h1, h2, hnone, ht] + +/-- **The last index has no successor.** -/ +theorem cursorNext_getLast? : + ∀ x ∈ (cursorList ws ps T n r).getLast?, cursorNext ws ps T n r x = none := by + intro x hx + rcases Nat.eq_zero_or_pos T with rfl | hT + · simp [cursorList] at hx + obtain ⟨β, hβ, hnone⟩ := getLast?_nodeBlock hr hn hps hws (T - 1) + rw [cursorList, getLast?_flatMap_range _ hT (nodeBlock_ne_nil hr hn hps hws _), hβ] at hx + simp only [Option.mem_def, Option.some.injEq] at hx + subst hx + have h1 : ¬ r - 1 + 1 < r := by omega + have h2 : ¬ n - 1 + 1 < n := by omega + have h3 : ¬ T - 1 + 1 < T := by omega + simp [cursorNext, h1, h2, h3, hnone] + +/-- **The indexed walk**, in the form a counted loop consumes: the first child is `cursorStart`, +child `c + 1` is the successor of child `c`, and the last child has no successor. -/ +theorem cursorList_walk (hT : 0 < T) : + ∃ h : 0 < (cursorList ws ps T n r).length, + (cursorList ws ps T n r)[0] = cursorStart ws ∧ + (∀ c (hc : c + 1 < (cursorList ws ps T n r).length), + cursorNext ws ps T n r (cursorList ws ps T n r)[c] = + some (cursorList ws ps T n r)[c + 1]) ∧ + cursorNext ws ps T n r ((cursorList ws ps T n r)[(cursorList ws ps T n r).length - 1]) = + none := by + have hhead := head?_cursorList hr hn hps hws (T := T) hT + have hpos : 0 < (cursorList ws ps T n r).length := by + rcases h : cursorList ws ps T n r with _ | ⟨x, l⟩ + · rw [h] at hhead; simp at hhead + · simp + refine ⟨hpos, ?_, fun c hc => (isChain_cursorList hr hn hps hws).getElem c hc, ?_⟩ + · rw [List.head?_eq_getElem?, List.getElem?_eq_getElem hpos] at hhead + exact Option.some.inj hhead + · refine cursorNext_getLast? hr hn hps hws _ ?_ + rw [List.getLast?_eq_getElem?, List.getElem?_eq_getElem (by omega)] + rfl + +end Walk + +/-! ### Polynomial time -/ + +/-- One step of the cursor, from the counts `(T, n, r)`, the current node's weights and budget, and +the next node's number of modes: `cursorNext` with the data of the nodes read off. -/ +@[expose] def cursorStep (T n r : ℕ) (wt : List ℕ) (pt nextLen : ℕ) (s : State) : Option State := + if s.2.2.2 + 1 < r then some (s.1, s.2.1, s.2.2.1, s.2.2.2 + 1) + else + (budgetNext wt pt s.2.2.1).elim + (if s.2.1 + 1 < n then some (s.1, s.2.1 + 1, List.replicate wt.length 0, 0) + else if s.1 + 1 < T then some (s.1 + 1, 0, List.replicate nextLen 0, 0) else none) + fun β => some (s.1, s.2.1, β, 0) + +/-- The cursor is its step at the current node. -/ +theorem cursorNext_eq_cursorStep (ws : ℕ → List ℕ) (ps : ℕ → ℕ) (T n r : ℕ) (s : State) : + cursorNext ws ps T n r s = cursorStep T n r (ws s.1) (ps s.1) (ws (s.1 + 1)).length s := by + unfold cursorNext cursorStep + split_ifs <;> cases budgetNext (ws s.1) (ps s.1) s.2.2.1 <;> rfl + +open Turing.MultiTapeTM + +/-- The inputs of `cursorStep`: the counts in unary, the weights and the budget in binary, the next +number of modes in unary, and the state with its exponents in binary. -/ +abbrev StepInput : Type := ((ℕ × ℕ × ℕ) × (List ℕ × ℕ × ℕ)) × State + +/-- The encoding of a state. -/ +@[expose] def encState : State ↪ List Bool := + encPair encUnary (encPair encUnary (encPair (encList encNat) encUnary)) + +/-- The encoding of `StepInput`. -/ +@[expose] def encStepInput : StepInput ↪ List Bool := + encPair (encPair (encPair encUnary (encPair encUnary encUnary)) + (encPair (encList encNat) (encPair encNat encUnary))) encState + +/-- **The cursor step is polynomial-time**: the children are enumerated with polynomial delay. -/ +theorem computableInPolyTime_cursorStep : + ComputableInPolyTime (fun x : StepInput => + cursorStep x.1.1.1 x.1.1.2.1 x.1.1.2.2 x.1.2.1 x.1.2.2.1 x.1.2.2.2 x.2) encStepInput + (encOption encState) := by + let e := encStepInput + have hT : ComputableInPolyTime (fun x : StepInput => x.1.1.1) e encUnary := by + unfold e encStepInput; fun_prop + have hn : ComputableInPolyTime (fun x : StepInput => x.1.1.2.1) e encUnary := by + unfold e encStepInput; fun_prop + have hr : ComputableInPolyTime (fun x : StepInput => x.1.1.2.2) e encUnary := by + unfold e encStepInput; fun_prop + have hwt : ComputableInPolyTime (fun x : StepInput => x.1.2.1) e (encList encNat) := by + unfold e encStepInput; fun_prop + have hpt : ComputableInPolyTime (fun x : StepInput => x.1.2.2.1) e encNat := by + unfold e encStepInput; fun_prop + have hnext : ComputableInPolyTime (fun x : StepInput => x.1.2.2.2) e encUnary := by + unfold e encStepInput; fun_prop + have ht : ComputableInPolyTime (fun x : StepInput => x.2.1) e encUnary := by + unfold e encStepInput encState; fun_prop + have hk : ComputableInPolyTime (fun x : StepInput => x.2.2.1) e encUnary := by + unfold e encStepInput encState; fun_prop + have hβ : ComputableInPolyTime (fun x : StepInput => x.2.2.2.1) e (encList encNat) := by + unfold e encStepInput encState; fun_prop + have hg : ComputableInPolyTime (fun x : StepInput => x.2.2.2.2) e encUnary := by + unfold e encStepInput encState; fun_prop + have hsome {f : StepInput → State} (hf : ComputableInPolyTime f e encState) : + ComputableInPolyTime (fun x => some (f x)) e (encOption encState) := + (ComputableInPolyTime.optionSome encState).comp hf + have hmk {t k g : StepInput → ℕ} {β : StepInput → List ℕ} + (h1 : ComputableInPolyTime t e encUnary) (h2 : ComputableInPolyTime k e encUnary) + (h3 : ComputableInPolyTime β e (encList encNat)) (h4 : ComputableInPolyTime g e encUnary) : + ComputableInPolyTime (fun x => ((t x, k x, β x, g x) : State)) e encState := by + unfold encState; exact h1.prod (h2.prod (h3.prod h4)) + have hsucc {f : StepInput → ℕ} (hf : ComputableInPolyTime f e encUnary) : + ComputableInPolyTime (fun x => f x + 1) e encUnary := + ComputableInPolyTime.unary_add' hf (.const 1) + have hbudget := computableInPolyTime_budgetNext.comp + (show ComputableInPolyTime (fun x : StepInput => (x.1.2.1, x.1.2.2.1, x.2.2.2.1)) e + encBudgetInput by unfold encBudgetInput; exact hwt.prod (hpt.prod hβ)) + have hzeros {f : StepInput → ℕ} (hf : ComputableInPolyTime f e encUnary) : + ComputableInPolyTime (fun x => List.replicate (f x) 0) e (encList encNat) := + ComputableInPolyTime.replicate hf (.const 0) + have hfallback : ComputableInPolyTime (fun x : StepInput => + if x.2.2.1 + 1 < x.1.1.2.1 then + some ((x.2.1, x.2.2.1 + 1, List.replicate x.1.2.1.length 0, 0) : State) + else if x.2.1 + 1 < x.1.1.1 then + some ((x.2.1 + 1, 0, List.replicate x.1.2.2.2 0, 0) : State) + else none) e (encOption encState) := by + refine (ComputableInPolyTime.ite' (ComputableInPolyTime.unary_lt' (hsucc hk) hn) + (hsome (hmk ht (hsucc hk) (hzeros ((ComputableInPolyTime.length_list _).comp hwt)) + (.const 0))) + (ComputableInPolyTime.ite' (ComputableInPolyTime.unary_lt' (hsucc ht) hT) + (hsome (hmk (hsucc ht) (.const 0) (hzeros hnext) (.const 0))) (.const none))).of_enc_eq + fun x => ?_ + simp only [decide_eq_true_eq, Function.comp_apply] + have hbody : ComputableInPolyTime (fun p : StepInput × List ℕ => + some ((p.1.2.1, p.1.2.2.1, p.2, 0) : State)) (encPair e (encList encNat)) + (encOption encState) := by + refine (ComputableInPolyTime.optionSome encState).comp ?_ + unfold encState + exact (ht.comp (ComputableInPolyTime.fst _ _)).prod + ((hk.comp (ComputableInPolyTime.fst _ _)).prod ((ComputableInPolyTime.snd _ _).prod + (.const 0))) + have helim := ComputableInPolyTime.optionElimWithInput + (body := fun x β => some ((x.2.1, x.2.2.1, β, 0) : State)) hbudget hfallback hbody + have h := ComputableInPolyTime.ite' (ComputableInPolyTime.unary_lt' (hsucc hg) hr) + (hsome (hmk ht hk hβ (hsucc hg))) helim + refine h.of_enc_eq fun x => ?_ + simp only [cursorStep, decide_eq_true_eq, Function.comp_apply] + +end Cslib.Circuits.Frontier.ChildCursor diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean new file mode 100644 index 000000000..e226003f5 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildCursor + +public section + +open Cslib.Circuits.Frontier.ChildCursor + +namespace Cslib.Tests.TensorNetworkChildCursor + +/-! Two nodes: node `0` has one mode of weight `1` and budget `2`, so the exponents `0, 1`; node +`1` has two modes of weights `1, 2` and budget `2`, so the exponents `00, 10`. With one point and +two groups the cursor visits eight children. -/ + +def ws (t : ℕ) : List ℕ := if t = 0 then [1] else [1, 2] +def ps (_ : ℕ) : ℕ := 2 + +example : cursorList ws ps 2 1 2 = + [(0, 0, [0], 0), (0, 0, [0], 1), (0, 0, [1], 0), (0, 0, [1], 1), + (1, 0, [0, 0], 0), (1, 0, [0, 0], 1), (1, 0, [1, 0], 0), (1, 0, [1, 0], 1)] := by + decide +kernel + +/-- The cursor walks the list and stops after the last child. -/ +example : cursorStart ws = (0, 0, [0], 0) ∧ + cursorNext ws ps 2 1 2 (0, 0, [0], 1) = some (0, 0, [1], 0) ∧ + cursorNext ws ps 2 1 2 (0, 0, [1], 1) = some (1, 0, [0, 0], 0) ∧ + cursorNext ws ps 2 1 2 (1, 0, [1, 0], 1) = none := by + decide +kernel + +/-- The walk, by index, from the general theorem. -/ +example : ∃ h : 0 < (cursorList ws ps 2 1 2).length, + (cursorList ws ps 2 1 2)[0] = cursorStart ws ∧ + (∀ c (hc : c + 1 < (cursorList ws ps 2 1 2).length), + cursorNext ws ps 2 1 2 (cursorList ws ps 2 1 2)[c] = some (cursorList ws ps 2 1 2)[c + 1]) ∧ + cursorNext ws ps 2 1 2 ((cursorList ws ps 2 1 2)[(cursorList ws ps 2 1 2).length - 1]) = + none := + cursorList_walk (by norm_num) (by norm_num) (fun _ => by simp [ps]) + (fun t w hw => by unfold ws at hw; split_ifs at hw <;> simp at hw <;> omega) (by norm_num) + +end Cslib.Tests.TensorNetworkChildCursor From af142d19bc9e0d360af8b5f53b34218742134ec1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:20:03 -0400 Subject: [PATCH 4/6] refactor(combinatorics): count the feasible coordinate values with Mathlib's ceiling division MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review of #1942: replace the parallel `headCount` with `p ⌈/⌉ w`, which is definitionally `(p + w - 1) / w`; `lt_ceilDiv_iff` now follows from `ceilDiv_le_iff_le_mul`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Combinatorics/BudgetTuples.lean | 39 ++++++++----------- 1 file changed, 17 insertions(+), 22 deletions(-) diff --git a/Complexity/Foundations/Combinatorics/BudgetTuples.lean b/Complexity/Foundations/Combinatorics/BudgetTuples.lean index ebc78e722..3ed809c73 100644 --- a/Complexity/Foundations/Combinatorics/BudgetTuples.lean +++ b/Complexity/Foundations/Combinatorics/BudgetTuples.lean @@ -8,6 +8,7 @@ module public import Complexity.Init public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.Order.Floor.Div public import Mathlib.Data.Fintype.Pi public import Mathlib.Data.List.Chain import Mathlib.Algebra.BigOperators.Group.List.Basic @@ -45,7 +46,6 @@ along `budgetTuples` (`sum_filter_weight_lt_eq`). ## Main definitions * `Cslib.BudgetTuples.weight`: the weight of a tuple. -* `Cslib.BudgetTuples.headCount`: the number of feasible values of a coordinate. * `Cslib.BudgetTuples.budgetTuples`: the tuples of weight below a budget, in lexicographic order. * `Cslib.BudgetTuples.budgetNext`: the successor of a tuple. * `Cslib.BudgetTuples.scanStep`, `Cslib.BudgetTuples.budgetNextScan`: the successor as a left scan. @@ -75,22 +75,17 @@ namespace Cslib.BudgetTuples | w :: ws, b :: β => w * b + weight ws β | _, _ => 0 -/-- The number of values `b` of a coordinate of weight `w` with `w * b < p`, that is -`⌈p / w⌉` for `w > 0`. -/ -@[expose] def headCount (w p : ℕ) : ℕ := (p + w - 1) / w - -/-- A value fits the budget exactly when it is below `headCount`. -/ -theorem lt_headCount_iff {w p b : ℕ} (hw : 0 < w) : b < headCount w p ↔ w * b < p := by - rw [headCount, Nat.lt_iff_add_one_le, Nat.le_div_iff_mul_le hw, Nat.add_mul, Nat.one_mul, - Nat.mul_comm b w] - omega +/-- A value of a coordinate of weight `w` fits the budget `p` exactly when it is below the ceiling +division `p ⌈/⌉ w`. -/ +theorem lt_ceilDiv_iff {w p b : ℕ} (hw : 0 < w) : b < p ⌈/⌉ w ↔ w * b < p := by + rw [← not_le, ceilDiv_le_iff_le_mul hw, not_le] /-- **The tuples of weight below `p`**, in lexicographic order: the first coordinate takes each -value `b` with `w * b < p` in increasing order, and the rest is a tuple of weight below -`p - w * b`. -/ +value `b` with `w * b < p` (`lt_ceilDiv_iff`) in increasing order, and the rest is a tuple of +weight below `p - w * b`. -/ @[expose] def budgetTuples : List ℕ → ℕ → List (List ℕ) | [], p => if 0 < p then [[]] else [] - | w :: ws, p => (List.range (headCount w p)).flatMap fun b => + | w :: ws, p => (List.range (p ⌈/⌉ w)).flatMap fun b => (budgetTuples ws (p - w * b)).map (b :: ·) /-- **The successor of a tuple**: advance the tail within its remaining budget if possible, and @@ -107,7 +102,7 @@ otherwise increment the first coordinate and reset the tail to zero. -/ @[simp] theorem budgetTuples_nil (p : ℕ) : budgetTuples [] p = if 0 < p then [[]] else [] := rfl theorem budgetTuples_cons (w : ℕ) (ws : List ℕ) (p : ℕ) : - budgetTuples (w :: ws) p = (List.range (headCount w p)).flatMap fun b => + budgetTuples (w :: ws) p = (List.range (p ⌈/⌉ w)).flatMap fun b => (budgetTuples ws (p - w * b)).map (b :: ·) := rfl @[simp] theorem weight_nil (β : List ℕ) : weight [] β = 0 := rfl @@ -126,7 +121,7 @@ theorem mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} { have hw0 : 0 < w := hw w List.mem_cons_self have ih' := @ih (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) rw [budgetTuples_cons] - simp only [List.mem_flatMap, List.mem_range, lt_headCount_iff hw0, List.mem_map] + simp only [List.mem_flatMap, List.mem_range, lt_ceilDiv_iff hw0, List.mem_map] constructor · rintro ⟨b, hb, γ, hγ, rfl⟩ rw [ih'] at hγ @@ -187,8 +182,8 @@ theorem head?_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} | cons w ws ih => have hw0 : 0 < w := hw w List.mem_cons_self have ih' := @ih (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) - obtain ⟨k, hk⟩ : ∃ k, headCount w p = k + 1 := - Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp ((lt_headCount_iff hw0).mpr + obtain ⟨k, hk⟩ : ∃ k, p ⌈/⌉ w = k + 1 := + Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp ((lt_ceilDiv_iff hw0).mpr (by simpa using hp))) rw [budgetTuples_cons, hk, List.range_succ_eq_map, List.flatMap_cons, List.head?_append, List.head?_map, Nat.mul_zero, Nat.sub_zero, ih' hp] @@ -204,9 +199,9 @@ theorem budgetNext_getLast? {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} have ih' := @ih (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) intro x hx rw [budgetTuples_cons] at hx - rcases hn : headCount w p with _ | k + rcases hn : p ⌈/⌉ w with _ | k · rw [hn] at hx; simp at hx - · have hk : w * k < p := (lt_headCount_iff hw0).mp (by omega) + · have hk : w * k < p := (lt_ceilDiv_iff hw0).mp (by omega) have hne : (budgetTuples ws (p - w * k)).map (k :: ·) ≠ [] := by rw [Ne, List.map_eq_nil_iff, ← List.head?_eq_none_iff, head?_budgetTuples (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) (by omega)] @@ -214,7 +209,7 @@ theorem budgetNext_getLast? {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} rw [hn, getLast?_flatMap_range_succ _ k hne, List.getLast?_map] at hx obtain ⟨x', hx', rfl⟩ := Option.map_eq_some_iff.mp hx have hnot : ¬ w * (k + 1) < p := fun h => by - have := (lt_headCount_iff hw0).mpr h; omega + have := (lt_ceilDiv_iff hw0).mpr h; omega simp only [budgetNext, ih' x' hx', hnot, ↓reduceIte] /-- **Each tuple is followed by its successor.** -/ @@ -229,13 +224,13 @@ theorem isChain_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) (p : ℕ have hws : ∀ w' ∈ ws, 0 < w' := fun w' hw' => hw w' (List.mem_cons_of_mem _ hw') rw [budgetTuples_cons] refine isChain_flatMap_range _ _ (fun b hb => ?_) (fun b _ => ?_) (fun b hb x hx y hy => ?_) - · have hb' := (lt_headCount_iff hw0).mp hb + · have hb' := (lt_ceilDiv_iff hw0).mp hb rw [Ne, List.map_eq_nil_iff, ← List.head?_eq_none_iff, head?_budgetTuples hws (by omega)] simp · rw [List.isChain_map] refine (ih hws (p - w * b)).imp fun x y hxy => ?_ simp only [budgetNext, hxy] - · have hb1 := (lt_headCount_iff hw0).mp hb + · have hb1 := (lt_ceilDiv_iff hw0).mp hb rw [List.getLast?_map] at hx obtain ⟨x', hx', rfl⟩ := Option.map_eq_some_iff.mp hx rw [List.head?_map, head?_budgetTuples hws (by omega)] at hy From 8daeef7a000815f86545a8b1e38f8846d251daf3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:23:56 -0400 Subject: [PATCH 5/6] feat(circuit/frontier): the values a call stores along the cursor `absorbAt` multiplies a child's value into the product over the groups, adds the product to the sum over the exponent tuples after the last group, and stores the sum after the last tuple. `runAcc_cursorList`: along `cursorList` it stores, for each node and point, the sum over the tuples of the products over the groups, seen through any map respecting the operations. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/ChildCursor.lean | 181 ++++++++++++++++++ 1 file changed, 181 insertions(+) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean index 3a210ee81..60e643d90 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean @@ -409,4 +409,185 @@ theorem computableInPolyTime_cursorStep : refine h.of_enc_eq fun x => ?_ simp only [cursorStep, decide_eq_true_eq, Function.comp_apply] +/-! ### Accumulating the values of the children -/ + +section Accumulate + +variable (ws ps r) +variable {S R : Type*} [CommSemiring R] (mul add : S → S → S) (one zero : S) (φ : S → R) + (hmul : ∀ x y, φ (mul x y) = φ x * φ y) (hadd : ∀ x y, φ (add x y) = φ x + φ y) + (hone : φ one = 1) + +/-- The accumulator of a call: the product over the groups so far, the sum over the exponent tuples +so far, and the stored values, one per node and point. -/ +abbrev Acc (S : Type*) : Type _ := S × S × List S + +/-- **Absorb the value `y` of the child at `s`**: multiply it into the product over the groups; +after the last group, add the product to the sum over the exponent tuples; after the last tuple, +store the sum. -/ +@[expose] def absorbAt (s : State) (acc : Acc S) (y : S) : Acc S := + if s.2.2.2 + 1 < r then (mul acc.1 y, acc.2.1, acc.2.2) + else if (budgetNext (ws s.1) (ps s.1) s.2.2.1).isNone then + (one, zero, acc.2.2 ++ [add acc.2.1 (mul acc.1 y)]) + else (one, add acc.2.1 (mul acc.1 y), acc.2.2) + +/-- The accumulator after the children `l` with the values `val`. -/ +@[expose] def runAcc (val : State → S) (l : List State) (acc : Acc S) : Acc S := + l.foldl (fun acc s => absorbAt ws ps r mul add one zero s acc (val s)) acc + +omit [CommSemiring R] in +/-- Absorbing two lists of children absorbs one, then the other. -/ +theorem runAcc_append (val : State → S) (l₁ l₂ : List State) (acc : Acc S) : + runAcc ws ps r mul add one zero val (l₁ ++ l₂) acc = + runAcc ws ps r mul add one zero val l₂ (runAcc ws ps r mul add one zero val l₁ acc) := by + simp only [runAcc, List.foldl_append] + +include hmul in +/-- Before the last group, the product over the groups accumulates. -/ +private theorem runAcc_groups (val : State → S) (t k : ℕ) (β : List ℕ) (j : ℕ) (hj : j + 1 ≤ r) + (acc : Acc S) : + (runAcc ws ps r mul add one zero val ((List.range j).map fun g => (t, k, β, g)) acc).2 = + acc.2 ∧ + φ (runAcc ws ps r mul add one zero val ((List.range j).map fun g => (t, k, β, g)) acc).1 = + φ acc.1 * ((List.range j).map fun g => φ (val (t, k, β, g))).prod := by + induction j with + | zero => simp [runAcc] + | succ j ih => + obtain ⟨h1, h2⟩ := ih (by omega) + have hsplit : runAcc ws ps r mul add one zero val + ((List.range (j + 1)).map fun g => (t, k, β, g)) acc = + absorbAt ws ps r mul add one zero (t, k, β, j) (runAcc ws ps r mul add one zero val + ((List.range j).map fun g => (t, k, β, g)) acc) (val (t, k, β, j)) := by + simp only [runAcc, List.range_succ, List.map_append, List.map_singleton, List.foldl_append, + List.foldl_cons, List.foldl_nil] + rw [hsplit] + simp only [absorbAt, show j + 1 < r by omega, ↓reduceIte] + refine ⟨h1, ?_⟩ + rw [hmul, h2, List.range_succ, List.map_append, List.prod_append, List.map_singleton, + List.prod_singleton, mul_assoc] + +include hmul hadd in +/-- After the last group of a tuple, the product joins the sum, and after the last tuple the sum is +stored. -/ +private theorem runAcc_groupBlock (hr : 0 < r) (val : State → S) (t k : ℕ) (β : List ℕ) + (acc : Acc S) : + ∃ q, φ q = φ acc.2.1 + φ acc.1 * ((List.range r).map fun g => φ (val (t, k, β, g))).prod ∧ + runAcc ws ps r mul add one zero val (groupBlock r t k β) acc = + if (budgetNext (ws t) (ps t) β).isNone then (one, zero, acc.2.2 ++ [q]) + else (one, q, acc.2.2) := by + obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr.ne' + obtain ⟨h1, h2⟩ := runAcc_groups ws ps (r + 1) mul add one zero φ hmul val t k β r le_rfl acc + set mid := runAcc ws ps (r + 1) mul add one zero val + ((List.range r).map fun g => (t, k, β, g)) acc + refine ⟨add acc.2.1 (mul mid.1 (val (t, k, β, r))), ?_, ?_⟩ + · rw [hadd, hmul, h2, List.range_succ, List.map_append, List.prod_append, List.map_singleton, + List.prod_singleton, mul_assoc] + · have hsplit : runAcc ws ps (r + 1) mul add one zero val (groupBlock (r + 1) t k β) acc = + absorbAt ws ps (r + 1) mul add one zero (t, k, β, r) mid (val (t, k, β, r)) := by + simp only [groupBlock, runAcc, mid, List.range_succ, List.map_append, List.map_singleton, + List.foldl_append, List.foldl_cons, List.foldl_nil] + rw [hsplit] + simp only [absorbAt, lt_irrefl, ↓reduceIte, h1] + +include hmul hadd hone in +/-- Over a list of tuples whose last one alone has no successor, the sum over the tuples is +stored. -/ +private theorem runAcc_tuples (hr : 0 < r) (val : State → S) (t k : ℕ) (B : List (List ℕ)) + (hB : B ≠ []) (hsome : ∀ β ∈ B.dropLast, (budgetNext (ws t) (ps t) β).isSome) + (hlast : (budgetNext (ws t) (ps t) (B.getLast hB)).isNone) (sm : S) (V : List S) : + ∃ q, φ q = φ sm + (B.map fun β => ((List.range r).map fun g => φ (val (t, k, β, g))).prod).sum ∧ + runAcc ws ps r mul add one zero val (B.flatMap (groupBlock r t k)) (one, sm, V) = + (one, zero, V ++ [q]) := by + induction B generalizing sm with + | nil => exact absurd rfl hB + | cons β B ih => + obtain ⟨q₁, hq₁, hrun₁⟩ := runAcc_groupBlock ws ps r mul add one zero φ hmul hadd hr val t k β + (one, sm, V) + rcases B with _ | ⟨β', B⟩ + · simp only [List.getLast_singleton] at hlast + refine ⟨q₁, ?_, ?_⟩ + · simpa [hone] using hq₁ + · simpa [runAcc, hlast] using hrun₁ + · have hβ : (budgetNext (ws t) (ps t) β).isSome := hsome β (by simp) + have hnone : (budgetNext (ws t) (ps t) β).isNone = false := by + simpa [Option.isNone_iff_eq_none, Option.isSome_iff_ne_none] using hβ + obtain ⟨q, hq, hrun⟩ := ih (List.cons_ne_nil _ _) + (fun γ hγ => hsome γ (by + simp only [List.dropLast_cons_cons]; exact List.mem_cons_of_mem _ hγ)) + (by simpa using hlast) q₁ + refine ⟨q, ?_, ?_⟩ + · simp only [hq, hq₁, hone, one_mul, List.map_cons, List.sum_cons, add_assoc] + · rw [List.flatMap_cons, runAcc_append, hrun₁, hnone] + simpa using hrun + +/-- The values stored for a node and point: the sum over the exponent tuples of the products over +the groups. -/ +@[expose] def sumAt (val : State → S) (t k : ℕ) : R := + ((budgetTuples (ws t) (ps t)).map fun β => + ((List.range r).map fun g => φ (val (t, k, β, g))).prod).sum + +include hmul hadd hone + +/-- Over the points of a node, one sum is stored per point. -/ +private theorem runAcc_points (hzero : φ zero = 0) (hr : 0 < r) (hps : ∀ t, 0 < ps t) + (hws : ∀ t, ∀ w ∈ ws t, 0 < w) (val : State → S) (t j : ℕ) (V : List S) : + ∃ qs : List S, qs.map φ = (List.range j).map (sumAt ws ps r φ val t) ∧ + runAcc ws ps r mul add one zero val ((List.range j).flatMap (pointBlock ws ps r t)) + (one, zero, V) = (one, zero, V ++ qs) := by + induction j generalizing V with + | zero => exact ⟨[], rfl, by simp [runAcc]⟩ + | succ j ih => + obtain ⟨qs, hqs, hrun⟩ := ih V + set B := budgetTuples (ws t) (ps t) + have hB : B ≠ [] := by + rw [Ne, ← List.head?_eq_none_iff, head?_budgetTuples (hws t) (hps t)] + simp + have hsome : ∀ β ∈ B.dropLast, (budgetNext (ws t) (ps t) β).isSome := by + intro β hβ + obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hβ + rw [List.length_dropLast] at hi + have hlen : B.length = (budgetTuples (ws t) (ps t)).length := rfl + rw [List.getElem_dropLast, (isChain_budgetTuples (hws t) (ps t)).getElem i (by omega)] + rfl + have hlast : (budgetNext (ws t) (ps t) (B.getLast hB)).isNone := by + rw [budgetNext_getLast? (hws t) _ (List.getLast?_eq_some_getLast hB ▸ rfl)] + rfl + obtain ⟨q, hq, hrunq⟩ := runAcc_tuples ws ps r mul add one zero φ hmul hadd hone hr val t j B + hB hsome hlast zero (V ++ qs) + refine ⟨qs ++ [q], ?_, ?_⟩ + · rw [List.map_append, hqs, List.range_succ, List.map_append, List.map_singleton, + List.map_singleton, hq, hzero, zero_add] + rfl + · rw [List.range_succ, List.flatMap_append, runAcc_append, hrun, List.flatMap_singleton, + pointBlock, hrunq, List.append_assoc] + +/-- **The values stored by a call**: absorbing the values of the children along `cursorList` +stores, for each node and point in order, the sum over the exponent tuples of the products over +the groups (`sumAt`), as seen through `φ`. -/ +theorem runAcc_cursorList (hzero : φ zero = 0) (hr : 0 < r) (hps : ∀ t, 0 < ps t) + (hws : ∀ t, ∀ w ∈ ws t, 0 < w) (val : State → S) : + ∃ qs : List S, qs.map φ = + (List.range T).flatMap (fun t => (List.range n).map (sumAt ws ps r φ val t)) ∧ + runAcc ws ps r mul add one zero val (cursorList ws ps T n r) (one, zero, []) = + (one, zero, qs) := by + have key : ∀ j, ∃ qs : List S, qs.map φ = + (List.range j).flatMap (fun t => (List.range n).map (sumAt ws ps r φ val t)) ∧ + runAcc ws ps r mul add one zero val ((List.range j).flatMap (nodeBlock ws ps n r)) + (one, zero, []) = (one, zero, qs) := by + intro j + induction j with + | zero => exact ⟨[], rfl, by simp [runAcc]⟩ + | succ j ih => + obtain ⟨qs, hqs, hrun⟩ := ih + obtain ⟨qs', hqs', hrun'⟩ := runAcc_points ws ps r mul add one zero φ hmul hadd hone hzero hr + hps hws val j n qs + refine ⟨qs ++ qs', ?_, ?_⟩ + · rw [List.map_append, hqs, hqs', List.range_succ, List.flatMap_append, + List.flatMap_singleton] + · rw [List.range_succ, List.flatMap_append, runAcc_append, hrun, List.flatMap_singleton, + nodeBlock, hrun'] + exact key T + +end Accumulate + end Cslib.Circuits.Frontier.ChildCursor From 207d29dcb87a1a8dded602ffcf32defdbcc8b401 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:25:37 -0400 Subject: [PATCH 6/6] feat(circuit/frontier): the stored values are the sums over the mode budget `sumAt_eq_sum_filter` turns the value a call stores for a node and point into the sum over the mode budget, through `sum_filter_weight_lt_eq`. Adds a test of the accumulator on two nodes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/ChildCursor.lean | 31 +++++++++++++++++++ .../Frontier/TensorNetworkChildCursor.lean | 8 +++++ 2 files changed, 39 insertions(+) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean index 60e643d90..27c591193 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildCursor.lean @@ -34,6 +34,14 @@ over counted children consumes. One step reads only the current node's weights a next node's number of modes (`cursorNext_eq_cursorStep`), and it is polynomial-time (`computableInPolyTime_cursorStep`), so the children are enumerated with polynomial delay. +**Accumulating.** `absorbAt` folds a child's value into the accumulator of the call: it multiplies +it into the product over the groups, adds the product to the sum over the exponent tuples after the +last group, and stores the sum after the last tuple. Along `cursorList` this stores, for each node +and point in order, the sum over the tuples of the products over the groups (`runAcc_cursorList`), +seen through any map to a commutative semiring that respects the operations, such as the value of +a coefficient list. With the weights listed along the modes, that sum is the sum over the mode +budget of the right side of (D.16) (`sumAt_eq_sum_filter`). + ## Main definitions * `Cslib.Circuits.Frontier.ChildCursor.cursorList`: the indices `(t, k, β, g)` in order. @@ -42,6 +50,8 @@ next node's number of modes (`cursorNext_eq_cursorStep`), and it is polynomial-t * `Cslib.Circuits.Frontier.ChildCursor.cursorStep`, `Cslib.Circuits.Frontier.ChildCursor.encStepInput`: one step from the data of the nodes, and its input encoding. +* `Cslib.Circuits.Frontier.ChildCursor.absorbAt`, `Cslib.Circuits.Frontier.ChildCursor.runAcc`, + `Cslib.Circuits.Frontier.ChildCursor.sumAt`: the accumulator of a call and the stored values. ## Main results @@ -51,6 +61,9 @@ next node's number of modes (`cursorNext_eq_cursorStep`), and it is polynomial-t `Cslib.Circuits.Frontier.ChildCursor.cursorList_walk`: the cursor walks the list. * `Cslib.Circuits.Frontier.ChildCursor.isChain_flatMap`: a chain of nonempty chained blocks. * `Cslib.Circuits.Frontier.ChildCursor.computableInPolyTime_cursorStep`: polynomial delay. +* `Cslib.Circuits.Frontier.ChildCursor.runAcc_cursorList`, + `Cslib.Circuits.Frontier.ChildCursor.sumAt_eq_sum_filter`: the stored values are the sums over + the mode budget. ## References @@ -588,6 +601,24 @@ theorem runAcc_cursorList (hzero : φ zero = 0) (hr : 0 < r) (hps : ∀ t, 0 < p nodeBlock, hrun'] exact key T +omit hmul hadd hone in +/-- **The stored sum is the sum over the mode budget.** If the weights of node `t` list the +weights `w` of the modes along a duplicate-free list `ms` of all of them, and the product over the +groups of the children of each tuple `l` is `F (ofList ms l)`, then the value stored for `t` and `k` +is the sum of `F` over the tuples of weight below `ps t`, which is +`Cslib.Circuits.Frontier.modeBudget w (ps t)`. -/ +theorem sumAt_eq_sum_filter {M : Type*} [Fintype M] [DecidableEq M] {ms : List M} + (hms : ms.Nodup) (hcover : ∀ Z, Z ∈ ms) {w : M → ℕ} (hw : ∀ Z, 0 < w Z) (val : State → S) + (t k : ℕ) (hwt : ws t = ms.map w) (F : (M → ℕ) → R) + (hF : ∀ l ∈ budgetTuples (ws t) (ps t), + ((List.range r).map fun g => φ (val (t, k, l, g))).prod = F (ofList ms l)) : + sumAt ws ps r φ val t k = ∑ β ∈ ({β ∈ Fintype.piFinset fun _ => Finset.range (ps t) | + ∑ Z, w Z * β Z < ps t} : Finset (M → ℕ)), F β := by + rw [sum_filter_weight_lt_eq hms hcover hw (ps t) F, sumAt, ← hwt] + congr 1 + refine List.map_congr_left fun l hl => ?_ + exact hF l hl + end Accumulate end Cslib.Circuits.Frontier.ChildCursor diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean index e226003f5..092e7b54e 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkChildCursor.lean @@ -43,4 +43,12 @@ example : ∃ h : 0 < (cursorList ws ps 2 1 2).length, cursorList_walk (by norm_num) (by norm_num) (fun _ => by simp [ps]) (fun t w hw => by unfold ws at hw; split_ifs at hw <;> simp at hw <;> omega) (by norm_num) +/-- With the value `t + Σβ + g + 1` at each child, the call stores `1·2 + 2·3 = 8` for node `0` and +`2·3 + 3·4 = 18` for node `1`. -/ +def val (s : State) : ℕ := s.1 + s.2.2.1.sum + s.2.2.2 + 1 + +example : (runAcc ws ps 2 (· * ·) (· + ·) 1 0 val (cursorList ws ps 2 1 2) (1, 0, [])) = + (1, 0, [8, 18]) := by + decide +kernel + end Cslib.Tests.TensorNetworkChildCursor