From d0984cd6017c4398259d5b0ad05cad6429363ca9 Mon Sep 17 00:00:00 2001
From: "aleph-prover[bot]"
 <247409690+aleph-prover[bot]@users.noreply.github.com>
Date: Sun, 31 May 2026 12:11:02 +0000
Subject: [PATCH] Proof for soundness

Automated commit at 20260531_121101
---
 .../Properties/Theorems/Soundness.lean        | 60 ++++++-------------
 1 file changed, 18 insertions(+), 42 deletions(-)

diff --git a/SumcheckProtocol/Properties/Theorems/Soundness.lean b/SumcheckProtocol/Properties/Theorems/Soundness.lean
index 4dad56a..f3db42a 100644
--- a/SumcheckProtocol/Properties/Theorems/Soundness.lean
+++ b/SumcheckProtocol/Properties/Theorems/Soundness.lean
@@ -24,54 +24,30 @@ theorem soundness {𝔽 : Type _} {n : ℕ} [Field 𝔽] [Fintype 𝔽] [Decidab
      probOverChallenges (E := AcceptsAndBadTranscriptOnChallenges ⟨n, Nat.lt_succ_self n⟩ st P)
       ≤ soundnessError st.polynomial := by
   classical
-
-  -- Keep AcceptsAndBad in the per-round event.
-  let E : Fin n → (Fin n → 𝔽) → Prop :=
-    fun i r =>
-      AcceptsAndBadTranscriptOnChallenges ⟨n, Nat.lt_succ_self n⟩ st P r ∧
-        RoundDisagreeButAgreeAtChallenge ⟨n, Nat.lt_succ_self n⟩ st P r i
-
-  -- Step 1: Accepts∧Bad implies ∃ i, (Accepts∧Bad ∧ RoundDisagreeButAgreeAtChallenge i).
+  let E : Fin n → (Fin n → 𝔽) → Prop := fun i r =>
+    AcceptsAndBadTranscriptOnChallenges ⟨n, Nat.lt_succ_self n⟩ st P r ∧
+      RoundDisagreeButAgreeAtChallenge ⟨n, Nat.lt_succ_self n⟩ st P r i
   have hImp :
-      ∀ r : (Fin n → 𝔽),
+      ∀ r,
         AcceptsAndBadTranscriptOnChallenges ⟨n, Nat.lt_succ_self n⟩ st P r →
-          ∃ i : Fin n, E i r := by
+          ∃ i, E i r := by
     intro r hAB
-    rcases
-      accepts_and_bad_implies_exists_round_disagree_but_agree
-        (st := st) (P := P) (r := r) hAB
-      with ⟨i, hi⟩
-    exact ⟨i, ⟨hAB, hi⟩⟩
-
-  have hmono :
-      probOverChallenges (𝔽 := 𝔽) (n := n)
-          (fun r => AcceptsAndBadTranscriptOnChallenges ⟨n, Nat.lt_succ_self n⟩ st P r)
-        ≤
-      probOverChallenges (𝔽 := 𝔽) (n := n)
-          (fun r => ∃ i : Fin n, E i r) :=
-    prob_over_challenges_mono (𝔽 := 𝔽) (n := n) hImp
-
-  -- Step 2: union bound over i.
-  have hunion :
-      probOverChallenges (𝔽 := 𝔽) (n := n)
-          (fun r => ∃ i : Fin n, E i r)
-        ≤
-      (∑ i : Fin n,
-        probOverChallenges (𝔽 := 𝔽) (n := n)
-          (fun r => E i r)) :=
+    rcases accepts_and_bad_implies_exists_round_disagree_but_agree
+        (st := st) (P := P) (r := r) hAB with ⟨i, hi⟩
+    exact ⟨i, hAB, hi⟩
+  have hmono :=
+    prob_over_challenges_mono
+      (E := AcceptsAndBadTranscriptOnChallenges ⟨n, Nat.lt_succ_self n⟩ st P)
+      (F := fun r => ∃ i, E i r)
+      hImp
+  have hunion :=
     prob_over_challenges_exists_le_sum (𝔽 := 𝔽) (n := n) E
-
-  -- Step 3: use the (now-lemma) sumcheck-specific bound.
-  have hround :
-      (∑ i : Fin n,
-        probOverChallenges (𝔽 := 𝔽) (n := n) (fun r => E i r))
-      ≤ soundnessError st.polynomial := by
-    simpa [E, soundnessError] using
-      sum_accepts_and_round_disagree_but_agree_bound
-        (st := st) (P := P)
-
+  have hround := by
+    simpa only [E, soundnessError] using
+      sum_accepts_and_round_disagree_but_agree_bound (st := st) (P := P)
   exact le_trans (le_trans hmono hunion) hround
 
+
 -- Prob verifier accepts transcript when claim is not honest claim
 theorem soundness_dishonest {𝔽 : Type _} {n : ℕ} [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽]
   (st : SumcheckProtocolStatement 𝔽 n)