From c7eb3ca05f1bfde1d0ce28318db53a2111305e0d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:53:33 -0400 Subject: [PATCH 1/5] feat(interactive): sumcheck with a final check, by composition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Lund–Fortnow–Karloff–Nisan sumcheck as a composition of one-round reductions over a finite field, followed by a final evaluation check. Each round (i < n) is perfectly complete and round-by-round sound with error d / |F| (degree bound, g(0) + g(1), one-variable root counting); perfect completeness and soundness n * (d / |F|) of the composed protocol are corollaries of the composition theorems. Milestone 1 (part B) of #643; the per-round proofs were written by a Claude subagent. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 1 + .../Computability/Interactive/Sumcheck.lean | 346 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/Sumcheck.lean | 68 ++++ 4 files changed, 416 insertions(+) create mode 100644 Complexity/Computability/Interactive/Sumcheck.lean create mode 100644 ComplexityTests/Sumcheck.lean diff --git a/Complexity.lean b/Complexity.lean index 8b81552e67..771c03f793 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -823,6 +823,7 @@ public import Complexity.Computability.Interactive.Basic public import Complexity.Computability.Interactive.Plain public import Complexity.Computability.Interactive.Security public import Complexity.Computability.Interactive.Sequential +public import Complexity.Computability.Interactive.Sumcheck public import Complexity.Computability.Kolmogorov.Basic public import Complexity.Computability.Kolmogorov.ChainRule public import Complexity.Computability.Kolmogorov.Depth diff --git a/Complexity/Computability/Interactive/Sumcheck.lean b/Complexity/Computability/Interactive/Sumcheck.lean new file mode 100644 index 0000000000..97391b07cf --- /dev/null +++ b/Complexity/Computability/Interactive/Sumcheck.lean @@ -0,0 +1,346 @@ +/- +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.Computability.Interactive.Sequential +import Complexity.Probability.PMF +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.MvPolynomial.Degrees +public import Mathlib.Algebra.Polynomial.Eval.Defs + +/-! +# Worked example: sumcheck followed by a final evaluation check (design prototype) + +The index is a polynomial `P` in `n` variables over a finite field `F` with every individual +degree at most `d`. A claim `(r, c)` at round `i` states that the sum of `P` over the Boolean +hypercube in the coordinates `i, …, n - 1`, with the coordinates below `i` fixed to `r`, is `c` +(`Sumcheck.rel P i`). At round `0` this is the sumcheck claim `∑_{b ∈ {0,1}ⁿ} P b = c`, and at +round `n` it is the evaluation claim `P r = c`. + +* `Sumcheck.round d P i` reduces `rel P i` to `rel P (i + 1)` in one prover message (a univariate + polynomial) and one uniform challenge. +* `Sumcheck.finalCheck P` reduces `rel P n` to acceptance by evaluating `P` without interaction. +* `Sumcheck.proof d P` is `round 0`, …, `round (n - 1)` followed by `finalCheck`. + +The end-to-end theorems `Sumcheck.proof_complete` and `Sumcheck.proof_sound` are corollaries of +the component theorems through the composition theorems: the soundness error `n * (d / |F|)` is the +sum of the per-round errors, and no step of the composed protocol is reasoned about directly. +-/ + +@[expose] public section + +namespace Cslib.Interactive.Sumcheck + +open scoped ENNReal +open Spec + +variable {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) + (P : MvPolynomial (Fin n) F) + +/-- A claim: a point, of which only the coordinates below the current round matter, and a value. -/ +abbrev Claim (F : Type) (n : ℕ) : Type := (Fin n → F) × F + +/-- The point `r` with the coordinates from `i` on read from the Boolean point `b`. -/ +def splice (i : ℕ) (r : Fin n → F) (b : Fin n → Bool) : Fin n → F := + fun j => if j.val < i then r j else if b j then 1 else 0 + +/-- The sum of `P` over the Boolean hypercube in the coordinates from `i` on, with the coordinates +below `i` fixed to `r`. Each assignment of those coordinates is counted once, by the Boolean point +that is `false` below `i`. -/ +noncomputable def partialSum (i : ℕ) (r : Fin n → F) : F := + ∑ b : Fin n → Bool, + if ∀ j : Fin n, j.val < i → b j = false then MvPolynomial.eval (splice i r b) P else 0 + +/-- The relation of round `i`: the claimed value is the partial sum. There is no witness. -/ +def rel (i : ℕ) : Claim F n → Unit → Prop := fun c _ => partialSum P i c.1 = c.2 + +/-- The honest message of round `i`: the partial sum as a polynomial in coordinate `i`. -/ +noncomputable def roundPoly (i : ℕ) (r : Fin n → F) : Polynomial F := + ∑ b : Fin n → Bool, + if ∀ j : Fin n, j.val ≤ i → b j = false then + MvPolynomial.aeval (fun j => if j.val < i then Polynomial.C (r j) + else if j.val = i then Polynomial.X + else Polynomial.C (if b j then 1 else 0)) P + else 0 + +/-- Set coordinate `i` of `r` to `z`. -/ +def setCoord (i : ℕ) (r : Fin n → F) (z : F) : Fin n → F := fun j => if j.val = i then z else r j + +/-- One round: the prover sends a polynomial, read in full; the verifier sends a field element. -/ +abbrev roundSpec (F : Type) [Semiring F] : Spec := + [.prover (Polynomial F) (OracleInterface.full _), .verifier F] + +/-- The verifier's test of a round polynomial `g` against the claimed value `c`. -/ +abbrev accepts (c : F) (g : Polynomial F) : Prop := g.natDegree ≤ d ∧ g.eval 0 + g.eval 1 = c + +/-- Round `i` of sumcheck. -/ +noncomputable def round (i : ℕ) : + Reduction emptySpec emptySpec (roundSpec F) (Claim F n) Unit (Claim F n) Unit where + prover x _ := + let g := roundPoly P i x.1 + pure (show ProbOracleComp emptySpec (Polynomial F × (F → ProbOracleComp emptySpec _)) from + pure (g, fun z => pure ((setCoord i x.1 z, g.eval z), ()))) + verifier := + { samplers := (ProbComp.uniform F, ()) + decide := fun x c => do + let g ← OracleComp.query (spec := emptySpec ⊕ₒ msgSpec (roundSpec F)) (.inr (.inl ())) + return if accepts d x.2 g then some (setCoord i x.1 c.1, g.eval c.1) else none } + +/-- The final check: evaluate `P` at the claimed point, without interaction. -/ +noncomputable def finalCheck : + Reduction emptySpec emptySpec [] (Claim F n) Unit Unit Unit where + prover _ _ := pure ((), ()) + verifier := + { samplers := () + decide := fun x _ => pure (if MvPolynomial.eval x.1 P = x.2 then some () else none) } + +/-- **Sumcheck followed by the final check**: a proof system for the claim `∑_{b ∈ {0,1}ⁿ} P b = c` +(`rel P 0`). -/ +noncomputable def proof : + Reduction emptySpec emptySpec (iterSpec (roundSpec F) n ++ []) (Claim F n) Unit Unit Unit := + (Reduction.iterate (round d P) n).append (finalCheck P) + +/-! ### The round polynomial -/ + +omit [Fintype F] [DecidableEq F] in +/-- Substituting the variable at coordinate `k` and constants elsewhere gives a polynomial of +degree at most the degree of `P` in `k`. -/ +private theorem natDegree_aeval_le (k : Fin n) (φ : Fin n → Polynomial F) + (hφ : ∀ j, j ≠ k → (φ j).natDegree = 0) (hk : (φ k).natDegree ≤ 1) : + (MvPolynomial.aeval φ P).natDegree ≤ P.degreeOf k := by + conv_lhs => rw [P.as_sum, map_sum] + refine Polynomial.natDegree_sum_le_of_forall_le _ _ fun m hm => ?_ + rw [MvPolynomial.aeval_monomial, Polynomial.algebraMap_eq] + refine (Polynomial.natDegree_C_mul_le _ _).trans ?_ + refine (Polynomial.natDegree_prod_le _ _).trans ?_ + refine le_trans ?_ (MvPolynomial.monomial_le_degreeOf k hm) + calc ∑ j ∈ m.support, ((φ j) ^ m j).natDegree + ≤ ∑ j ∈ m.support, if k = j then m j else 0 := by + refine Finset.sum_le_sum fun j _ => Polynomial.natDegree_pow_le.trans ?_ + by_cases hj : k = j + · subst hj + simpa only [ite_true, mul_one] using Nat.mul_le_mul_left (m k) hk + · rw [hφ j (Ne.symm hj), mul_zero] + exact Nat.zero_le _ + _ ≤ m k := by + rw [Finset.sum_ite_eq] + split_ifs <;> simp + +omit [Fintype F] [DecidableEq F] in +/-- The round polynomial has degree at most `d`. -/ +private theorem natDegree_roundPoly_le (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) + (r : Fin n → F) : (roundPoly P i r).natDegree ≤ d := by + refine Polynomial.natDegree_sum_le_of_forall_le _ _ fun b _ => ?_ + split_ifs + · refine (natDegree_aeval_le P ⟨i, hi⟩ _ (fun j hj => ?_) ?_).trans (hP _) + · have : j.val ≠ i := fun h => hj (Fin.ext h) + simp only [this, ite_false] + split_ifs <;> exact Polynomial.natDegree_C _ + · simp + · simp + +omit [Fintype F] [DecidableEq F] in +/-- The round polynomial evaluated at `t`. -/ +private theorem eval_roundPoly (i : ℕ) (r : Fin n → F) (t : F) : + (roundPoly P i r).eval t = ∑ b : Fin n → Bool, + if ∀ j : Fin n, j.val ≤ i → b j = false then + MvPolynomial.eval (fun j => if j.val < i then r j else if j.val = i then t + else if b j then 1 else 0) P + else 0 := by + rw [roundPoly, Polynomial.eval_finsetSum] + refine Finset.sum_congr rfl fun b _ => ?_ + split_ifs + · rw [← Polynomial.coe_aeval_eq_eval, MvPolynomial.comp_aeval_apply, + MvPolynomial.aeval_eq_eval] + congr 2 + funext j + split_ifs <;> simp + · simp + +omit [Fintype F] [DecidableEq F] in +/-- The round polynomial at `z` is the partial sum of the next round at `r` with `z` at `i`. -/ +private theorem eval_roundPoly_eq (i : ℕ) (r : Fin n → F) (z : F) : + (roundPoly P i r).eval z = partialSum P (i + 1) (setCoord i r z) := by + rw [eval_roundPoly, partialSum] + refine Finset.sum_congr rfl fun b _ => ?_ + simp only [Nat.lt_succ_iff] + congr 3 + funext j + simp only [splice, setCoord] + split_ifs <;> first | rfl | omega + +omit [Fintype F] [DecidableEq F] in +/-- The verifier's test passes on the honest round polynomial: its values at `0` and `1` sum to +the partial sum. -/ +private theorem roundPoly_eval_zero_add_one {i : ℕ} (hi : i < n) (r : Fin n → F) : + (roundPoly P i r).eval 0 + (roundPoly P i r).eval 1 = partialSum P i r := by + obtain ⟨k, hk⟩ : ∃ k : Fin n, k.val = i := ⟨⟨i, hi⟩, rfl⟩ + have hne {j : Fin n} (hj : j.val ≠ i) : j ≠ k := fun h => hj (h ▸ hk) + set G : (Fin n → Bool) → F := fun b => + if ∀ j : Fin n, j.val < i → b j = false then MvPolynomial.eval (splice i r b) P else 0 + -- `σ` flips the Boolean coordinate `k`. + set σ : (Fin n → Bool) → Fin n → Bool := fun b => Function.update b k (!b k) + have hσk (b) : σ b k = !b k := Function.update_self _ _ _ + have hσj (b) (j : Fin n) (hj : j ≠ k) : σ b j = b j := Function.update_of_ne hj _ _ + have hσσ : Function.Involutive σ := fun b => by + funext j + by_cases hj : j = k + · subst hj + rw [hσk, hσk, Bool.not_not] + · rw [hσj _ _ hj, hσj _ _ hj] + have hcond (b : Fin n → Bool) (hb : b k = false) : + (∀ j : Fin n, j.val ≤ i → b j = false) ↔ ∀ j : Fin n, j.val < i → b j = false := by + refine ⟨fun h j hj => h j hj.le, fun h j hj => ?_⟩ + rcases hj.lt_or_eq with hj | hj + · exact h j hj + · obtain rfl : j = k := Fin.ext (hj.trans hk.symm) + exact hb + have hflip : ∑ b, (if b k then 0 else G (σ b)) = ∑ b, (if b k then G b else 0) := by + rw [← Equiv.sum_comp (hσσ.toPerm σ) (fun b => if b k then G b else 0)] + refine Finset.sum_congr rfl fun b _ => ?_ + simp only [Function.Involutive.coe_toPerm, hσk] + cases b k <;> rfl + have hsplit : partialSum P i r = + ∑ b, (if b k then 0 else G b) + ∑ b, (if b k then G b else 0) := by + rw [← Finset.sum_add_distrib] + refine Finset.sum_congr rfl fun b _ => ?_ + cases b k <;> simp [G] + rw [hsplit, ← hflip, eval_roundPoly, eval_roundPoly] + congr 1 <;> refine Finset.sum_congr rfl fun b _ => ?_ <;> cases hb : b k + · simp only [Bool.false_eq_true, ite_false, G] + refine if_congr (hcond b hb) (congrArg (MvPolynomial.eval · P) (funext fun j => ?_)) rfl + by_cases hj : j.val = i + · obtain rfl : j = k := Fin.ext (hj.trans hk.symm) + simp [splice, hk, hb] + · simp [splice, hj] + · rw [ite_eq_left rfl, ite_eq_right fun h => by simpa [hb] using h k hk.le] + · simp only [Bool.false_eq_true, ite_false, G] + refine if_congr ((hcond b hb).trans (forall_congr' fun j => imp_congr_right fun hj => ?_)) + (congrArg (MvPolynomial.eval · P) (funext fun j => ?_)) rfl + · rw [hσj b j (hne hj.ne)] + · by_cases hj : j.val = i + · obtain rfl : j = k := Fin.ext (hj.trans hk.symm) + simp [splice, hk, hσk, hb] + · simp [splice, hj, hσj b j (hne hj)] + · rw [ite_eq_left rfl, ite_eq_right fun h => by simpa [hb] using h k hk.le] + +omit [Fintype F] [DecidableEq F] in +/-- At round `n` all coordinates are fixed: the partial sum is the evaluation. -/ +theorem partialSum_self (r : Fin n → F) : partialSum P n r = MvPolynomial.eval r P := by + rw [partialSum, Finset.sum_eq_single (fun _ => false)] + · have : splice n r (fun _ => false) = r := funext fun j => by simp [splice, j.isLt] + simp [this] + · intro b _ hb + have : ¬ ∀ j : Fin n, j.val < n → b j = false := + fun h => hb (funext fun j => h j j.isLt) + simp only [this, ite_false] + · exact fun h => absurd (Finset.mem_univ _) h + +/-- The verifier of round `i` outputs the claim at the challenge if it accepts the message. -/ +private theorem round_outputOn (i : ℕ) (x : Claim F n) (τ : Transcript (roundSpec F)) : + (round d P i).verifier.outputOn x τ = + if accepts d x.2 τ.1 then some (setCoord i x.1 τ.2.1, τ.1.eval τ.2.1) else none := + rfl + +/-! ### Component theorems (milestone 2) -/ + +/-- Each round is perfectly complete. -/ +theorem round_complete (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) : + (round d P i).Complete World.plain (rel P i) (rel P (i + 1)) 0 := by + intro x w hxw + rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] + simp only [round, runStrategy, plainLaw_bind, plainLaw_pure, plainLaw_sample, PMF.pure_bind, + PMF.bind_bind] + have hacc : accepts d x.2 (roundPoly P i x.1) := + ⟨natDegree_roundPoly_le d P hP hi x.1, (roundPoly_eval_zero_add_one P hi x.1).trans hxw⟩ + rw [PMF.toOuterMeasure_bind_apply] + refine Probability.PMF.tsum_mul_le_of_forall_le _ fun z => le_of_eq ?_ + refine (PMF.toOuterMeasure_pure_apply _ _).trans (ite_eq_right fun h => h ⟨?_, ?_⟩) + · exact (round_outputOn d P i x _).trans (ite_eq_left hacc) + · exact (eval_roundPoly_eq P i x.1 z).symm + +/-- Each round is round-by-round sound with error `d / |F|` (Schwartz–Zippel for one variable). -/ +theorem round_rbrSound (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) : + (round d P i).verifier.RbrSound (language (rel P i)) (language (rel P (i + 1))) + ((d : ℝ≥0∞) / Fintype.card F, ()) := by + refine ⟨fun x p => match p with + | none => partialSum P i x.1 = x.2 + | some (g, none) => accepts d x.2 g ∧ g = roundPoly P i x.1 + | some (g, some (z, _)) => accepts d x.2 g ∧ g.eval z = (roundPoly P i x.1).eval z, + fun x hx h => hx ⟨(), h⟩, fun x => ⟨?_, fun g => ⟨?_, fun z => ?_⟩⟩⟩ + · rintro hS m ⟨hacc, rfl⟩ + exact hS ((roundPoly_eval_zero_add_one P hi x.1).symm.trans hacc.2) + · intro hS + change (ProbComp.eval (ProbComp.uniform F)).toOuterMeasure + {c | accepts d x.2 g ∧ g.eval c = (roundPoly P i x.1).eval c} ≤ (d : ℝ≥0∞) / Fintype.card F + by_cases hacc : accepts d x.2 g + · have hne : g - roundPoly P i x.1 ≠ 0 := sub_ne_zero.mpr fun h => hS ⟨hacc, h⟩ + classical + rw [ProbComp.eval_uniform, Probability.PMF.toOuterMeasure_uniformOfFintype, div_eq_mul_inv] + gcongr + have hsub : Finset.univ.filter + (· ∈ {c | accepts d x.2 g ∧ g.eval c = (roundPoly P i x.1).eval c}) ⊆ + (g - roundPoly P i x.1).roots.toFinset := by + intro c hc + simp only [Finset.mem_filter, Set.mem_ofPred_eq] at hc + rw [Multiset.mem_toFinset, Polynomial.mem_roots hne, Polynomial.IsRoot, + Polynomial.eval_sub, hc.2.2, sub_self] + exact_mod_cast (Finset.card_le_card hsub).trans ((Multiset.toFinset_card_le _).trans + ((Polynomial.card_roots' _).trans ((Polynomial.natDegree_sub_le _ _).trans + (max_le hacc.1 (natDegree_roundPoly_le d P hP hi x.1))))) + · simp [hacc] + · rintro hS ⟨x', ⟨_, hx'⟩, hout⟩ + rw [round_outputOn] at hout + split_ifs at hout with hacc + obtain rfl := Option.some.inj hout + exact hS ⟨hacc, hx'.symm.trans (eval_roundPoly_eq P i x.1 z).symm⟩ + +omit [Fintype F] in +/-- The final check is perfectly complete. -/ +theorem finalCheck_complete : + (finalCheck P).Complete World.plain (rel P n) Accept 0 := by + intro x w hxw + rw [rel, partialSum_self] at hxw + rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] + simp only [finalCheck, runStrategy, plainLaw_bind, plainLaw_pure, PMF.pure_bind] + refine le_of_eq ((PMF.toOuterMeasure_pure_apply _ _).trans + (ite_eq_right fun h => h ⟨?_, trivial⟩)) + exact ite_eq_left hxw + +omit [Fintype F] in +/-- The final check is round-by-round sound without error. -/ +theorem finalCheck_rbrSound : + (finalCheck P).verifier.RbrSound (language (rel P n)) Set.univ () := by + refine ⟨fun x _ => MvPolynomial.eval x.1 P = x.2, + fun x hx h => hx ⟨(), by rw [rel, partialSum_self]; exact h⟩, + fun x hS ⟨x', _, hout⟩ => hS ?_⟩ + by_contra h + simp [Verifier.outputOn, finalCheck, h] at hout + +/-! ### End-to-end theorems, by composition -/ + +/-- **Completeness of sumcheck with the final check.** -/ +theorem proof_complete (hP : ∀ j, P.degreeOf j ≤ d) : + (proof d P).Complete World.plain (rel P 0) Accept 0 := by + have h := (Reduction.Complete.iterate (rel := rel P) n fun i hi => + round_complete d P hP hi).append (finalCheck_complete P) + simp only [Finset.sum_const_zero, add_zero] at h + exact h + +/-- **Soundness of sumcheck with the final check**: a false claim is accepted with probability at +most `n * (d / |F|)`. -/ +theorem proof_sound (hP : ∀ j, P.degreeOf j ≤ d) : + (proof d P).verifier.Sound (oP := emptySpec) World.plain (language (rel P 0)) Set.univ + (n * ((d : ℝ≥0∞) / Fintype.card F)) := by + have h := ((Verifier.RbrSound.iterate (R := round d P) (L := fun i => language (rel P i)) n + fun i hi => round_rbrSound d P hP hi).append (finalCheck_rbrSound P)).sound + simp only [PerChallenge.sum_append, PerChallenge.sum_iterate] at h + simp only [PerChallenge.sum, add_zero, Finset.sum_const, Finset.card_range, nsmul_eq_mul] at h + exact h + +end Cslib.Interactive.Sumcheck diff --git a/ComplexityTests.lean b/ComplexityTests.lean index a5fbb80413..71769750b5 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -426,6 +426,7 @@ import ComplexityTests.SparseLanguages import ComplexityTests.SparseMemory import ComplexityTests.StatefulRefinement import ComplexityTests.SubbotovskayaAndreev +import ComplexityTests.Sumcheck import ComplexityTests.SynthesisBuilder import ComplexityTests.TFNP import ComplexityTests.TFNPCompleteness diff --git a/ComplexityTests/Sumcheck.lean b/ComplexityTests/Sumcheck.lean new file mode 100644 index 0000000000..b6a24dc11f --- /dev/null +++ b/ComplexityTests/Sumcheck.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Interactive.Sumcheck +import Mathlib.Algebra.Field.ZMod +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for the sumcheck protocol + +The polynomial `X₀` in one variable over `ZMod 3` has individual degree `1`. Its hypercube sum is +`0 + 1 = 1`, so the claim `(r, 1)` is true and `(r, 0)` is false. The end-to-end theorems apply: +sumcheck with the final check is perfectly complete and has soundness error `1 / 3`. +-/ + +namespace ComplexityTests.Sumcheck + +open Cslib Cslib.Interactive Cslib.Interactive.Sumcheck +open scoped ENNReal + +instance : Fact (Nat.Prime 3) := ⟨by norm_num⟩ + +/-- The polynomial `X₀` over `ZMod 3`. -/ +noncomputable abbrev P : MvPolynomial (Fin 1) (ZMod 3) := MvPolynomial.X 0 + +/-- `X₀` has individual degree at most `1`. -/ +theorem degreeOf_P_le (j : Fin 1) : P.degreeOf j ≤ 1 := by + rw [MvPolynomial.degreeOf_X] + split_ifs <;> simp + +/-- The hypercube sum of `X₀` is `1`. -/ +theorem partialSum_P (r : Fin 1 → ZMod 3) : partialSum P 0 r = 1 := by + rw [partialSum, ← (Equiv.funUnique (Fin 1) Bool).symm.sum_comp] + simp [splice] + +/-- The true claim. -/ +example (r : Fin 1 → ZMod 3) : rel P 0 (r, 1) () := partialSum_P r + +/-- A false claim. -/ +example (r : Fin 1 → ZMod 3) : ¬ rel P 0 (r, 0) () := by + simp [rel, partialSum_P] + +/-- Sumcheck with the final check is perfectly complete on this instance. -/ +example : (proof 1 P).Complete World.plain (rel P 0) Accept 0 := + proof_complete 1 P degreeOf_P_le + +/-- Sumcheck with the final check is sound with error `1 / 3` on this instance. -/ +example : + (proof 1 P).verifier.Sound (oP := emptySpec) World.plain (language (rel P 0)) Set.univ + (1 / 3) := by + simpa using proof_sound 1 P degreeOf_P_le + +/-- +info: 'Cslib.Interactive.Sumcheck.proof_complete' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Sumcheck.proof_complete + +/-- +info: 'Cslib.Interactive.Sumcheck.proof_sound' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Sumcheck.proof_sound + +end ComplexityTests.Sumcheck From 66997c7f5c56bb0825e7efac5ca2fa0f94ee0279 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:53:33 -0400 Subject: [PATCH 2/5] doc(roadmap): record sumcheck as a client of the interactive core Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ROADMAP.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index a26d0999cb..8959fa81e5 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1232,7 +1232,9 @@ Jukna coverage below is an additional target beyond the V1 port: [sequential composition](Complexity/Computability/Interactive/Sequential.lean) is proved for completeness, soundness, knowledge soundness and round-by-round soundness, and so is per-stage iteration. [Round-by-round soundness implies soundness](Complexity/Computability/Interactive/Plain.lean). - Sumcheck, the first client, is in review (#703). Open, in order: + [Sumcheck with a final evaluation check](Complexity/Computability/Interactive/Sumcheck.lean), + the first client, is perfectly complete and has soundness error `n · d / |F|`; both follow from + the one-round theorems by composition. Open, in order: - the `PublicCoin → IP` bridge, with a uniform word verifier and adversarial decoding; - parallel and AND/OR composition, and round-by-round knowledge soundness; - oracle statements. Today a later phase cannot query an earlier phase's oracle message, From 9a95e464afdaea26e4f9a8aebf642c1aedad27f1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 23:31:22 -0400 Subject: [PATCH 3/5] refactor(interactive): sumcheck claims carry only the challenges so far MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The claim of round `i` is now `Claim F i := (Fin i → F) × F`, and round `i` outputs `(Fin.snoc r z, g.eval z)`. The protocol is a per-stage `Reduction.iterate` over `Claim F`, so `splice`, `setCoord` and the "false below i" filter in `partialSum` are gone: `partialSum P r` sums `P` at `point r b` over `b : Fin (n - i) → Bool`. The component and end-to-end theorems keep their meaning; the end-to-end proofs remain corollaries of `Complete.iterate`/`RbrSound.iterate`, `append` and `sum_iterate`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Computability/Interactive/Sumcheck.lean | 257 ++++++++---------- ComplexityTests/Sumcheck.lean | 15 +- 2 files changed, 128 insertions(+), 144 deletions(-) diff --git a/Complexity/Computability/Interactive/Sumcheck.lean b/Complexity/Computability/Interactive/Sumcheck.lean index 97391b07cf..4bfc86a28f 100644 --- a/Complexity/Computability/Interactive/Sumcheck.lean +++ b/Complexity/Computability/Interactive/Sumcheck.lean @@ -14,22 +14,47 @@ public import Mathlib.Algebra.MvPolynomial.Degrees public import Mathlib.Algebra.Polynomial.Eval.Defs /-! -# Worked example: sumcheck followed by a final evaluation check (design prototype) +# The sumcheck protocol with a final evaluation check The index is a polynomial `P` in `n` variables over a finite field `F` with every individual -degree at most `d`. A claim `(r, c)` at round `i` states that the sum of `P` over the Boolean -hypercube in the coordinates `i, …, n - 1`, with the coordinates below `i` fixed to `r`, is `c` +degree at most `d`. A claim `(r, c)` at round `i` consists of the challenges `r : Fin i → F` of +the earlier rounds and a value `c`. It states that the sum of `P` over the Boolean hypercube in +the coordinates `i, …, n - 1`, with the coordinates below `i` fixed to `r`, is `c` (`Sumcheck.rel P i`). At round `0` this is the sumcheck claim `∑_{b ∈ {0,1}ⁿ} P b = c`, and at round `n` it is the evaluation claim `P r = c`. +This is the protocol of Lund, Fortnow, Karloff and Nisan [LundFortnowKarloffNisan1992] as a +composition of one-round reductions, with each challenge uniform on the field. Each round needs +`i < n`: past the last variable the honest round polynomial is constant, and the round is neither +complete nor round-by-round sound. The TQBF protocol in +`Complexity.Computability.Complexity.Classes.IP.TQBF.Protocol` is a separate, unchanged +development. + +## Main definitions + +* `Sumcheck.Claim F i`: the claims of round `i`, a point of `F^i` and a value. +* `Sumcheck.partialSum P r`: the sum of `P` over the Boolean hypercube in the coordinates from + `i` on, with the coordinates below `i` fixed to `r : Fin i → F`. * `Sumcheck.round d P i` reduces `rel P i` to `rel P (i + 1)` in one prover message (a univariate - polynomial) and one uniform challenge. + polynomial) and one uniform challenge `z`, and appends `z` to the point. * `Sumcheck.finalCheck P` reduces `rel P n` to acceptance by evaluating `P` without interaction. -* `Sumcheck.proof d P` is `round 0`, …, `round (n - 1)` followed by `finalCheck`. +* `Sumcheck.proof d P` is `round 0`, …, `round (n - 1)`, by `Reduction.iterate`, followed by + `finalCheck`. + +## Main results + +* `Sumcheck.round_complete`, `Sumcheck.round_rbrSound`: each round is perfectly complete and + round-by-round sound with error `d / |F|`. +* `Sumcheck.finalCheck_complete`, `Sumcheck.finalCheck_rbrSound`: the final check is perfectly + complete and round-by-round sound without error. +* `Sumcheck.proof_complete`, `Sumcheck.proof_sound`: the end-to-end theorems, corollaries of the + component theorems through the composition theorems. The soundness error `n * (d / |F|)` is the + sum of the per-round errors, and no step of the composed protocol is reasoned about directly. -The end-to-end theorems `Sumcheck.proof_complete` and `Sumcheck.proof_sound` are corollaries of -the component theorems through the composition theorems: the soundness error `n * (d / |F|)` is the -sum of the per-round errors, and no step of the composed protocol is reasoned about directly. +## References + +* [C. Lund, L. Fortnow, H. Karloff, N. Nisan, *Algebraic methods for interactive proof + systems*][LundFortnowKarloffNisan1992] -/ @[expose] public section @@ -42,34 +67,28 @@ open Spec variable {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) -/-- A claim: a point, of which only the coordinates below the current round matter, and a value. -/ -abbrev Claim (F : Type) (n : ℕ) : Type := (Fin n → F) × F +/-- A claim of round `i`: the challenges of the rounds before `i` and the claimed value. -/ +abbrev Claim (F : Type) (i : ℕ) : Type := (Fin i → F) × F -/-- The point `r` with the coordinates from `i` on read from the Boolean point `b`. -/ -def splice (i : ℕ) (r : Fin n → F) (b : Fin n → Bool) : Fin n → F := - fun j => if j.val < i then r j else if b j then 1 else 0 +/-- The point of `F^n` equal to `r` on the first `i` coordinates and to the Boolean point `b` on +the others. -/ +def point {i : ℕ} (r : Fin i → F) (b : Fin (n - i) → Bool) : Fin n → F := + fun j => if h : j.val < i then r ⟨j.val, h⟩ else if b ⟨j.val - i, by omega⟩ then 1 else 0 /-- The sum of `P` over the Boolean hypercube in the coordinates from `i` on, with the coordinates -below `i` fixed to `r`. Each assignment of those coordinates is counted once, by the Boolean point -that is `false` below `i`. -/ -noncomputable def partialSum (i : ℕ) (r : Fin n → F) : F := - ∑ b : Fin n → Bool, - if ∀ j : Fin n, j.val < i → b j = false then MvPolynomial.eval (splice i r b) P else 0 +below `i` fixed to `r`. -/ +noncomputable def partialSum {i : ℕ} (r : Fin i → F) : F := + ∑ b : Fin (n - i) → Bool, MvPolynomial.eval (point r b) P /-- The relation of round `i`: the claimed value is the partial sum. There is no witness. -/ -def rel (i : ℕ) : Claim F n → Unit → Prop := fun c _ => partialSum P i c.1 = c.2 +def rel (i : ℕ) : Claim F i → Unit → Prop := fun c _ => partialSum P c.1 = c.2 /-- The honest message of round `i`: the partial sum as a polynomial in coordinate `i`. -/ -noncomputable def roundPoly (i : ℕ) (r : Fin n → F) : Polynomial F := - ∑ b : Fin n → Bool, - if ∀ j : Fin n, j.val ≤ i → b j = false then - MvPolynomial.aeval (fun j => if j.val < i then Polynomial.C (r j) - else if j.val = i then Polynomial.X - else Polynomial.C (if b j then 1 else 0)) P - else 0 - -/-- Set coordinate `i` of `r` to `z`. -/ -def setCoord (i : ℕ) (r : Fin n → F) (z : F) : Fin n → F := fun j => if j.val = i then z else r j +noncomputable def roundPoly {i : ℕ} (r : Fin i → F) : Polynomial F := + ∑ b : Fin (n - (i + 1)) → Bool, + MvPolynomial.aeval (fun j => if h : j.val < i then Polynomial.C (r ⟨j.val, h⟩) + else if h' : j.val = i then Polynomial.X + else Polynomial.C (if b ⟨j.val - (i + 1), by omega⟩ then 1 else 0)) P /-- One round: the prover sends a polynomial, read in full; the verifier sends a field element. -/ abbrev roundSpec (F : Type) [Semiring F] : Spec := @@ -78,18 +97,19 @@ abbrev roundSpec (F : Type) [Semiring F] : Spec := /-- The verifier's test of a round polynomial `g` against the claimed value `c`. -/ abbrev accepts (c : F) (g : Polynomial F) : Prop := g.natDegree ≤ d ∧ g.eval 0 + g.eval 1 = c -/-- Round `i` of sumcheck. -/ +/-- Round `i` of sumcheck: on the claim `(r, c)` and the challenge `z`, the new claim is +`(Fin.snoc r z, g.eval z)` for the prover's polynomial `g`. -/ noncomputable def round (i : ℕ) : - Reduction emptySpec emptySpec (roundSpec F) (Claim F n) Unit (Claim F n) Unit where + Reduction emptySpec emptySpec (roundSpec F) (Claim F i) Unit (Claim F (i + 1)) Unit where prover x _ := - let g := roundPoly P i x.1 + let g := roundPoly P x.1 pure (show ProbOracleComp emptySpec (Polynomial F × (F → ProbOracleComp emptySpec _)) from - pure (g, fun z => pure ((setCoord i x.1 z, g.eval z), ()))) + pure (g, fun z => pure ((Fin.snoc x.1 z, g.eval z), ()))) verifier := { samplers := (ProbComp.uniform F, ()) decide := fun x c => do let g ← OracleComp.query (spec := emptySpec ⊕ₒ msgSpec (roundSpec F)) (.inr (.inl ())) - return if accepts d x.2 g then some (setCoord i x.1 c.1, g.eval c.1) else none } + return if accepts d x.2 g then some (Fin.snoc x.1 c.1, g.eval c.1) else none } /-- The final check: evaluate `P` at the claimed point, without interaction. -/ noncomputable def finalCheck : @@ -102,8 +122,10 @@ noncomputable def finalCheck : /-- **Sumcheck followed by the final check**: a proof system for the claim `∑_{b ∈ {0,1}ⁿ} P b = c` (`rel P 0`). -/ noncomputable def proof : - Reduction emptySpec emptySpec (iterSpec (roundSpec F) n ++ []) (Claim F n) Unit Unit Unit := - (Reduction.iterate (round d P) n).append (finalCheck P) + Reduction emptySpec emptySpec (iterSpec (fun _ => roundSpec F) n ++ []) (Claim F 0) Unit + Unit Unit := + (Reduction.iterate (s := fun _ => roundSpec F) (S := Claim F) (W := fun _ => Unit) + (round d P) n).append (finalCheck P) /-! ### The round polynomial -/ @@ -134,117 +156,78 @@ private theorem natDegree_aeval_le (k : Fin n) (φ : Fin n → Polynomial F) omit [Fintype F] [DecidableEq F] in /-- The round polynomial has degree at most `d`. -/ private theorem natDegree_roundPoly_le (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) - (r : Fin n → F) : (roundPoly P i r).natDegree ≤ d := by + (r : Fin i → F) : (roundPoly P r).natDegree ≤ d := by refine Polynomial.natDegree_sum_le_of_forall_le _ _ fun b _ => ?_ - split_ifs - · refine (natDegree_aeval_le P ⟨i, hi⟩ _ (fun j hj => ?_) ?_).trans (hP _) - · have : j.val ≠ i := fun h => hj (Fin.ext h) - simp only [this, ite_false] - split_ifs <;> exact Polynomial.natDegree_C _ - · simp + refine (natDegree_aeval_le P ⟨i, hi⟩ _ (fun j hj => ?_) ?_).trans (hP _) + · have : j.val ≠ i := fun h => hj (Fin.ext h) + split_ifs <;> exact Polynomial.natDegree_C _ · simp +omit [Field F] [Fintype F] [DecidableEq F] in +/-- The coordinate `j < i + 1` of `Fin.snoc r z`. -/ +private theorem snoc_mk {i : ℕ} (r : Fin i → F) (z : F) {j : ℕ} (hj : j < i + 1) : + (Fin.snoc r z : Fin (i + 1) → F) ⟨j, hj⟩ = if h : j < i then r ⟨j, h⟩ else z := + rfl + omit [Fintype F] [DecidableEq F] in -/-- The round polynomial evaluated at `t`. -/ -private theorem eval_roundPoly (i : ℕ) (r : Fin n → F) (t : F) : - (roundPoly P i r).eval t = ∑ b : Fin n → Bool, - if ∀ j : Fin n, j.val ≤ i → b j = false then - MvPolynomial.eval (fun j => if j.val < i then r j else if j.val = i then t - else if b j then 1 else 0) P - else 0 := by - rw [roundPoly, Polynomial.eval_finsetSum] +/-- The round polynomial at `z` is the partial sum of the next round at the point extended +by `z`. -/ +private theorem eval_roundPoly_eq {i : ℕ} (r : Fin i → F) (z : F) : + (roundPoly P r).eval z = partialSum P (Fin.snoc r z) := by + rw [roundPoly, Polynomial.eval_finsetSum, partialSum] refine Finset.sum_congr rfl fun b _ => ?_ - split_ifs - · rw [← Polynomial.coe_aeval_eq_eval, MvPolynomial.comp_aeval_apply, - MvPolynomial.aeval_eq_eval] - congr 2 - funext j - split_ifs <;> simp - · simp + rw [← Polynomial.coe_aeval_eq_eval, MvPolynomial.comp_aeval_apply, + MvPolynomial.aeval_eq_eval] + congr 2 + funext j + simp only [point, snoc_mk] + split_ifs <;> first | omega | simp omit [Fintype F] [DecidableEq F] in -/-- The round polynomial at `z` is the partial sum of the next round at `r` with `z` at `i`. -/ -private theorem eval_roundPoly_eq (i : ℕ) (r : Fin n → F) (z : F) : - (roundPoly P i r).eval z = partialSum P (i + 1) (setCoord i r z) := by - rw [eval_roundPoly, partialSum] - refine Finset.sum_congr rfl fun b _ => ?_ - simp only [Nat.lt_succ_iff] - congr 3 +/-- Split a Boolean point of length `m + 1` into its first coordinate and the others. -/ +private theorem sum_bool_succ {k m : ℕ} (h : k = m + 1) (f : (Fin k → Bool) → F) : + ∑ b, f b = ∑ c : Bool, ∑ b' : Fin m → Bool, + f (fun j => if h0 : j.val = 0 then c else b' ⟨j.val - 1, by omega⟩) := by + subst h + rw [← (Fin.consEquiv fun _ => Bool).sum_comp, Fintype.sum_prod_type] + refine Fintype.sum_congr _ _ fun c => Fintype.sum_congr _ _ fun b' => congrArg f ?_ + funext j + refine Fin.cases ?_ (fun j => ?_) j <;> simp + +omit [Fintype F] [DecidableEq F] in +/-- Fixing coordinate `i` to the Boolean value `c` is reading `c` as the first of the Boolean +coordinates of round `i`. -/ +private theorem point_snoc {i : ℕ} (r : Fin i → F) (c : Bool) (b : Fin (n - (i + 1)) → Bool) : + point (Fin.snoc r (if c then (1 : F) else 0)) b = + point r (fun j => if h0 : j.val = 0 then c else b ⟨j.val - 1, by omega⟩) := by funext j - simp only [splice, setCoord] - split_ifs <;> first | rfl | omega + simp only [point, snoc_mk] + split_ifs <;> first | omega | simp_all [Nat.sub_sub] omit [Fintype F] [DecidableEq F] in /-- The verifier's test passes on the honest round polynomial: its values at `0` and `1` sum to the partial sum. -/ -private theorem roundPoly_eval_zero_add_one {i : ℕ} (hi : i < n) (r : Fin n → F) : - (roundPoly P i r).eval 0 + (roundPoly P i r).eval 1 = partialSum P i r := by - obtain ⟨k, hk⟩ : ∃ k : Fin n, k.val = i := ⟨⟨i, hi⟩, rfl⟩ - have hne {j : Fin n} (hj : j.val ≠ i) : j ≠ k := fun h => hj (h ▸ hk) - set G : (Fin n → Bool) → F := fun b => - if ∀ j : Fin n, j.val < i → b j = false then MvPolynomial.eval (splice i r b) P else 0 - -- `σ` flips the Boolean coordinate `k`. - set σ : (Fin n → Bool) → Fin n → Bool := fun b => Function.update b k (!b k) - have hσk (b) : σ b k = !b k := Function.update_self _ _ _ - have hσj (b) (j : Fin n) (hj : j ≠ k) : σ b j = b j := Function.update_of_ne hj _ _ - have hσσ : Function.Involutive σ := fun b => by - funext j - by_cases hj : j = k - · subst hj - rw [hσk, hσk, Bool.not_not] - · rw [hσj _ _ hj, hσj _ _ hj] - have hcond (b : Fin n → Bool) (hb : b k = false) : - (∀ j : Fin n, j.val ≤ i → b j = false) ↔ ∀ j : Fin n, j.val < i → b j = false := by - refine ⟨fun h j hj => h j hj.le, fun h j hj => ?_⟩ - rcases hj.lt_or_eq with hj | hj - · exact h j hj - · obtain rfl : j = k := Fin.ext (hj.trans hk.symm) - exact hb - have hflip : ∑ b, (if b k then 0 else G (σ b)) = ∑ b, (if b k then G b else 0) := by - rw [← Equiv.sum_comp (hσσ.toPerm σ) (fun b => if b k then G b else 0)] - refine Finset.sum_congr rfl fun b _ => ?_ - simp only [Function.Involutive.coe_toPerm, hσk] - cases b k <;> rfl - have hsplit : partialSum P i r = - ∑ b, (if b k then 0 else G b) + ∑ b, (if b k then G b else 0) := by - rw [← Finset.sum_add_distrib] - refine Finset.sum_congr rfl fun b _ => ?_ - cases b k <;> simp [G] - rw [hsplit, ← hflip, eval_roundPoly, eval_roundPoly] - congr 1 <;> refine Finset.sum_congr rfl fun b _ => ?_ <;> cases hb : b k - · simp only [Bool.false_eq_true, ite_false, G] - refine if_congr (hcond b hb) (congrArg (MvPolynomial.eval · P) (funext fun j => ?_)) rfl - by_cases hj : j.val = i - · obtain rfl : j = k := Fin.ext (hj.trans hk.symm) - simp [splice, hk, hb] - · simp [splice, hj] - · rw [ite_eq_left rfl, ite_eq_right fun h => by simpa [hb] using h k hk.le] - · simp only [Bool.false_eq_true, ite_false, G] - refine if_congr ((hcond b hb).trans (forall_congr' fun j => imp_congr_right fun hj => ?_)) - (congrArg (MvPolynomial.eval · P) (funext fun j => ?_)) rfl - · rw [hσj b j (hne hj.ne)] - · by_cases hj : j.val = i - · obtain rfl : j = k := Fin.ext (hj.trans hk.symm) - simp [splice, hk, hσk, hb] - · simp [splice, hj, hσj b j (hne hj)] - · rw [ite_eq_left rfl, ite_eq_right fun h => by simpa [hb] using h k hk.le] +private theorem roundPoly_eval_zero_add_one {i : ℕ} (hi : i < n) (r : Fin i → F) : + (roundPoly P r).eval 0 + (roundPoly P r).eval 1 = partialSum P r := by + rw [eval_roundPoly_eq, eval_roundPoly_eq, add_comm] + conv_rhs => rw [partialSum, sum_bool_succ (show n - i = n - (i + 1) + 1 by omega), + Fintype.sum_bool] + congr 1 + · exact Finset.sum_congr rfl fun b _ => congrArg (MvPolynomial.eval · P) (point_snoc r true b) + · exact Finset.sum_congr rfl fun b _ => congrArg (MvPolynomial.eval · P) (point_snoc r false b) omit [Fintype F] [DecidableEq F] in /-- At round `n` all coordinates are fixed: the partial sum is the evaluation. -/ -theorem partialSum_self (r : Fin n → F) : partialSum P n r = MvPolynomial.eval r P := by +theorem partialSum_self (r : Fin n → F) : partialSum P r = MvPolynomial.eval r P := by rw [partialSum, Finset.sum_eq_single (fun _ => false)] - · have : splice n r (fun _ => false) = r := funext fun j => by simp [splice, j.isLt] - simp [this] - · intro b _ hb - have : ¬ ∀ j : Fin n, j.val < n → b j = false := - fun h => hb (funext fun j => h j j.isLt) - simp only [this, ite_false] + · exact congrArg (MvPolynomial.eval · P) (funext fun j => dite_eq_left j.isLt) + · exact fun b _ hb => absurd (funext fun j => absurd j.isLt (by omega)) hb · exact fun h => absurd (Finset.mem_univ _) h /-- The verifier of round `i` outputs the claim at the challenge if it accepts the message. -/ -private theorem round_outputOn (i : ℕ) (x : Claim F n) (τ : Transcript (roundSpec F)) : +private theorem round_outputOn (i : ℕ) (x : Claim F i) (τ : Transcript (roundSpec F)) : (round d P i).verifier.outputOn x τ = - if accepts d x.2 τ.1 then some (setCoord i x.1 τ.2.1, τ.1.eval τ.2.1) else none := + if accepts d x.2 τ.1 then some (Fin.snoc x.1 τ.2.1, τ.1.eval τ.2.1) else none := rfl /-! ### Component theorems (milestone 2) -/ @@ -256,36 +239,36 @@ theorem round_complete (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) : rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] simp only [round, runStrategy, plainLaw_bind, plainLaw_pure, plainLaw_sample, PMF.pure_bind, PMF.bind_bind] - have hacc : accepts d x.2 (roundPoly P i x.1) := + have hacc : accepts d x.2 (roundPoly P x.1) := ⟨natDegree_roundPoly_le d P hP hi x.1, (roundPoly_eval_zero_add_one P hi x.1).trans hxw⟩ rw [PMF.toOuterMeasure_bind_apply] refine Probability.PMF.tsum_mul_le_of_forall_le _ fun z => le_of_eq ?_ refine (PMF.toOuterMeasure_pure_apply _ _).trans (ite_eq_right fun h => h ⟨?_, ?_⟩) · exact (round_outputOn d P i x _).trans (ite_eq_left hacc) - · exact (eval_roundPoly_eq P i x.1 z).symm + · exact (eval_roundPoly_eq P x.1 z).symm /-- Each round is round-by-round sound with error `d / |F|` (Schwartz–Zippel for one variable). -/ theorem round_rbrSound (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) : (round d P i).verifier.RbrSound (language (rel P i)) (language (rel P (i + 1))) ((d : ℝ≥0∞) / Fintype.card F, ()) := by refine ⟨fun x p => match p with - | none => partialSum P i x.1 = x.2 - | some (g, none) => accepts d x.2 g ∧ g = roundPoly P i x.1 - | some (g, some (z, _)) => accepts d x.2 g ∧ g.eval z = (roundPoly P i x.1).eval z, + | none => partialSum P x.1 = x.2 + | some (g, none) => accepts d x.2 g ∧ g = roundPoly P x.1 + | some (g, some (z, _)) => accepts d x.2 g ∧ g.eval z = (roundPoly P x.1).eval z, fun x hx h => hx ⟨(), h⟩, fun x => ⟨?_, fun g => ⟨?_, fun z => ?_⟩⟩⟩ · rintro hS m ⟨hacc, rfl⟩ exact hS ((roundPoly_eval_zero_add_one P hi x.1).symm.trans hacc.2) · intro hS change (ProbComp.eval (ProbComp.uniform F)).toOuterMeasure - {c | accepts d x.2 g ∧ g.eval c = (roundPoly P i x.1).eval c} ≤ (d : ℝ≥0∞) / Fintype.card F + {c | accepts d x.2 g ∧ g.eval c = (roundPoly P x.1).eval c} ≤ (d : ℝ≥0∞) / Fintype.card F by_cases hacc : accepts d x.2 g - · have hne : g - roundPoly P i x.1 ≠ 0 := sub_ne_zero.mpr fun h => hS ⟨hacc, h⟩ + · have hne : g - roundPoly P x.1 ≠ 0 := sub_ne_zero.mpr fun h => hS ⟨hacc, h⟩ classical rw [ProbComp.eval_uniform, Probability.PMF.toOuterMeasure_uniformOfFintype, div_eq_mul_inv] gcongr have hsub : Finset.univ.filter - (· ∈ {c | accepts d x.2 g ∧ g.eval c = (roundPoly P i x.1).eval c}) ⊆ - (g - roundPoly P i x.1).roots.toFinset := by + (· ∈ {c | accepts d x.2 g ∧ g.eval c = (roundPoly P x.1).eval c}) ⊆ + (g - roundPoly P x.1).roots.toFinset := by intro c hc simp only [Finset.mem_filter, Set.mem_ofPred_eq] at hc rw [Multiset.mem_toFinset, Polynomial.mem_roots hne, Polynomial.IsRoot, @@ -298,7 +281,7 @@ theorem round_rbrSound (hP : ∀ j, P.degreeOf j ≤ d) {i : ℕ} (hi : i < n) : rw [round_outputOn] at hout split_ifs at hout with hacc obtain rfl := Option.some.inj hout - exact hS ⟨hacc, hx'.symm.trans (eval_roundPoly_eq P i x.1 z).symm⟩ + exact hS ⟨hacc, hx'.symm.trans (eval_roundPoly_eq P x.1 z).symm⟩ omit [Fintype F] in /-- The final check is perfectly complete. -/ diff --git a/ComplexityTests/Sumcheck.lean b/ComplexityTests/Sumcheck.lean index b6a24dc11f..5a4d6d288e 100644 --- a/ComplexityTests/Sumcheck.lean +++ b/ComplexityTests/Sumcheck.lean @@ -12,8 +12,8 @@ import Mathlib.Tactic.NormNum.Prime # Tests for the sumcheck protocol The polynomial `X₀` in one variable over `ZMod 3` has individual degree `1`. Its hypercube sum is -`0 + 1 = 1`, so the claim `(r, 1)` is true and `(r, 0)` is false. The end-to-end theorems apply: -sumcheck with the final check is perfectly complete and has soundness error `1 / 3`. +`0 + 1 = 1`, so the initial claim `(![], 1)` is true and `(![], 0)` is false. The end-to-end +theorems apply: sumcheck with the final check is perfectly complete and has soundness error `1 / 3`. -/ namespace ComplexityTests.Sumcheck @@ -32,15 +32,16 @@ theorem degreeOf_P_le (j : Fin 1) : P.degreeOf j ≤ 1 := by split_ifs <;> simp /-- The hypercube sum of `X₀` is `1`. -/ -theorem partialSum_P (r : Fin 1 → ZMod 3) : partialSum P 0 r = 1 := by - rw [partialSum, ← (Equiv.funUnique (Fin 1) Bool).symm.sum_comp] - simp [splice] +theorem partialSum_P : partialSum P (![] : Fin 0 → ZMod 3) = 1 := by + change ∑ b : Fin 1 → Bool, MvPolynomial.eval (point ![] b) P = 1 + rw [← (Equiv.funUnique (Fin 1) Bool).symm.sum_comp] + simp [point] /-- The true claim. -/ -example (r : Fin 1 → ZMod 3) : rel P 0 (r, 1) () := partialSum_P r +example : rel P 0 (![], 1) () := partialSum_P /-- A false claim. -/ -example (r : Fin 1 → ZMod 3) : ¬ rel P 0 (r, 0) () := by +example : ¬ rel P 0 (![], 0) () := by simp [rel, partialSum_P] /-- Sumcheck with the final check is perfectly complete on this instance. -/ From 98c31a0cce1669ce90cef717942f77ef9fce4456 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 02:35:24 -0400 Subject: [PATCH 4/5] refactor(interactive): sumcheck uses the shared empty oracle interface Follows #701's migration to #732's OracleSpec.empty; no statement changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Computability/Interactive/Sumcheck.lean | 17 ++++++++++------- ComplexityTests/Sumcheck.lean | 2 +- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/Complexity/Computability/Interactive/Sumcheck.lean b/Complexity/Computability/Interactive/Sumcheck.lean index 4bfc86a28f..86fc7bdb06 100644 --- a/Complexity/Computability/Interactive/Sumcheck.lean +++ b/Complexity/Computability/Interactive/Sumcheck.lean @@ -100,20 +100,23 @@ abbrev accepts (c : F) (g : Polynomial F) : Prop := g.natDegree ≤ d ∧ g.eval /-- Round `i` of sumcheck: on the claim `(r, c)` and the challenge `z`, the new claim is `(Fin.snoc r z, g.eval z)` for the prover's polynomial `g`. -/ noncomputable def round (i : ℕ) : - Reduction emptySpec emptySpec (roundSpec F) (Claim F i) Unit (Claim F (i + 1)) Unit where + Reduction OracleSpec.empty OracleSpec.empty (roundSpec F) (Claim F i) Unit (Claim F (i + 1)) + Unit where prover x _ := let g := roundPoly P x.1 - pure (show ProbOracleComp emptySpec (Polynomial F × (F → ProbOracleComp emptySpec _)) from + pure (show ProbOracleComp OracleSpec.empty + (Polynomial F × (F → ProbOracleComp OracleSpec.empty _)) from pure (g, fun z => pure ((Fin.snoc x.1 z, g.eval z), ()))) verifier := { samplers := (ProbComp.uniform F, ()) decide := fun x c => do - let g ← OracleComp.query (spec := emptySpec ⊕ₒ msgSpec (roundSpec F)) (.inr (.inl ())) + let g ← OracleComp.query (spec := OracleSpec.empty ⊕ₒ msgSpec (roundSpec F)) + (.inr (.inl ())) return if accepts d x.2 g then some (Fin.snoc x.1 c.1, g.eval c.1) else none } /-- The final check: evaluate `P` at the claimed point, without interaction. -/ noncomputable def finalCheck : - Reduction emptySpec emptySpec [] (Claim F n) Unit Unit Unit where + Reduction OracleSpec.empty OracleSpec.empty [] (Claim F n) Unit Unit Unit where prover _ _ := pure ((), ()) verifier := { samplers := () @@ -122,8 +125,8 @@ noncomputable def finalCheck : /-- **Sumcheck followed by the final check**: a proof system for the claim `∑_{b ∈ {0,1}ⁿ} P b = c` (`rel P 0`). -/ noncomputable def proof : - Reduction emptySpec emptySpec (iterSpec (fun _ => roundSpec F) n ++ []) (Claim F 0) Unit - Unit Unit := + Reduction OracleSpec.empty OracleSpec.empty (iterSpec (fun _ => roundSpec F) n ++ []) + (Claim F 0) Unit Unit Unit := (Reduction.iterate (s := fun _ => roundSpec F) (S := Claim F) (W := fun _ => Unit) (round d P) n).append (finalCheck P) @@ -318,7 +321,7 @@ theorem proof_complete (hP : ∀ j, P.degreeOf j ≤ d) : /-- **Soundness of sumcheck with the final check**: a false claim is accepted with probability at most `n * (d / |F|)`. -/ theorem proof_sound (hP : ∀ j, P.degreeOf j ≤ d) : - (proof d P).verifier.Sound (oP := emptySpec) World.plain (language (rel P 0)) Set.univ + (proof d P).verifier.Sound (oP := OracleSpec.empty) World.plain (language (rel P 0)) Set.univ (n * ((d : ℝ≥0∞) / Fintype.card F)) := by have h := ((Verifier.RbrSound.iterate (R := round d P) (L := fun i => language (rel P i)) n fun i hi => round_rbrSound d P hP hi).append (finalCheck_rbrSound P)).sound diff --git a/ComplexityTests/Sumcheck.lean b/ComplexityTests/Sumcheck.lean index 5a4d6d288e..417825fd87 100644 --- a/ComplexityTests/Sumcheck.lean +++ b/ComplexityTests/Sumcheck.lean @@ -50,7 +50,7 @@ example : (proof 1 P).Complete World.plain (rel P 0) Accept 0 := /-- Sumcheck with the final check is sound with error `1 / 3` on this instance. -/ example : - (proof 1 P).verifier.Sound (oP := emptySpec) World.plain (language (rel P 0)) Set.univ + (proof 1 P).verifier.Sound (oP := OracleSpec.empty) World.plain (language (rel P 0)) Set.univ (1 / 3) := by simpa using proof_sound 1 P degreeOf_P_le From eafe6a789f60601a7851c02d8545fb02727012ef Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 04:42:45 -0400 Subject: [PATCH 5/5] chore(interactive): sumcheck imports the split PMF modules (#693) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Computability/Interactive/Sumcheck.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Complexity/Computability/Interactive/Sumcheck.lean b/Complexity/Computability/Interactive/Sumcheck.lean index 86fc7bdb06..b643dda5b9 100644 --- a/Complexity/Computability/Interactive/Sumcheck.lean +++ b/Complexity/Computability/Interactive/Sumcheck.lean @@ -9,6 +9,8 @@ module public import Complexity.Computability.Interactive.Sequential import Complexity.Probability.PMF +import Complexity.Probability.PMF.Bind +import Complexity.Probability.PMF.Uniform import Mathlib.Algebra.BigOperators.Group.Finset.Basic public import Mathlib.Algebra.MvPolynomial.Degrees public import Mathlib.Algebra.Polynomial.Eval.Defs