diff --git a/Examples/OneTimePad.lean b/Examples/OneTimePad.lean
index 9c2af45..ccd360b 100644
--- a/Examples/OneTimePad.lean
+++ b/Examples/OneTimePad.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SymmEncAlg
 import VCVio.OracleComp.Constructions.BitVec
diff --git a/ToMathlib/Data/ENNReal/SumSquares.lean b/ToMathlib/Data/ENNReal/SumSquares.lean
index 5039e30..fd3ef15 100644
--- a/ToMathlib/Data/ENNReal/SumSquares.lean
+++ b/ToMathlib/Data/ENNReal/SumSquares.lean
@@ -53,4 +53,48 @@ lemma sq_sum_le_card_mul_sum_sq {ι' : Type*}
           Finset.mul_sum]
     _ = 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) := by rw [← two_mul]
 
+private lemma tsum_mul_tsum_eq {α : Type*} (g h : α → ℝ≥0∞) :
+    (∑' a, g a) * (∑' b, h b) = ∑' a, ∑' b, g a * h b := by
+  rw [← ENNReal.tsum_mul_right]; congr 1; ext a
+  exact ENNReal.tsum_mul_left.symm
+
+lemma sq_tsum_le_tsum_mul_tsum {α : Type*} (w f : α → ℝ≥0∞) :
+    (∑' a, w a * f a) ^ 2 ≤ (∑' a, w a) * ∑' a, w a * f a ^ 2 := by
+  rw [sq, tsum_mul_tsum_eq, tsum_mul_tsum_eq]
+  have h2 : (2 : ℝ≥0∞) ≠ 0 := two_ne_zero
+  have h2' : (2 : ℝ≥0∞) ≠ ⊤ := by norm_num
+  suffices h : 2 * ∑' a, ∑' b, (w a * f a) * (w b * f b) ≤
+      2 * ∑' a, ∑' b, w a * (w b * f b ^ 2) by
+    calc ∑' a, ∑' b, (w a * f a) * (w b * f b)
+      _ = 2⁻¹ * (2 * ∑' a, ∑' b, (w a * f a) * (w b * f b)) := by
+          rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
+      _ ≤ 2⁻¹ * (2 * ∑' a, ∑' b, w a * (w b * f b ^ 2)) := by gcongr
+      _ = ∑' a, ∑' b, w a * (w b * f b ^ 2) := by
+          rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
+  calc 2 * ∑' a, ∑' b, (w a * f a) * (w b * f b)
+    _ = ∑' a, ∑' b, 2 * ((w a * f a) * (w b * f b)) := by
+        rw [← ENNReal.tsum_mul_left]; congr 1; ext
+        rw [← ENNReal.tsum_mul_left]
+    _ ≤ ∑' a, ∑' b, (w a * (w b * f b ^ 2) + w b * (w a * f a ^ 2)) := by
+        gcongr with a b
+        calc 2 * ((w a * f a) * (w b * f b))
+          _ = w a * w b * (2 * f a * f b) := by ring
+          _ ≤ w a * w b * (f a ^ 2 + f b ^ 2) := by
+              gcongr; exact two_mul_le_add_sq (f a) (f b)
+          _ = w a * (w b * f b ^ 2) + w b * (w a * f a ^ 2) := by ring
+    _ = (∑' a, ∑' b, w a * (w b * f b ^ 2)) +
+          ∑' a, ∑' b, w b * (w a * f a ^ 2) := by
+        simp_rw [← ENNReal.tsum_add]
+    _ = (∑' a, ∑' b, w a * (w b * f b ^ 2)) +
+          ∑' b, ∑' a, w b * (w a * f a ^ 2) := by
+        congr 1; exact ENNReal.tsum_comm
+    _ = 2 * ∑' a, ∑' b, w a * (w b * f b ^ 2) := by rw [two_mul]
+
+lemma sq_tsum_le_tsum_sq {α : Type*} (w f : α → ℝ≥0∞) (hw : ∑' a, w a ≤ 1) :
+    (∑' a, w a * f a) ^ 2 ≤ ∑' a, w a * f a ^ 2 :=
+  calc (∑' a, w a * f a) ^ 2
+    _ ≤ (∑' a, w a) * ∑' a, w a * f a ^ 2 := sq_tsum_le_tsum_mul_tsum w f
+    _ ≤ 1 * ∑' a, w a * f a ^ 2 := by gcongr
+    _ = ∑' a, w a * f a ^ 2 := one_mul _
+
 end ENNReal
diff --git a/VCVio/CryptoFoundations/AsymmEncAlg.lean b/VCVio/CryptoFoundations/AsymmEncAlg.lean
index d2eed39..b0d084d 100644
--- a/VCVio/CryptoFoundations/AsymmEncAlg.lean
+++ b/VCVio/CryptoFoundations/AsymmEncAlg.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.ProbComp
diff --git a/VCVio/CryptoFoundations/FiatShamir.lean b/VCVio/CryptoFoundations/FiatShamir.lean
index 7f63788..f696718 100644
--- a/VCVio/CryptoFoundations/FiatShamir.lean
+++ b/VCVio/CryptoFoundations/FiatShamir.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SigmaAlg
 import VCVio.CryptoFoundations.SignatureAlg
@@ -52,7 +52,21 @@ def FiatShamir (sigmaAlg : SigmaAlg X W PC SC Ω P p)
       (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp)
     StateT.run' (simulateQ (idImpl + ro) comp) ∅
   lift_probComp := monadLift
-  exec_lift_probComp c := by sorry
+  exec_lift_probComp c := by
+    let ro : QueryImpl (M × PC →ₒ Ω)
+      (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp) := randomOracle
+    let idImpl := (QueryImpl.ofLift unifSpec ProbComp).liftTarget
+      (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp)
+    change StateT.run' (simulateQ (idImpl + ro) (monadLift c)) ∅ = c
+    rw [show simulateQ (idImpl + ro) (monadLift c) = simulateQ idImpl c by
+      simpa [MonadLift.monadLift] using
+        (QueryImpl.simulateQ_add_liftComp_left (impl₁' := idImpl) (impl₂' := ro) c)]
+    have hid : ∀ t s, (idImpl t).run' s = query t := by
+      intro t s
+      rfl
+    simpa using
+      (StateT_run'_simulateQ_eq_self (so := idImpl) (h := hid) (oa := c)
+        (s := (∅ : (M × PC →ₒ Ω).QueryCache)))
 
 namespace FiatShamir
 
diff --git a/VCVio/CryptoFoundations/Fork.lean b/VCVio/CryptoFoundations/Fork.lean
index ee87804..a1ca270 100644
--- a/VCVio/CryptoFoundations/Fork.lean
+++ b/VCVio/CryptoFoundations/Fork.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.QueryTracking.SeededOracle
@@ -261,7 +261,6 @@ private lemma probOutput_collision_le_main_div (s : Fin (qb i + 1)) :
               (qc := qb) (js := js) (oa := main) (f := cf)
               (y := (some s : Option (Fin (qb i + 1)))))
 
-set_option maxHeartbeats 800000 in
 /-- Key bound of the forking lemma: the probability that both runs succeed with fork point `s`
 is at least `Pr[cf(main) = s]² - Pr[cf(main) = s] / |Range i|`. -/
 theorem le_probOutput_fork (s : Fin (qb i + 1)) :
@@ -345,32 +344,288 @@ theorem le_probOutput_fork (s : Fin (qb i + 1)) :
       (mx := (liftComp (generateSeed spec qb js) spec : OracleComp spec (QuerySeed spec)))
       (y := z) (z₁ := z) (z₂ := (some s : Option (Fin (qb i + 1))))) ?_
     intro seed hseed
-    stop
     refine (probOutput_bind_congr_le_add
-      (mx := (simulateQ seededOracle main).run' seed)
+      (mx := ((simulateQ seededOracle main).run seed :
+        OracleComp spec (α × QuerySeed spec)))
       (y := z) (z₁ := z) (z₂ := (some s : Option (Fin (qb i + 1))))) ?_
-    intro x₁ hx₁
-    by_cases hcfx₁ : cf x₁ = some s
-    · simp [hcfx₁]
-      refine (probOutput_bind_congr_le_add
-        (mx := (liftComp ($ᵗ spec.Range i) spec : OracleComp spec (spec.Range i)))
-        (y := z) (z₁ := z) (z₂ := (some s : Option (Fin (qb i + 1))))) ?_
-      intro u hu
-      by_cases hu' : (seed i)[↑s]? = some u
-      · simp [hu']
-        exact probOutput_le_one
-      · simp [hu']
-    · have hcfx₁' : (some s : Option (Fin (qb i + 1))) ≠ cf x₁ := by
-        simpa [eq_comm] using hcfx₁
-      simp [hcfx₁, hcfx₁']
+    intro a ha
+    cases hca : cf a.1 with
+    | none =>
+        have hL :
+            Pr[= z | do
+              let u ← liftM ($ᵗ spec.Range i)
+              (fun a₂ : α × QuerySeed spec ↦ some (none, cf a₂.1)) <$>
+                (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)] = 0 := by
+          rw [probOutput_eq_zero_iff]
+          simp [support_bind, support_map, z]
+        rw [hL]
+        simp [z]
+    | some t =>
+        by_cases hts : t = s
+        · cases hts
+          simp [z]
+          refine (probOutput_bind_congr_le_add
+            (mx := (liftComp ($ᵗ spec.Range i) spec : OracleComp spec (spec.Range i)))
+            (y := z) (z₁ := z) (z₂ := (some s : Option (Fin (qb i + 1))))) ?_
+          intro u hu
+          by_cases hu' : (seed i)[↑s]? = some u
+          · have h1 :
+                Pr[= z | (fun a ↦ some (some s, cf a.1)) <$>
+                  (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)] ≤ 1 :=
+                probOutput_le_one
+            have h2 :
+                (1 : ℝ≥0∞) ≤
+                  Pr[= z |
+                      (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                        if (seed i)[↑s]? = some u then pure none
+                        else do
+                          let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                          if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none] +
+                    Pr[= (some s : Option (Fin (qb i + 1))) |
+                      if (seed i)[↑s]? = some u then
+                        (pure (some s) : OracleComp spec (Option (Fin (qb i + 1))))
+                      else pure none] := by
+              have hnonneg :
+                  0 ≤ Pr[= z |
+                      (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                        if (seed i)[↑s]? = some u then pure none
+                        else do
+                          let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                          if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none] := zero_le _
+              have haux :
+                  (1 : ℝ≥0∞) ≤
+                    Pr[= z |
+                        (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                          if (seed i)[↑s]? = some u then pure none
+                          else do
+                            let a_1 ← (simulateQ seededOracle main).run
+                              ((seed.takeAtIndex i ↑s).addValue i u)
+                            if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none] + 1 := by
+                simp
+              simp [hu']
+            exact le_trans h1 h2
+          · have hmono :
+                Pr[= z |
+                  (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u) >>=
+                    (fun x => pure (some (some s, cf x.1)))] ≤
+                Pr[= z |
+                  (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u) >>=
+                    (fun x =>
+                      (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                        (if cf x.1 = some s then pure (some (a.1, x.1)) else pure none))] := by
+              refine probOutput_bind_mono ?_
+              intro x hx
+              by_cases hxs : cf x.1 = some s
+              · simp [hxs, hca, z]
+              · have hrhs_nonneg :
+                    0 ≤ Pr[= z |
+                      (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                        (if cf x.1 = some s then
+                          (pure (some (a.1, x.1)) : OracleComp spec (Option (α × α)))
+                         else pure none)] := zero_le _
+                have hxs' : (some s : Option (Fin (qb i + 1))) ≠ cf x.1 := by
+                  simpa [eq_comm] using hxs
+                simp [hxs, hxs', z]
+            have hu'' : (seed i)[↑s]? ≠ some u := by simpa using hu'
+            have hif :
+                (if (seed i)[↑s]? = some u then
+                    (pure none : OracleComp spec (Option (α × α)))
+                 else
+                    do
+                      let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                      if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none) =
+                (do
+                  let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                  if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none) := by
+              exact if_neg hu''
+            have hmono' :
+                Pr[= z |
+                  (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u) >>=
+                    (fun x => pure (some (some s, cf x.1)))] ≤
+                Pr[= z |
+                  (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                    (if (seed i)[↑s]? = some u then
+                       (pure none : OracleComp spec (Option (α × α)))
+                     else do
+                       let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                       if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none)] := by
+              rw [hif]
+              simpa [map_eq_bind_pure_comp] using hmono
+            have hadd :
+                Pr[= z |
+                  (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                    (if (seed i)[↑s]? = some u then
+                       (pure none : OracleComp spec (Option (α × α)))
+                     else do
+                       let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                       if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none)] ≤
+                  Pr[= z |
+                    (fun r ↦ Option.map (Prod.map cf cf) r) <$>
+                      (if (seed i)[↑s]? = some u then
+                         (pure none : OracleComp spec (Option (α × α)))
+                       else do
+                         let a_1 ← (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)
+                         if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none)] +
+                    Pr[= (some s : Option (Fin (qb i + 1))) |
+                      if (seed i)[↑s]? = some u then
+                        (pure (some s) : OracleComp spec (Option (Fin (qb i + 1))))
+                      else pure none] := by
+              exact le_add_of_nonneg_right (zero_le _)
+            exact le_trans hmono' hadd
+        · have hts' : (some t : Option (Fin (qb i + 1))) ≠ some s := by
+            simpa using hts
+          have hzero :
+              Pr[= z | do
+                let u ← liftM ($ᵗ spec.Range i)
+                (fun a₂ : α × QuerySeed spec ↦ some (some t, cf a₂.1)) <$>
+                  (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)] = 0 := by
+            rw [probOutput_eq_zero_iff]
+            simp [support_bind, support_map, z, hts']
+          have hzero' :
+              Pr[= z | do
+                let u ← liftM ($ᵗ spec.Range i)
+                (fun a₂ : α × QuerySeed spec ↦ some (some t, cf a₂.1)) <$>
+                  (simulateQ seededOracle main).run ((seed.takeAtIndex i ↑s).addValue i u)] = 0 := by
+            simpa using hzero
+          rw [hzero']
+          exact zero_le _
   have hNoGuardMinusLeRhs :
       Pr[= z | noGuardComp] - Pr[= (some s : Option (Fin (qb i + 1))) | collisionComp] ≤
         Pr[= z | f <$> fork main qb js i cf] := by
     exact (tsub_le_iff_right).2 hNoGuardLeAdd
   have hNoGuardGeSquare :
       Pr[= s | cf <$> main] ^ 2 ≤ Pr[= z | noGuardComp] := by
-    -- Remaining core: seed-factorization and weighted-square lower bound.
-    sorry
+    -- Step 1: Express Pr[= s | cf <$> main] as E_σ[P(σ)] via seeded oracle factorization
+    have hMain : (Pr[= s | cf <$> main] : ℝ≥0∞) =
+        ∑' σ, Pr[= σ | generateSeed spec qb js] *
+          Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' σ] := by
+      rw [show (Pr[= s | cf <$> main] : ℝ≥0∞) =
+        Pr[= (some s : Option (Fin (qb i + 1))) |
+          (do let seed ← liftComp (generateSeed spec qb js) spec
+              cf <$> (simulateQ seededOracle main).run' seed :
+            OracleComp spec (Option (Fin (qb i + 1))))] from by
+        simpa using (seededOracle.probOutput_generateSeed_bind_map_simulateQ
+          (qc := qb) (js := js) (oa := main) (f := cf)
+          (y := (some s : Option (Fin (qb i + 1))))).symm]
+      rw [probOutput_bind_eq_tsum]
+      simp_rw [probOutput_liftComp]
+    -- Step 2: Factor Pr[= z | noGuardComp] = ∑' σ, w(σ) * P(σ) * P(take(σ))
+    -- Uses conditional independence (probOutput_bind_bind_prod_mk_eq_mul')
+    -- and the addValue factorization lemma.
+    have hFactor : Pr[= z | noGuardComp] =
+        ∑' σ, Pr[= σ | generateSeed spec qb js] *
+          (Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' σ] *
+           Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run'
+              (σ.takeAtIndex i ↑s)]) := by
+      simp only [noGuardComp, z]
+      rw [probOutput_bind_eq_tsum]
+      simp_rw [probOutput_liftComp]
+      congr 1; ext σ; congr 1
+      have hcomp : (do let x₁ ← (simulateQ seededOracle main).run' σ
+                       let u ← liftComp ($ᵗ spec.Range i) spec
+                       let x₂ ← (simulateQ seededOracle main).run'
+                         ((σ.takeAtIndex i ↑s).addValue i u)
+                       pure (some (cf x₁, cf x₂)) : OracleComp spec _) =
+          some <$> (do let x₁ ← (simulateQ seededOracle main).run' σ
+                       let x₂ ← (liftComp ($ᵗ spec.Range i) spec >>= fun u =>
+                         (simulateQ seededOracle main).run'
+                           ((σ.takeAtIndex i ↑s).addValue i u))
+                       pure (cf x₁, cf x₂)) := by
+        simp only [map_eq_bind_pure_comp, bind_assoc, Function.comp, pure_bind]
+      rw [hcomp, probOutput_some_map_some, probOutput_bind_bind_prod_mk_eq_mul']
+      congr 1
+      have h := seededOracle.evalDist_liftComp_uniformSample_bind_simulateQ_run'_addValue
+        (σ.takeAtIndex i ↑s) i main
+      exact congrFun (congrArg DFunLike.coe (by simp only [evalDist_map, h])) (some s)
+    -- Step 3: Jensen/Cauchy-Schwarz via prefix grouping
+    -- (∑ w * P)² ≤ ∑ w * P * P(take) by decomposing into prefix groups
+    -- and applying sq_tsum_le_tsum_sq.
+    have hJensen :
+        (∑' σ, Pr[= σ | generateSeed spec qb js] *
+          Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' σ]) ^ 2 ≤
+        ∑' σ, Pr[= σ | generateSeed spec qb js] *
+          (Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' σ] *
+           Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run'
+              (σ.takeAtIndex i ↑s)]) := by
+      -- Notation: w(σ) = Pr[=σ|gen], P(σ) = Pr[=y|run'(σ)], Q(σ) = Pr[=y|run'(take(σ))]
+      -- hEq: ∑ w * P = ∑ w * Q (both equal Pr[= some s | cf <$> main])
+      have hMainTake : ∑' σ, Pr[= σ | generateSeed spec qb js] *
+          Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)] =
+          Pr[= (some s : Option (Fin (qb i + 1))) | cf <$> main] := by
+        have hTake :=
+          seededOracle.probOutput_generateSeed_bind_map_simulateQ_takeAtIndex
+            (qc := qb) (js := js) (i₀ := i) (k := ↑s) (oa := main) (f := cf)
+            (y := (some s : Option (Fin (qb i + 1))))
+        rw [probOutput_bind_eq_tsum] at hTake
+        simp_rw [probOutput_liftComp] at hTake
+        exact hTake
+      have hEq : ∑' σ, Pr[= σ | generateSeed spec qb js] *
+          Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' σ] =
+        ∑' σ, Pr[= σ | generateSeed spec qb js] *
+          Pr[= (some s : Option (Fin (qb i + 1))) |
+            cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)] :=
+        by
+          calc
+            ∑' σ, Pr[= σ | generateSeed spec qb js] *
+                Pr[= (some s : Option (Fin (qb i + 1))) |
+                  cf <$> (simulateQ seededOracle main).run' σ]
+              = Pr[= (some s : Option (Fin (qb i + 1))) | cf <$> main] := by
+                  simpa using hMain.symm
+            _ = ∑' σ, Pr[= σ | generateSeed spec qb js] *
+                  Pr[= (some s : Option (Fin (qb i + 1))) |
+                    cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)] := by
+                  simpa using hMainTake.symm
+      -- Jensen: (∑ w * Q)² ≤ ∑ w * Q²
+      set w : QuerySeed spec → ℝ≥0∞ := fun σ => Pr[= σ | generateSeed spec qb js]
+      set Q : QuerySeed spec → ℝ≥0∞ := fun σ =>
+        Pr[= (some s : Option (Fin (qb i + 1))) |
+          cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)]
+      have hw : ∑' σ, w σ ≤ 1 := tsum_probOutput_le_one
+      -- hEq2: ∑ w * Q² = ∑ w * (P * Q) via weighted takeAtIndex faithfulness
+      have hEq2 : ∑' σ, w σ * Q σ ^ 2 =
+          ∑' σ, w σ *
+            (Pr[= (some s : Option (Fin (qb i + 1))) |
+              cf <$> (simulateQ seededOracle main).run' σ] * Q σ) := by
+        simp only [sq, Q, w]
+        have hSim : ∀ σ', (simulateQ seededOracle (cf <$> main :
+            OracleComp spec (Option (Fin (qb i + 1))))).run' σ' =
+            cf <$> (simulateQ seededOracle main).run' σ' := by
+          intro σ'
+          simp only [simulateQ_map]
+          show Prod.fst <$> (Prod.map cf id <$> (simulateQ seededOracle main).run σ') =
+            cf <$> (Prod.fst <$> (simulateQ seededOracle main).run σ')
+          simp [Functor.map_map]
+        have hWF := seededOracle.tsum_probOutput_generateSeed_weight_takeAtIndex
+          qb js i (↑s) (cf <$> main : OracleComp spec (Option (Fin (qb i + 1))))
+          (some s : Option (Fin (qb i + 1)))
+          (fun τ => Pr[= (some s : Option (Fin (qb i + 1))) |
+            (simulateQ seededOracle (cf <$> main :
+              OracleComp spec (Option (Fin (qb i + 1))))).run' τ])
+        simp_rw [hSim] at hWF
+        exact hWF.symm.trans (by congr 1; ext σ; congr 1; exact mul_comm _ _)
+      calc _ = (∑' σ, w σ * Q σ) ^ 2 := by rw [hEq]
+        _ ≤ ∑' σ, w σ * Q σ ^ 2 := ENNReal.sq_tsum_le_tsum_sq w Q hw
+        _ = _ := hEq2
+    calc Pr[= s | cf <$> main] ^ 2
+        = (∑' σ, Pr[= σ | generateSeed spec qb js] *
+            Pr[= (some s : Option (Fin (qb i + 1))) |
+              cf <$> (simulateQ seededOracle main).run' σ]) ^ 2 := by
+          rw [hMain]
+      _ ≤ ∑' σ, Pr[= σ | generateSeed spec qb js] *
+            (Pr[= (some s : Option (Fin (qb i + 1))) |
+              cf <$> (simulateQ seededOracle main).run' σ] *
+             Pr[= (some s : Option (Fin (qb i + 1))) |
+              cf <$> (simulateQ seededOracle main).run'
+                (σ.takeAtIndex i ↑s)]) := hJensen
+      _ = Pr[= z | noGuardComp] := hFactor.symm
   exact le_trans
     (tsub_le_tsub_right hNoGuardGeSquare (Pr[= (some s : Option (Fin (qb i + 1))) | collisionComp]))
     hNoGuardMinusLeRhs
diff --git a/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean b/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean
index e185d07..6aef00f 100644
--- a/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean
+++ b/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.HardnessAssumptions.HardHomogeneousSpace
 
diff --git a/VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean b/VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean
index 55d1318..a7111c9 100644
--- a/VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean
+++ b/VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.ProbComp
diff --git a/VCVio/CryptoFoundations/SecExp.lean b/VCVio/CryptoFoundations/SecExp.lean
index 7e9dd55..7c21667 100644
--- a/VCVio/CryptoFoundations/SecExp.lean
+++ b/VCVio/CryptoFoundations/SecExp.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.ExecutionMethod
 import VCVio.OracleComp.ProbComp
diff --git a/VCVio/CryptoFoundations/SignatureAlg.lean b/VCVio/CryptoFoundations/SignatureAlg.lean
index b04499b..de977fd 100644
--- a/VCVio/CryptoFoundations/SignatureAlg.lean
+++ b/VCVio/CryptoFoundations/SignatureAlg.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.ProbComp
diff --git a/VCVio/CryptoFoundations/SymmEncAlg.lean b/VCVio/CryptoFoundations/SymmEncAlg.lean
index ce49c40..439eeba 100644
--- a/VCVio/CryptoFoundations/SymmEncAlg.lean
+++ b/VCVio/CryptoFoundations/SymmEncAlg.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.EvalDist.Prod
diff --git a/VCVio/EvalDist/Defs/Basic.lean b/VCVio/EvalDist/Defs/Basic.lean
index f96690f..879d647 100644
--- a/VCVio/EvalDist/Defs/Basic.lean
+++ b/VCVio/EvalDist/Defs/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.Support
 
diff --git a/VCVio/EvalDist/Instances/OptionT.lean b/VCVio/EvalDist/Instances/OptionT.lean
index 03f9adf..6312067 100644
--- a/VCVio/EvalDist/Instances/OptionT.lean
+++ b/VCVio/EvalDist/Instances/OptionT.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import ToMathlib.Control.OptionT
 import VCVio.EvalDist.Option
diff --git a/VCVio/EvalDist/List.lean b/VCVio/EvalDist/List.lean
index 6377685..4f4ce9c 100644
--- a/VCVio/EvalDist/List.lean
+++ b/VCVio/EvalDist/List.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.NeverFails
 import ToMathlib.General
diff --git a/VCVio/EvalDist/Monad/Basic.lean b/VCVio/EvalDist/Monad/Basic.lean
index 3b17913..d52adb3 100644
--- a/VCVio/EvalDist/Monad/Basic.lean
+++ b/VCVio/EvalDist/Monad/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.Basic
 
diff --git a/VCVio/EvalDist/Monad/Seq.lean b/VCVio/EvalDist/Monad/Seq.lean
index bd3d714..3fade52 100644
--- a/VCVio/EvalDist/Monad/Seq.lean
+++ b/VCVio/EvalDist/Monad/Seq.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Monad.Map
 
diff --git a/VCVio/OracleComp/Coercions/Add.lean b/VCVio/OracleComp/Coercions/Add.lean
index 541b582..0086859 100644
--- a/VCVio/OracleComp/Coercions/Add.lean
+++ b/VCVio/OracleComp/Coercions/Add.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.Coercions.SubSpec
 import VCVio.OracleComp.ProbComp
diff --git a/VCVio/OracleComp/Coercions/SubSpec.lean b/VCVio/OracleComp/Coercions/SubSpec.lean
index 6c6ac18..e133b78 100644
--- a/VCVio/OracleComp/Coercions/SubSpec.lean
+++ b/VCVio/OracleComp/Coercions/SubSpec.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.SimulateQ
 import VCVio.OracleComp.EvalDist
diff --git a/VCVio/OracleComp/Constructions/GenerateSeed.lean b/VCVio/OracleComp/Constructions/GenerateSeed.lean
index 509a281..f8baaa5 100644
--- a/VCVio/OracleComp/Constructions/GenerateSeed.lean
+++ b/VCVio/OracleComp/Constructions/GenerateSeed.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.Constructions.Replicate
 import VCVio.OracleComp.Constructions.SampleableType
diff --git a/VCVio/OracleComp/Constructions/SampleableType.lean b/VCVio/OracleComp/Constructions/SampleableType.lean
index 9cf06ab..da31808 100644
--- a/VCVio/OracleComp/Constructions/SampleableType.lean
+++ b/VCVio/OracleComp/Constructions/SampleableType.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.ProbComp
 import VCVio.EvalDist.BitVec
diff --git a/VCVio/OracleComp/EvalDist.lean b/VCVio/OracleComp/EvalDist.lean
index 246d7e4..18839ed 100644
--- a/VCVio/OracleComp/EvalDist.lean
+++ b/VCVio/OracleComp/EvalDist.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.NeverFails
 import VCVio.EvalDist.Instances.OptionT
diff --git a/VCVio/OracleComp/OracleComp.lean b/VCVio/OracleComp/OracleComp.lean
index 625e66f..b264d54 100644
--- a/VCVio/OracleComp/OracleComp.lean
+++ b/VCVio/OracleComp/OracleComp.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.OracleQuery
 import ToMathlib.PFunctor.Free
diff --git a/VCVio/OracleComp/ProbComp.lean b/VCVio/OracleComp/ProbComp.lean
index 517f04b..aff7894 100644
--- a/VCVio/OracleComp/ProbComp.lean
+++ b/VCVio/OracleComp/ProbComp.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.EvalDist
 import Batteries.Control.OptionT
diff --git a/VCVio/OracleComp/QueryTracking/CachingOracle.lean b/VCVio/OracleComp/QueryTracking/CachingOracle.lean
index 97868a7..e1f4e5e 100644
--- a/VCVio/OracleComp/QueryTracking/CachingOracle.lean
+++ b/VCVio/OracleComp/QueryTracking/CachingOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.QueryTracking.Structures
 import VCVio.OracleComp.SimSemantics.Constructions
diff --git a/VCVio/OracleComp/QueryTracking/CountingOracle.lean b/VCVio/OracleComp/QueryTracking/CountingOracle.lean
index 49a3774..a17a8c8 100644
--- a/VCVio/OracleComp/QueryTracking/CountingOracle.lean
+++ b/VCVio/OracleComp/QueryTracking/CountingOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.QueryTracking.Structures
 import VCVio.OracleComp.SimSemantics.WriterT
diff --git a/VCVio/OracleComp/QueryTracking/LoggingOracle.lean b/VCVio/OracleComp/QueryTracking/LoggingOracle.lean
index 6fe8acf..928220e 100644
--- a/VCVio/OracleComp/QueryTracking/LoggingOracle.lean
+++ b/VCVio/OracleComp/QueryTracking/LoggingOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.WriterT
 import VCVio.OracleComp.SimSemantics.Constructions
diff --git a/VCVio/OracleComp/QueryTracking/SeededOracle.lean b/VCVio/OracleComp/QueryTracking/SeededOracle.lean
index c06aa9d..722e432 100644
--- a/VCVio/OracleComp/QueryTracking/SeededOracle.lean
+++ b/VCVio/OracleComp/QueryTracking/SeededOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.Constructions
 import VCVio.OracleComp.QueryTracking.Structures
@@ -431,4 +431,630 @@ lemma probOutput_generateSeed_bind_map_simulateQ
     (probOutput_generateSeed_bind_simulateQ_bind (qc := qc) (js := js)
       (oa := oa) (ob := fun x => pure (f x)) (y := y))
 
+set_option maxHeartbeats 800000 in
+/-- Adding a uniform value at index `i` to a seed does not change the distribution of
+running a computation with the seeded oracle. This is because the extra value replaces
+what would otherwise be a fresh uniform oracle response. -/
+lemma evalDist_liftComp_uniformSample_bind_simulateQ_run'_addValue
+    {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀]
+    [∀ j, SampleableType (spec₀.Range j)] [unifSpec ⊂ₒ spec₀]
+    [OracleSpec.LawfulSubSpec unifSpec spec₀]
+    [spec₀.Fintype] [spec₀.Inhabited]
+    (σ : QuerySeed spec₀) (i : ι₀) {α : Type} (oa : OracleComp spec₀ α) :
+    evalDist (do
+      let u ← liftComp ($ᵗ spec₀.Range i) spec₀
+      (simulateQ seededOracle oa).run' (σ.addValue i u) : OracleComp spec₀ α) =
+    evalDist ((simulateQ seededOracle oa).run' σ : OracleComp spec₀ α) := by
+  revert σ
+  induction oa using OracleComp.inductionOn with
+  | pure x =>
+    intro σ
+    have hrun' : ∀ s, (simulateQ seededOracle (pure x : OracleComp spec₀ α)).run' s =
+        (pure x : OracleComp spec₀ α) := fun s => by
+      show Prod.fst <$> (pure (x, s) : OracleComp spec₀ _) = pure x
+      rw [map_pure]
+    apply evalDist_ext; intro a
+    simp_rw [hrun']
+    rw [probOutput_bind_const]
+    simp [HasEvalPMF.probFailure_eq_zero]
+  | query_bind t mx ih =>
+    intro σ
+    simp only [simulateQ_bind, simulateQ_query, OracleQuery.cont_query,
+      OracleQuery.input_query, id_map]
+    apply evalDist_ext; intro a
+    have hrun' : ∀ s : QuerySeed spec₀,
+        (do let r ← seededOracle t; simulateQ seededOracle (mx r) :
+          StateT _ (OracleComp spec₀) α).run' s =
+        match s.pop t with
+        | none => liftM (query t) >>= fun r => (simulateQ seededOracle (mx r)).run' s
+        | some (r, s') => (simulateQ seededOracle (mx r)).run' s' := by
+      intro s
+      show Prod.fst <$>
+        (seededOracle t >>= fun r => simulateQ seededOracle (mx r)).run s = _
+      rw [run_bind_query_eq_pop]
+      cases s.pop t with
+      | none => simp [map_bind]
+      | some p => rfl
+    simp_rw [hrun']
+    by_cases hti : t = i
+    · cases hti
+      cases hσi : σ i with
+      | nil =>
+        have hadd_pop : ∀ v, (σ.addValue i v).pop i = some (v, σ) := by
+          intro v
+          have hlist : (σ.addValue i v) i = [v] := by
+            simp [QuerySeed.addValue, QuerySeed.addValues, hσi]
+          rw [QuerySeed.pop_eq_some_of_cons _ _ v [] hlist]
+          suffices Function.update (σ.addValue i v) i
+              ([] : List (spec₀.Range i)) = σ by rw [this]
+          funext j; by_cases hj : j = i
+          · subst hj; simp [hσi]
+          · rw [Function.update_of_ne hj]
+            exact QuerySeed.addValues_of_ne σ [v] hj
+        have horig_pop : σ.pop i = none := by
+          rw [QuerySeed.pop_eq_none_iff]; exact hσi
+        simp_rw [hadd_pop, horig_pop]
+        rw [probOutput_bind_eq_tsum, probOutput_bind_eq_tsum]
+        congr 1; ext v; congr 1
+        simp only [probOutput_liftComp, probOutput_uniformSample, probOutput_query]
+      | cons u₀ rest =>
+        have hadd_pop : ∀ v, (σ.addValue i v).pop i =
+            some (u₀, QuerySeed.addValue (Function.update σ i rest) i v) := by
+          intro v
+          have hlist : (σ.addValue i v) i = u₀ :: (rest ++ [v]) := by
+            simp [QuerySeed.addValue, QuerySeed.addValues, hσi]
+          rw [QuerySeed.pop_eq_some_of_cons _ _ u₀ (rest ++ [v]) hlist]
+          suffices Function.update (σ.addValue i v) i (rest ++ [v]) =
+              QuerySeed.addValue (Function.update σ i rest) i v by rw [this]
+          funext j; by_cases hj : j = i
+          · subst hj; simp [QuerySeed.addValue, QuerySeed.addValues]
+          · simp [Function.update_of_ne hj, QuerySeed.addValue,
+              QuerySeed.addValues]
+        have horig_pop : σ.pop i = some (u₀, Function.update σ i rest) :=
+          QuerySeed.pop_eq_some_of_cons σ i u₀ rest hσi
+        simp_rw [hadd_pop, horig_pop]
+        exact congrFun (congrArg DFunLike.coe (ih u₀ (Function.update σ i rest))) a
+    · cases hσt : σ t with
+      | nil =>
+        have hadd_pop : ∀ v, (σ.addValue i v).pop t = none := by
+          intro v; rw [QuerySeed.pop_eq_none_iff]
+          exact (QuerySeed.addValues_of_ne σ [_] hti).trans hσt
+        have horig_pop : σ.pop t = none := by
+          rw [QuerySeed.pop_eq_none_iff]; exact hσt
+        simp_rw [hadd_pop, horig_pop]
+        rw [probOutput_bind_eq_tsum, probOutput_bind_eq_tsum]
+        simp_rw [probOutput_bind_eq_tsum, ← ENNReal.tsum_mul_left, mul_left_comm]
+        rw [ENNReal.tsum_comm]
+        simp_rw [ENNReal.tsum_mul_left]
+        congr 1; ext r; congr 1
+        rw [← probOutput_bind_eq_tsum]
+        exact congrFun (congrArg DFunLike.coe (ih r σ)) a
+      | cons u₀ rest =>
+        have hadd_pop : ∀ v, (σ.addValue i v).pop t =
+            some (u₀, QuerySeed.addValue (Function.update σ t rest) i v) := by
+          intro v
+          have hlist : (σ.addValue i v) t = u₀ :: rest :=
+            (QuerySeed.addValues_of_ne σ [_] hti).trans hσt
+          rw [QuerySeed.pop_eq_some_of_cons _ _ u₀ rest hlist]
+          suffices Function.update (σ.addValue i v) t rest =
+              QuerySeed.addValue (Function.update σ t rest) i v by rw [this]
+          show Function.update (Function.update σ i (σ i ++ [v])) t rest =
+            Function.update (Function.update σ t rest) i
+              ((Function.update σ t rest) i ++ [v])
+          conv_rhs =>
+            rw [show (Function.update σ t rest) i = σ i from
+              Function.update_of_ne (Ne.symm hti) rest σ]
+          exact Function.update_comm (Ne.symm hti) (σ i ++ [v]) rest σ
+        have horig_pop : σ.pop t = some (u₀, Function.update σ t rest) :=
+          QuerySeed.pop_eq_some_of_cons σ t u₀ rest hσt
+        simp_rw [hadd_pop, horig_pop]
+        exact congrFun (congrArg DFunLike.coe
+          (ih u₀ (Function.update σ t rest))) a
+
+lemma evalDist_liftComp_replicate_uniformSample_bind_simulateQ_run'_addValues
+    {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀]
+    [∀ j, SampleableType (spec₀.Range j)] [unifSpec ⊂ₒ spec₀]
+    [OracleSpec.LawfulSubSpec unifSpec spec₀]
+    [spec₀.Fintype] [spec₀.Inhabited]
+    (i : ι₀) {α : Type} (oa : OracleComp spec₀ α) (n : ℕ) :
+    ∀ (σ : QuerySeed spec₀),
+    evalDist (do
+      let us ← liftComp (replicate n ($ᵗ spec₀.Range i)) spec₀
+      (simulateQ seededOracle oa).run' (σ.addValues us) : OracleComp spec₀ α) =
+    evalDist ((simulateQ seededOracle oa).run' σ : OracleComp spec₀ α) := by
+  induction n with
+  | zero => intro σ; simp [replicate_zero, QuerySeed.addValues_nil]
+  | succ n ih =>
+    intro σ
+    simp only [replicate_succ, seq_eq_bind_map, map_eq_bind_pure_comp,
+      liftComp_bind, liftComp_pure, bind_assoc, Function.comp, pure_bind]
+    have hrew : (do
+        let u ← liftComp ($ᵗ spec₀.Range i) spec₀
+        let us ← liftComp (replicate n ($ᵗ spec₀.Range i)) spec₀
+        (simulateQ seededOracle oa).run' (σ.addValues (u :: us))
+          : OracleComp spec₀ α) =
+      (do
+        let u ← liftComp ($ᵗ spec₀.Range i) spec₀
+        let us ← liftComp (replicate n ($ᵗ spec₀.Range i)) spec₀
+        (simulateQ seededOracle oa).run' ((σ.addValues [u]).addValues us)
+          : OracleComp spec₀ α) := by
+      congr 1; ext u; congr 1; ext us
+      rw [QuerySeed.addValues_cons]
+    rw [congrArg evalDist hrew, evalDist_bind]
+    simp_rw [ih]
+    rw [← evalDist_bind]
+    exact evalDist_liftComp_uniformSample_bind_simulateQ_run'_addValue σ i oa
+
+set_option maxHeartbeats 4000000 in
+/-- Truncating the seed at oracle `i₀` to only the first `k` entries does not change
+the distribution when averaging over seeds from `generateSeed`. -/
+lemma evalDist_liftComp_generateSeed_bind_simulateQ_run'_takeAtIndex
+    {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀]
+    [∀ i, SampleableType (spec₀.Range i)] [unifSpec ⊂ₒ spec₀]
+    [OracleSpec.LawfulSubSpec unifSpec spec₀]
+    [spec₀.Fintype] [spec₀.Inhabited]
+    (qc : ι₀ → ℕ) (js : List ι₀) (i₀ : ι₀) (k : ℕ)
+    {α : Type} (oa : OracleComp spec₀ α) :
+    evalDist (do
+      let seed ← liftComp (generateSeed spec₀ qc js) spec₀
+      (simulateQ seededOracle oa).run' (seed.takeAtIndex i₀ k) : OracleComp spec₀ α) =
+    evalDist oa := by
+  classical
+  revert qc js k
+  induction oa using OracleComp.inductionOn with
+  | pure x =>
+    intro qc js k; apply evalDist_ext; intro a; simp
+  | query_bind t mx ih =>
+    intro qc js k
+    simp only [simulateQ_bind, simulateQ_query, OracleQuery.cont_query,
+      OracleQuery.input_query, id_map]
+    apply evalDist_ext; intro x
+    have hrun' : ∀ s : QuerySeed spec₀,
+        (do let u ← seededOracle t; simulateQ seededOracle (mx u) :
+          StateT _ (OracleComp spec₀) α).run' s =
+        match s.pop t with
+        | none => liftM (query t) >>= fun u => (simulateQ seededOracle (mx u)).run' s
+        | some (u, s') => (simulateQ seededOracle (mx u)).run' s' := by
+      intro s
+      show Prod.fst <$>
+        (seededOracle t >>= fun u => simulateQ seededOracle (mx u)).run s = _
+      rw [run_bind_query_eq_pop]
+      cases s.pop t with
+      | none => simp [map_bind]
+      | some p => rfl
+    simp_rw [hrun']
+    rw [probOutput_bind_eq_tsum]
+    simp_rw [probOutput_liftComp]
+    by_cases hpop_none : qc t * js.count t = 0 ∨ (t = i₀ ∧ k = 0)
+    · -- Pop from the take'd seed gives none
+      have hpop : ∀ s ∈ support (generateSeed spec₀ qc js),
+          (s.takeAtIndex i₀ k).pop t = none := by
+        intro s hs; rw [QuerySeed.pop_eq_none_iff]
+        rw [support_generateSeed (spec := spec₀)] at hs
+        rcases hpop_none with hcount | ⟨rfl, rfl⟩
+        · have hlen : (s t).length = qc t * js.count t := hs t
+          have hnil := List.eq_nil_of_length_eq_zero (hlen.trans hcount)
+          by_cases hti : t = i₀
+          · subst hti; simp [QuerySeed.takeAtIndex, hnil]
+          · rw [QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hti]; exact hnil
+        · simp [QuerySeed.takeAtIndex]
+      have step1 : ∀ s,
+          Pr[= s | generateSeed spec₀ qc js] *
+            Pr[= x | match (s.takeAtIndex i₀ k).pop t with
+              | none => liftM (query t) >>= fun u =>
+                  (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)
+              | some (u, s') => (simulateQ seededOracle (mx u)).run' s'] =
+          Pr[= s | generateSeed spec₀ qc js] *
+            Pr[= x | liftM (query t) >>= fun u =>
+                (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)] := by
+        intro s
+        by_cases hs : s ∈ support (generateSeed spec₀ qc js)
+        · simp [hpop s hs]
+        · simp [(probOutput_eq_zero_iff _ _).2 hs]
+      simp_rw [step1, probOutput_bind_eq_tsum (liftM (query t))]
+      simp_rw [← ENNReal.tsum_mul_left, mul_left_comm]
+      rw [ENNReal.tsum_comm]
+      simp_rw [ENNReal.tsum_mul_left]
+      congr 1; ext u; congr 1
+      have hih : Pr[= x | (liftComp (generateSeed spec₀ qc js) spec₀ >>= fun seed =>
+          (simulateQ seededOracle (mx u)).run' (seed.takeAtIndex i₀ k))] = Pr[= x | mx u] :=
+        congrFun (congrArg DFunLike.coe (ih u qc js k)) x
+      rw [show Pr[= x | liftComp (generateSeed spec₀ qc js) spec₀ >>= fun seed =>
+          (simulateQ seededOracle (mx u)).run' (seed.takeAtIndex i₀ k)] =
+        ∑' s, Pr[= s | generateSeed spec₀ qc js] *
+          Pr[= x | (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)] from by
+        rw [probOutput_bind_eq_tsum]; simp_rw [probOutput_liftComp]] at hih
+      exact hih
+    · -- Pop from the take'd seed gives some
+      push_neg at hpop_none
+      obtain ⟨hcount_ne, htk⟩ := hpop_none
+      have hcount : 0 < qc t * js.count t := Nat.pos_of_ne_zero (by omega)
+      -- Original seed always has non-empty list at t
+      have hpop_orig : ∀ s ∈ support (generateSeed spec₀ qc js),
+          ∃ u s', s.pop t = some (u, s') := by
+        intro s hs
+        have hne : s t ≠ [] :=
+          ne_nil_of_mem_support_generateSeed (spec := spec₀) (qc := qc) (js := js) s t hs
+            (Nat.pos_of_ne_zero (by omega))
+        obtain ⟨u, us, hcons⟩ := List.exists_cons_of_ne_nil hne
+        exact ⟨u, Function.update s t us, QuerySeed.pop_eq_some_of_cons s t u us hcons⟩
+      -- Take'd seed also has non-empty list at t
+      have hpop_take : ∀ s ∈ support (generateSeed spec₀ qc js),
+          ∃ u s', (s.takeAtIndex i₀ k).pop t = some (u, s') := by
+        intro s hs
+        have hne : s t ≠ [] :=
+          ne_nil_of_mem_support_generateSeed (spec := spec₀) (qc := qc) (js := js) s t hs
+            (Nat.pos_of_ne_zero (by omega))
+        by_cases hti : t = i₀
+        · have hk : 0 < k := Nat.pos_of_ne_zero (htk hti)
+          have htake_ne : (s.takeAtIndex i₀ k) t ≠ [] := by
+            rw [hti, QuerySeed.takeAtIndex_apply_self]
+            obtain ⟨a, l, hl⟩ := List.exists_cons_of_ne_nil (hti ▸ hne)
+            rw [hl, show k = (k - 1) + 1 from (Nat.succ_pred_eq_of_pos hk).symm,
+              List.take_succ_cons]
+            exact List.cons_ne_nil _ _
+          obtain ⟨u, us, hcons⟩ := List.exists_cons_of_ne_nil htake_ne
+          exact ⟨u, Function.update (s.takeAtIndex i₀ k) t us,
+            QuerySeed.pop_eq_some_of_cons _ _ u us hcons⟩
+        · obtain ⟨u, us, hcons⟩ := List.exists_cons_of_ne_nil hne
+          exact ⟨u, Function.update (s.takeAtIndex i₀ k) t us,
+            QuerySeed.pop_eq_some_of_cons _ _ u us
+              ((QuerySeed.takeAtIndex_apply_of_ne s i₀ k t hti).trans hcons)⟩
+      have step1 : ∀ s,
+          Pr[= s | generateSeed spec₀ qc js] *
+            Pr[= x | match (s.takeAtIndex i₀ k).pop t with
+              | none => liftM (query t) >>= fun u =>
+                  (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)
+              | some (u, s') => (simulateQ seededOracle (mx u)).run' s'] =
+          Pr[= s | generateSeed spec₀ qc js] *
+            (match (s.takeAtIndex i₀ k).pop t with
+              | none => 0
+              | some (u, s') =>
+                  Pr[= x | (simulateQ seededOracle (mx u)).run' s']) := by
+        intro s
+        by_cases hs : s ∈ support (generateSeed spec₀ qc js)
+        · obtain ⟨u, s', hpop⟩ := hpop_take s hs; simp [hpop]
+        · simp [(probOutput_eq_zero_iff _ _).2 hs]
+      simp_rw [step1]
+      -- h_supp uses the ORIGINAL seed's pop for reparametrization
+      have h_supp : Function.support (fun s =>
+          Pr[= s | generateSeed spec₀ qc js] *
+            match (s.takeAtIndex i₀ k).pop t with
+            | none => 0
+            | some (u, s') => Pr[= x | (simulateQ seededOracle (mx u)).run' s']) ⊆
+          Set.range (fun (p : spec₀.Range t × QuerySeed spec₀) =>
+            p.2.prependValues [p.1]) := by
+        intro s hs
+        simp only [Function.mem_support] at hs
+        have hmem : s ∈ support (generateSeed spec₀ qc js) := by
+          by_contra h; exact hs (by simp [(probOutput_eq_zero_iff _ _).2 h])
+        obtain ⟨u, s', hpop⟩ := hpop_orig s hmem
+        exact ⟨(u, s'), QuerySeed.eq_prependValues_of_pop_eq_some hpop⟩
+      rw [← (QuerySeed.prependValues_singleton_injective t).tsum_eq h_supp]
+      -- After reparametrization: seed = s'.prependValues [u₀]
+      -- Use helper lemmas for pop of take'd seed after prependValues
+      by_cases hti : t = i₀
+      · -- t = i₀, k > 0: pop consumes from the take'd prefix, k decreases by 1
+        subst hti
+        have hk : 0 < k := Nat.pos_of_ne_zero (htk rfl)
+        simp only [QuerySeed.pop_takeAtIndex_prependValues_self _ _ _ hk]
+        rw [ENNReal.tsum_prod', probOutput_bind_eq_tsum]
+        congr 1; ext u
+        have hfact := fun s' =>
+          probOutput_generateSeed_prependValues spec₀ qc js u s' hcount
+        simp_rw [hfact, mul_assoc]
+        rw [ENNReal.tsum_mul_left]
+        congr 1
+        · exact (probOutput_query _ u).symm
+        · suffices h : Pr[= x | (do
+              let seed ← liftComp (generateSeed spec₀
+                  (Function.update (fun j => qc j * js.count j) t
+                    (qc t * js.count t - 1))
+                  js.dedup) spec₀
+              (simulateQ seededOracle (mx u)).run'
+                (seed.takeAtIndex t (k - 1)))] = Pr[= x | mx u] by
+            rw [probOutput_bind_eq_tsum] at h
+            simp_rw [probOutput_liftComp] at h
+            exact h
+          exact congrFun (congrArg DFunLike.coe (ih u _ js.dedup (k - 1))) x
+      · -- t ≠ i₀: pop consumes from oracle t, k stays the same
+        simp only [QuerySeed.pop_takeAtIndex_prependValues_of_ne _ _ _ _ hti]
+        rw [ENNReal.tsum_prod', probOutput_bind_eq_tsum]
+        congr 1; ext u
+        have hfact := fun s' =>
+          probOutput_generateSeed_prependValues spec₀ qc js u s' hcount
+        simp_rw [hfact, mul_assoc]
+        rw [ENNReal.tsum_mul_left]
+        congr 1
+        · exact (probOutput_query t u).symm
+        · suffices h : Pr[= x | (do
+              let seed ← liftComp (generateSeed spec₀
+                  (Function.update (fun j => qc j * js.count j) t
+                    (qc t * js.count t - 1))
+                  js.dedup) spec₀
+              (simulateQ seededOracle (mx u)).run'
+                (seed.takeAtIndex i₀ k))] = Pr[= x | mx u] by
+            rw [probOutput_bind_eq_tsum] at h
+            simp_rw [probOutput_liftComp] at h
+            exact h
+          exact congrFun (congrArg DFunLike.coe (ih u _ js.dedup k)) x
+
+@[simp]
+lemma probOutput_generateSeed_bind_map_simulateQ_takeAtIndex
+    {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀]
+    [∀ i, SampleableType (spec₀.Range i)] [unifSpec ⊂ₒ spec₀]
+    [OracleSpec.LawfulSubSpec unifSpec spec₀]
+    [spec₀.Fintype] [spec₀.Inhabited]
+    (qc : ι₀ → ℕ) (js : List ι₀) (i₀ : ι₀) (k : ℕ)
+    {α β : Type} (oa : OracleComp spec₀ α) (f : α → β) (y : β) :
+    Pr[= y | (do
+      let seed ← liftComp (generateSeed spec₀ qc js) spec₀
+      f <$> (simulateQ seededOracle oa).run' (seed.takeAtIndex i₀ k)
+        : OracleComp spec₀ β)] =
+      Pr[= y | f <$> oa] := by
+  have h := evalDist_liftComp_generateSeed_bind_simulateQ_run'_takeAtIndex
+    qc js i₀ k oa
+  have hcomp : (do
+      let seed ← liftComp (generateSeed spec₀ qc js) spec₀
+      f <$> (simulateQ seededOracle oa).run' (seed.takeAtIndex i₀ k)
+        : OracleComp spec₀ β) =
+    f <$> (do
+      let seed ← liftComp (generateSeed spec₀ qc js) spec₀
+      (simulateQ seededOracle oa).run' (seed.takeAtIndex i₀ k)) := by
+    simp only [map_bind]
+  rw [hcomp]
+  exact congrFun (congrArg DFunLike.coe (by simp only [evalDist_map, h])) y
+
+set_option maxHeartbeats 8000000 in
+/-- Weighted takeAtIndex faithfulness: a prefix-dependent weight `h` preserves the
+faithfulness equality between full-seed and truncated-seed simulation.
+This generalizes the basic takeAtIndex faithfulness by allowing multiplication
+by an arbitrary function of the seed prefix `σ.takeAtIndex i₀ k`. -/
+lemma tsum_probOutput_generateSeed_weight_takeAtIndex
+    {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀]
+    [∀ i, SampleableType (spec₀.Range i)] [unifSpec ⊂ₒ spec₀]
+    [OracleSpec.LawfulSubSpec unifSpec spec₀]
+    [spec₀.Fintype] [spec₀.Inhabited]
+    (qc : ι₀ → ℕ) (js : List ι₀) (i₀ : ι₀) (k : ℕ)
+    {α : Type} (oa : OracleComp spec₀ α) (x : α)
+    (h : QuerySeed spec₀ → ENNReal) :
+    ∑' σ, Pr[= σ | generateSeed spec₀ qc js] *
+      (h (σ.takeAtIndex i₀ k) *
+        Pr[= x | (simulateQ seededOracle oa).run' σ]) =
+    ∑' σ, Pr[= σ | generateSeed spec₀ qc js] *
+      (h (σ.takeAtIndex i₀ k) *
+        Pr[= x | (simulateQ seededOracle oa).run' (σ.takeAtIndex i₀ k)]) := by
+  classical
+  revert qc js k h
+  induction oa using OracleComp.inductionOn with
+  | pure a =>
+    intro qc js k h; simp
+  | query_bind t mx ih =>
+    intro qc js k h
+    simp only [simulateQ_bind, simulateQ_query, OracleQuery.cont_query,
+      OracleQuery.input_query, id_map]
+    have hrun' : ∀ s : QuerySeed spec₀,
+        (do let u ← seededOracle t; simulateQ seededOracle (mx u) :
+          StateT _ (OracleComp spec₀) α).run' s =
+        match s.pop t with
+        | none => liftM (query t) >>= fun u => (simulateQ seededOracle (mx u)).run' s
+        | some (u, s') => (simulateQ seededOracle (mx u)).run' s' := by
+      intro s
+      show Prod.fst <$>
+        (seededOracle t >>= fun u => simulateQ seededOracle (mx u)).run s = _
+      rw [run_bind_query_eq_pop]
+      cases s.pop t with
+      | none => simp [map_bind]
+      | some p => rfl
+    simp_rw [hrun']
+    have hcomm : ∀ (g : spec₀.Range t → QuerySeed spec₀ → OracleComp spec₀ α),
+        ∑' s, Pr[= s | generateSeed spec₀ qc js] *
+          (h (s.takeAtIndex i₀ k) *
+            ∑' u, Pr[= u | (liftM (query t) : OracleComp spec₀ _)] *
+              Pr[= x | g u s]) =
+        ∑' u, Pr[= u | (liftM (query t) : OracleComp spec₀ _)] *
+          ∑' s, Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | g u s]) := by
+      intro g
+      simp_rw [ENNReal.tsum_mul_left.symm]
+      rw [ENNReal.tsum_comm]
+      congr 1; ext u; congr 1; ext s; ring
+    by_cases hcount_zero : qc t * js.count t = 0
+    · -- Case 1: no seed entries at oracle t — both pop to none
+      have hpop_full : ∀ s ∈ support (generateSeed spec₀ qc js), s.pop t = none := by
+        intro s hs; rw [QuerySeed.pop_eq_none_iff]
+        rw [support_generateSeed (spec := spec₀)] at hs
+        exact List.eq_nil_of_length_eq_zero ((hs t).trans hcount_zero)
+      have hpop_take : ∀ s ∈ support (generateSeed spec₀ qc js),
+          (s.takeAtIndex i₀ k).pop t = none := by
+        intro s hs; rw [QuerySeed.pop_eq_none_iff]
+        have hnil := List.eq_nil_of_length_eq_zero (((support_generateSeed
+          (spec := spec₀) (qc := qc) (js := js) ▸ hs : _) t).trans hcount_zero)
+        by_cases hti : t = i₀
+        · subst hti; simp [QuerySeed.takeAtIndex, hnil]
+        · rw [QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hti]; exact hnil
+      have step_full : ∀ s,
+          Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | match s.pop t with
+              | none => liftM (query t) >>= fun u =>
+                  (simulateQ seededOracle (mx u)).run' s
+              | some (u, s') => (simulateQ seededOracle (mx u)).run' s']) =
+          Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | liftM (query t) >>= fun u =>
+                (simulateQ seededOracle (mx u)).run' s]) := by
+        intro s
+        by_cases hs : s ∈ support (generateSeed spec₀ qc js)
+        · simp [hpop_full s hs]
+        · simp [(probOutput_eq_zero_iff _ _).2 hs]
+      have step_take : ∀ s,
+          Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | match (s.takeAtIndex i₀ k).pop t with
+              | none => liftM (query t) >>= fun u =>
+                  (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)
+              | some (u, s') => (simulateQ seededOracle (mx u)).run' s']) =
+          Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | liftM (query t) >>= fun u =>
+                (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)]) := by
+        intro s
+        by_cases hs : s ∈ support (generateSeed spec₀ qc js)
+        · simp [hpop_take s hs]
+        · simp [(probOutput_eq_zero_iff _ _).2 hs]
+      simp_rw [step_full, step_take, probOutput_bind_eq_tsum (liftM (query t))]
+      rw [hcomm, hcomm]
+      congr 1; ext u; congr 1
+      exact ih u qc js k h
+    · -- Case 2+3: seed has entries at oracle t
+      push_neg at hcount_zero
+      have hcount : 0 < qc t * js.count t := Nat.pos_of_ne_zero (by omega)
+      have hpop_orig : ∀ s ∈ support (generateSeed spec₀ qc js),
+          ∃ u s', s.pop t = some (u, s') := by
+        intro s hs
+        have hne : s t ≠ [] :=
+          ne_nil_of_mem_support_generateSeed (spec := spec₀) (qc := qc) (js := js) s t hs
+            (Nat.pos_of_ne_zero (by omega))
+        obtain ⟨u, us, hcons⟩ := List.exists_cons_of_ne_nil hne
+        exact ⟨u, Function.update s t us, QuerySeed.pop_eq_some_of_cons s t u us hcons⟩
+      have h_supp_full : Function.support (fun s =>
+          Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | match s.pop t with
+              | none => liftM (query t) >>= fun u =>
+                  (simulateQ seededOracle (mx u)).run' s
+              | some (u, s') => (simulateQ seededOracle (mx u)).run' s'])) ⊆
+          Set.range (fun (p : spec₀.Range t × QuerySeed spec₀) =>
+            p.2.prependValues [p.1]) := by
+        intro s hs
+        simp only [Function.mem_support] at hs
+        have hmem : s ∈ support (generateSeed spec₀ qc js) := by
+          by_contra hc; exact hs (by simp [(probOutput_eq_zero_iff _ _).2 hc])
+        obtain ⟨u, s', hpop⟩ := hpop_orig s hmem
+        exact ⟨(u, s'), QuerySeed.eq_prependValues_of_pop_eq_some hpop⟩
+      have h_supp_take : Function.support (fun s =>
+          Pr[= s | generateSeed spec₀ qc js] *
+            (h (s.takeAtIndex i₀ k) * Pr[= x | match (s.takeAtIndex i₀ k).pop t with
+              | none => liftM (query t) >>= fun u =>
+                  (simulateQ seededOracle (mx u)).run' (s.takeAtIndex i₀ k)
+              | some (u, s') => (simulateQ seededOracle (mx u)).run' s'])) ⊆
+          Set.range (fun (p : spec₀.Range t × QuerySeed spec₀) =>
+            p.2.prependValues [p.1]) := by
+        intro s hs
+        simp only [Function.mem_support] at hs
+        have hmem : s ∈ support (generateSeed spec₀ qc js) := by
+          by_contra hc; exact hs (by simp [(probOutput_eq_zero_iff _ _).2 hc])
+        obtain ⟨u, s', hpop⟩ := hpop_orig s hmem
+        exact ⟨(u, s'), QuerySeed.eq_prependValues_of_pop_eq_some hpop⟩
+      rw [← (QuerySeed.prependValues_singleton_injective t).tsum_eq h_supp_full,
+        ← (QuerySeed.prependValues_singleton_injective t).tsum_eq h_supp_take]
+      simp only [QuerySeed.pop_prependValues_singleton]
+      by_cases hti : t = i₀
+      · subst hti
+        by_cases hk : k = 0
+        · -- Case 3: t = i₀, k = 0 — LHS pop some, RHS pop none
+          subst hk
+          have htake_zero : ∀ (u₀ : spec₀.Range t) (s' : QuerySeed spec₀),
+              (QuerySeed.prependValues s' [u₀]).takeAtIndex t 0 =
+              QuerySeed.takeAtIndex s' t 0 := by
+            intro u₀ s'; funext j; by_cases hj : j = t
+            · subst hj; simp [QuerySeed.takeAtIndex_apply_self]
+            · simp [QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hj,
+                QuerySeed.prependValues_of_ne _ _ hj]
+          have hpop_rhs : ∀ (s' : QuerySeed spec₀),
+              (QuerySeed.takeAtIndex s' t 0).pop t = none := by
+            intro s'; rw [QuerySeed.pop_eq_none_iff]
+            simp [QuerySeed.takeAtIndex]
+          simp_rw [htake_zero, hpop_rhs]
+          rw [ENNReal.tsum_prod']; conv_rhs => rw [ENNReal.tsum_prod']
+          simp_rw [probOutput_generateSeed_prependValues spec₀ qc js _ _ hcount,
+            mul_assoc]
+          conv_lhs =>
+            arg 1
+            intro u₀
+            rw [ENNReal.tsum_mul_left]
+          conv_rhs =>
+            arg 1
+            intro u₀
+            rw [ENNReal.tsum_mul_left]
+          rw [ENNReal.tsum_mul_left]; conv_rhs => rw [ENNReal.tsum_mul_left]
+          congr 1
+          conv_lhs =>
+            arg 1
+            intro u₀
+            rw [ih u₀ _ js.dedup 0 h]
+          rw [ENNReal.tsum_comm]; conv_rhs => rw [ENNReal.tsum_comm]
+          congr 1; ext s'
+          rw [ENNReal.tsum_mul_left]; conv_rhs => rw [ENNReal.tsum_mul_left]
+          congr 1
+          rw [ENNReal.tsum_mul_left]; conv_rhs => rw [ENNReal.tsum_mul_left]
+          congr 1
+          conv_rhs => rw [probOutput_bind_eq_tsum (liftM (query t) : OracleComp spec₀ _)]
+          conv_rhs => simp [probOutput_query]
+          conv_rhs => rw [← Finset.mul_sum]
+          have hcard_ne_zero : (↑(Fintype.card (spec₀.Range t)) : ENNReal) ≠ 0 := by
+            exact_mod_cast Fintype.card_pos.ne'
+          have hcard_ne_top : (↑(Fintype.card (spec₀.Range t)) : ENNReal) ≠ ⊤ := by
+            exact ENNReal.natCast_ne_top (n := Fintype.card (spec₀.Range t))
+          rw [← mul_assoc, ENNReal.mul_inv_cancel hcard_ne_zero hcard_ne_top, one_mul]
+          have hrun'_eq : ∀ i : spec₀.Range t,
+              (simulateQ seededOracle (mx i)).run' (s'.takeAtIndex t 0) =
+                (fun x ↦ x.1) <$> (simulateQ seededOracle (mx i)).run (s'.takeAtIndex t 0) := by
+            intro i; rfl
+          simp_rw [hrun'_eq]
+          exact (tsum_fintype (L := .unconditional _)
+            (f := fun i : spec₀.Range t =>
+              Pr[= x | (fun x ↦ x.1) <$> (simulateQ seededOracle (mx i)).run
+                (s'.takeAtIndex t 0)]))
+        · -- Case 2a: t = i₀, k > 0 — both pop some, k decreases
+          have hk_pos : 0 < k := Nat.pos_of_ne_zero hk
+          simp only [QuerySeed.pop_takeAtIndex_prependValues_self _ _ _ hk_pos]
+          rw [ENNReal.tsum_prod']
+          conv_rhs => rw [ENNReal.tsum_prod']
+          congr 1; ext u₀
+          have htake_prepend : ∀ (s' : QuerySeed spec₀),
+              (QuerySeed.prependValues s' [u₀]).takeAtIndex t k =
+              QuerySeed.prependValues (QuerySeed.takeAtIndex s' t (k - 1)) [u₀] := by
+            intro s'; funext j; by_cases hj : j = t
+            · subst hj
+              simp only [QuerySeed.takeAtIndex_apply_self,
+                QuerySeed.prependValues_singleton]
+              conv_lhs =>
+                rw [show k = (k - 1) + 1 from (Nat.succ_pred_eq_of_pos hk_pos).symm]
+              rw [List.take_succ_cons]
+            · simp [QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hj,
+                QuerySeed.prependValues_of_ne _ _ hj]
+          simp_rw [htake_prepend]
+          have hfact := fun (s' : QuerySeed spec₀) =>
+            probOutput_generateSeed_prependValues spec₀ qc js u₀ s' hcount
+          simp_rw [hfact, mul_assoc]
+          rw [ENNReal.tsum_mul_left]
+          conv_rhs => rw [ENNReal.tsum_mul_left]
+          congr 1
+          exact ih u₀ _ js.dedup (k - 1)
+            (fun σ => h (QuerySeed.prependValues σ [u₀]))
+      · -- Case 2b: t ≠ i₀ — both pop some, k unchanged
+        simp only [QuerySeed.pop_takeAtIndex_prependValues_of_ne _ _ _ _ hti]
+        rw [ENNReal.tsum_prod']
+        conv_rhs => rw [ENNReal.tsum_prod']
+        congr 1; ext u₀
+        have htake_prepend : ∀ (s' : QuerySeed spec₀),
+            (QuerySeed.prependValues s' [u₀]).takeAtIndex i₀ k =
+            QuerySeed.prependValues (QuerySeed.takeAtIndex s' i₀ k) [u₀] := by
+          intro s'; funext j; by_cases hji : j = i₀
+          · subst hji
+            simp [QuerySeed.takeAtIndex_apply_self,
+              QuerySeed.prependValues_of_ne _ _ (Ne.symm hti)]
+          · rw [QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hji]
+            by_cases hjt : j = t
+            · subst hjt
+              simp [QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hti]
+            · simp [QuerySeed.prependValues_of_ne _ _ hjt,
+                QuerySeed.takeAtIndex_apply_of_ne _ _ _ _ hji]
+        simp_rw [htake_prepend]
+        have hfact := fun (s' : QuerySeed spec₀) =>
+          probOutput_generateSeed_prependValues spec₀ qc js u₀ s' hcount
+        simp_rw [hfact, mul_assoc]
+        rw [ENNReal.tsum_mul_left]
+        conv_rhs => rw [ENNReal.tsum_mul_left]
+        congr 1
+        exact ih u₀ _ js.dedup k
+          (fun σ => h (QuerySeed.prependValues σ [u₀]))
+
 end seededOracle
diff --git a/VCVio/OracleComp/QueryTracking/Structures.lean b/VCVio/OracleComp/QueryTracking/Structures.lean
index ddd576b..0005745 100644
--- a/VCVio/OracleComp/QueryTracking/Structures.lean
+++ b/VCVio/OracleComp/QueryTracking/Structures.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.SimulateQ
 import ToMathlib.Control.WriterT
@@ -407,6 +407,13 @@ lemma addValues_nil (seed : QuerySeed spec) (i : ι) :
     seed.addValues (i := i) ([] : List (spec.Range i)) = seed := by
   simp [addValues]
 
+lemma addValues_cons (seed : QuerySeed spec) {i : ι} (u : spec.Range i)
+    (us : List (spec.Range i)) :
+    seed.addValues (u :: us) = (seed.addValues [u]).addValues us := by
+  ext j; by_cases hj : j = i
+  · subst hj; simp [addValues]
+  · simp [addValues, Function.update_of_ne hj]
+
 /-- Prepend a list of values to the seed at index `i`. -/
 def prependValues (seed : QuerySeed spec) {i : ι} (us : List (spec.Range i)) : QuerySeed spec :=
   Function.update seed i (us ++ seed i)
@@ -496,6 +503,12 @@ def takeAtIndex (seed : QuerySeed spec) (i : ι) (n : ℕ) : QuerySeed spec :=
     · subst hj; simp [takeAtIndex]
     · simp [takeAtIndex, Function.update_of_ne hj]
 
+lemma takeAtIndex_addValues_drop (seed : QuerySeed spec) (i : ι) (n : ℕ) :
+    (seed.takeAtIndex i n).addValues ((seed i).drop n) = seed := by
+  ext j; by_cases hj : j = i
+  · subst hj; simp [takeAtIndex, addValues, List.take_append_drop]
+  · simp [takeAtIndex, addValues, Function.update_of_ne hj]
+
 /-- Pop one value from index `i`, returning the consumed value and updated seed when nonempty. -/
 def pop (seed : QuerySeed spec) (i : ι) : Option (spec.Range i × QuerySeed spec) :=
   match seed i with
@@ -601,6 +614,45 @@ lemma eq_prependValues_of_pop_eq_some {seed : QuerySeed spec} {i : ι}
     simpa [Function.update_self] using hcons
   · simp only [prependValues_of_ne _ _ hj, Function.update_of_ne hj]
 
+lemma pop_takeAtIndex_prependValues_of_ne (s' : QuerySeed spec) (i₀ : ι) (k : ℕ)
+    {t : ι} (u₀ : spec.Range t) (hti : t ≠ i₀) :
+    ((s'.prependValues [u₀]).takeAtIndex i₀ k).pop t =
+      some (u₀, s'.takeAtIndex i₀ k) := by
+  have h1 : ((s'.prependValues [u₀]).takeAtIndex i₀ k) t = u₀ :: s' t := by
+    rw [takeAtIndex_apply_of_ne _ _ _ _ hti, prependValues_singleton]
+  rw [pop_eq_some_of_cons _ _ u₀ (s' t) h1]
+  congr 1
+  suffices Function.update ((s'.prependValues [u₀]).takeAtIndex i₀ k) t (s' t) =
+      s'.takeAtIndex i₀ k from Prod.ext rfl this
+  funext j
+  by_cases hj : j = t
+  · subst hj; simp [Function.update_self, takeAtIndex_apply_of_ne _ _ _ _ hti]
+  · rw [Function.update_of_ne hj]
+    by_cases hji : j = i₀
+    · subst hji
+      simp [takeAtIndex_apply_self, prependValues_of_ne _ _ (Ne.symm hti)]
+    · simp [takeAtIndex_apply_of_ne _ _ _ _ hji, prependValues_of_ne _ _ hj]
+
+lemma pop_takeAtIndex_prependValues_self (s' : QuerySeed spec) (i₀ : ι)
+    (u₀ : spec.Range i₀) {k : ℕ} (hk : 0 < k) :
+    ((s'.prependValues [u₀]).takeAtIndex i₀ k).pop i₀ =
+      some (u₀, s'.takeAtIndex i₀ (k - 1)) := by
+  have h1 : ((s'.prependValues [u₀]).takeAtIndex i₀ k) i₀ =
+      u₀ :: (s' i₀).take (k - 1) := by
+    simp only [takeAtIndex_apply_self, prependValues_singleton]
+    obtain ⟨k', rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp hk)
+    simp [List.take_succ_cons]
+  rw [pop_eq_some_of_cons _ _ u₀ ((s' i₀).take (k - 1)) h1]
+  congr 1
+  suffices Function.update ((s'.prependValues [u₀]).takeAtIndex i₀ k) i₀
+      ((s' i₀).take (k - 1)) = s'.takeAtIndex i₀ (k - 1) by
+    exact Prod.ext rfl this
+  funext j
+  by_cases hj : j = i₀
+  · subst hj; simp [Function.update_self, takeAtIndex_apply_self]
+  · rw [Function.update_of_ne hj, takeAtIndex_apply_of_ne _ _ _ _ hj,
+      takeAtIndex_apply_of_ne _ _ _ _ hj, prependValues_of_ne _ _ hj]
+
 end QuerySeed
 
 end OracleSpec
diff --git a/VCVio/OracleComp/SimSemantics/Constructions.lean b/VCVio/OracleComp/SimSemantics/Constructions.lean
index a62c74a..64bb85a 100644
--- a/VCVio/OracleComp/SimSemantics/Constructions.lean
+++ b/VCVio/OracleComp/SimSemantics/Constructions.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.SimulateQ
 import VCVio.OracleComp.Constructions.SampleableType
diff --git a/VCVio/OracleComp/SimSemantics/SimulateQ.lean b/VCVio/OracleComp/SimSemantics/SimulateQ.lean
index 8ec7690..cace569 100644
--- a/VCVio/OracleComp/SimSemantics/SimulateQ.lean
+++ b/VCVio/OracleComp/SimSemantics/SimulateQ.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.QueryImpl
 import ToMathlib.Control.OptionT