diff --git a/Complexity/Computability/Complexity/Classes/WPP/Robustness.lean b/Complexity/Computability/Complexity/Classes/WPP/Robustness.lean
index 4014ba63d..5be6f61c8 100644
--- a/Complexity/Computability/Complexity/Classes/WPP/Robustness.lean
+++ b/Complexity/Computability/Complexity/Classes/WPP/Robustness.lean
@@ -32,8 +32,8 @@ Thus the proof uses certified word sums and powers, without assuming indexed-pro
 The two-sided acceptance/rejection-target generalization is proved in `WPP.TwoSided`.
 Oracle lowness is a separate result.
 
-The public polynomial-time interfaces use `Turing.MultiTapeTM.ComputableInPolyTime`, following
-the plain-statement convention of #456. Private machine-construction lemmas remain tidy.
+The public polynomial-time interfaces use `Turing.MultiTapeTM.ComputableInPolyTime`. Private
+machine-construction lemmas remain tidy.
 
 ## Main results
 
diff --git a/Complexity/Computability/Complexity/Classes/WPP/TwoSided.lean b/Complexity/Computability/Complexity/Classes/WPP/TwoSided.lean
index a67f8981b..9721339ba 100644
--- a/Complexity/Computability/Complexity/Classes/WPP/TwoSided.lean
+++ b/Complexity/Computability/Complexity/Classes/WPP/TwoSided.lean
@@ -23,8 +23,7 @@ of the differences between rejection targets and the original gap. This vanishes
 and on acceptance takes one of a uniformly computed family of nonzero products. The uniform
 product theorem and one-sided robustness then finish the construction.
 
-The public interfaces ask for `Turing.MultiTapeTM.ComputableInPolyTime` certificates, following
-the plain-statement convention of #456.
+The public interfaces ask for `Turing.MultiTapeTM.ComputableInPolyTime` certificates.
 
 ## Main results
 
diff --git a/Complexity/Computability/GenericRAM/Native/MeasurementFold.lean b/Complexity/Computability/GenericRAM/Native/MeasurementFold.lean
index 97d61672e..b29390643 100644
--- a/Complexity/Computability/GenericRAM/Native/MeasurementFold.lean
+++ b/Complexity/Computability/GenericRAM/Native/MeasurementFold.lean
@@ -30,7 +30,7 @@ loop. The generic callback may grow its accumulator: polynomial whole-loop works
 actual all-prefix accumulator invariant, not just a polynomial per-visit certificate.
 
 This is the measurement-VALUE enumeration of [OpenAI2026ETH], Lemma 3.2 and Proposition 3.4
-(pp. 22–26), runtime M0.4 of #1226. It is not formal mode-exponent enumeration, subset-pair
+(pp. 22–26). It is not formal mode-exponent enumeration, subset-pair
 traversal, rational coefficient accumulation or a complete runtime/ETH result.
 -/
 
diff --git a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
index 6ca658743..796e00a93 100644
--- a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
+++ b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
@@ -617,7 +617,7 @@ theorem exists_fin_selectBestTestRow (countSys : List (List Bool) → ℕ)
   obtain ⟨γ, hγ⟩ := exists_fin_of_lt_candidateTupleCount hjStar
   exact ⟨γ, by rw [hrow, hγ, materializeTestRow_ofFn]⟩
 
-/-! ### Row counts, widths, weights, and CNF `#1234` bridge for `greedyParityRows` -/
+/-! ### Row counts, widths, weights, and CNF bridge for `greedyParityRows` -/
 
 @[simp] theorem length_greedyParityRowsAt (countSys : List (List Bool) → ℕ)
     (m P : ℕ) (initRows : List (List Bool)) (i : ℕ) :
@@ -688,7 +688,8 @@ theorem length_encList_greedyParityRowsAt (countSys : List (List Bool) → ℕ)
     rw [greedyParityRowsAt_succ, encList_append, List.length_append, ih, encList_cons, encList_nil,
       List.append_nil, length_frame, encBits_apply, length_selectBestTestRow]; ring
 
-/-- **Exact bridge from `greedyParityRows` to `CNF.numPassing_greedy` (`#1234`, Lemma 6.2).**
+/-- **Exact bridge from `greedyParityRows` to `CNF.numPassing_greedy`**
+([OpenAI2026ETH], Lemma 6.2).
 Under `hn : 1 ≤ Fintype.card V` and `hP : 1 ≤ P`, when `initRows` has row width `φ.length`,
 `countSys` computes `numPassing φ.violations` on width-`φ.length` candidate row lists of length at
 most `initRows.length + 3 * Fintype.card V` whose appended rows have weight `≤ P`, and `initRows`
diff --git a/Complexity/Probability/HashFamily/Uniform.lean b/Complexity/Probability/HashFamily/Uniform.lean
index cc2fe576a..43d41e465 100644
--- a/Complexity/Probability/HashFamily/Uniform.lean
+++ b/Complexity/Probability/HashFamily/Uniform.lean
@@ -19,10 +19,6 @@ A uniformly random function into a finite additive group has uniform differences
 inputs. Negating the complete function preserves its uniform law, and hence the same bound.
 These are information-theoretic laws; they make no efficient-sampling claim.
 
-The uniform-function proof is moved from `Complexity.Crypto.Protocols.Cipher.LubyRackoff`.
-The negated-function proof is extracted from the reviewed #1099 contribution by
-`worker-jetski-fb3f7966`; the proof bodies and their assumptions are retained.
-
 ## Main results
 
 * `Cslib.Probability.isDeltaUniversalHash_uniformOfFintype`: uniform functions are Δ-universal.
diff --git a/ComplexityTests/Crypto/AuthenticatedEncryption.lean b/ComplexityTests/Crypto/AuthenticatedEncryption.lean
index f23cdacbb..01e592a59 100644
--- a/ComplexityTests/Crypto/AuthenticatedEncryption.lean
+++ b/ComplexityTests/Crypto/AuthenticatedEncryption.lean
@@ -12,8 +12,8 @@ import Complexity.Crypto.Computational.Encryption.Authenticated
 Provides concrete instantiations of `SymmetricCipher`, verifies oracle behavior on concrete inputs,
 proves that `echoCipher` fails both `INDCPA` (via `not_indcpa_of_ciphertext_length_eq`,
 Boneh–Shoup Example 5.1 / Exercise 5.10(a)) and `CiphertextIntegrity` (via an explicit zero-query
-oracle-PPT adversary), and exercises the runtime certificates (`IsPPT`, `IsOraclePPT`) and
-quantitative/asymptotic security theorems for Boneh–Shoup Theorem 9.1 (`AE ⇒ CCA`).
+oracle-PPT adversary), and exercises the composed runtime certificates (`IsPPT`, `IsOraclePPT`) and
+quantitative security bounds for Boneh–Shoup Theorem 9.1 (`AE ⇒ CCA`) on `echoCipher`.
 -/
 
 namespace ComplexityTests.Crypto.AuthenticatedEncryption
@@ -104,82 +104,111 @@ theorem not_authenticatedEncryption_echoCipher :
     ¬ echoCipher.AuthenticatedEncryption :=
   fun hae => not_ciphertextIntegrity_echoCipher hae.2
 
-/-! ### API and Certificate Smoke Checks -/
+/-! ### Concrete Reduction Certificates and Quantitative Bounds on `echoCipher` -/
 
-section CertificatesAndReductions
+/-- Zero-query CCA adversary that always outputs `false`. -/
+def zeroCCAAdversary : CCAAdversary :=
+  fun _ _ => ProbOracleComp.sample (pure false)
 
-variable (E : SymmetricCipher)
-  {ctBound Q : ℕ → ℕ}
-  (hctBound : ComputableInPolyTime ctBound encUnary encUnary)
-  (hQ : ComputableInPolyTime Q encUnary encUnary)
-  {cpaAdv : OracleDistinguisher} (hcpaAdv : IsOraclePPT encBool cpaAdv)
-  {ciAdv : CIAdversary} (hciAdv : IsOraclePPT encBits ciAdv)
-  {ccaAdv : CCAAdversary} (hccaAdv : IsOraclePPT encBool ccaAdv)
+theorem isOraclePPT_zeroCCAAdversary : IsOraclePPT encBool zeroCCAAdversary := by
+  have hbody : IsPPTOn (encPair encUnary encBits) encBool
+      (fun _ : ℕ × List Bool => (pure false : ProbComp Bool)) :=
+    (ComputableTidilyInPolyTime.const false).isPPTOn
+  exact hbody.isOraclePPTOn.isOraclePPT
 
--- Closed game `IsPPT` certificates.
-example (bit : Bool) : IsPPT encBool (fun n _ => E.cpaGame cpaAdv bit n) :=
-  E.isPPT_cpaGame hcpaAdv bit
-
-example : IsPPT encBool (fun n _ => E.ciGame ciAdv n) :=
-  E.isPPT_ciGame hciAdv
-
-example (bit : Bool) : IsPPT encBool (fun n _ => E.ccaGame ccaAdv bit n) :=
-  E.isPPT_ccaGame hccaAdv bit
-
--- Theorem 9.1 reduction `IsOraclePPT` certificates.
-example : IsOraclePPT encBool (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) :=
-  SymmetricCipher.isOraclePPT_ccaToCPAAdversary hctBound hccaAdv
+theorem isQueryBounded_zeroCCAAdversary (n : ℕ) :
+    (zeroCCAAdversary n []).IsQueryBounded 0 :=
+  ProbOracleComp.IsQueryBounded.sample (pure false)
 
+-- Composed closed-game `IsPPT` and Theorem 9.1 reduction `IsOraclePPT` certificates on
+-- `echoCipher` with `ctBound = id` and `Q = 0`.
 example (bit : Bool) :
-    IsOraclePPT encBits (SymmetricCipher.ccaToCIAdversary ctBound Q bit ccaAdv) :=
-  SymmetricCipher.isOraclePPT_ccaToCIAdversary hctBound hQ bit hccaAdv
+    IsPPT encBool
+      (fun n _ =>
+        echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) bit n) :=
+  echoCipher.isPPT_cpaGame
+    (SymmetricCipher.isOraclePPT_ccaToCPAAdversary ComputableInPolyTime.id'
+      isOraclePPT_zeroCCAAdversary)
+    bit
 
-example : IsOraclePPT encBits (SymmetricCipher.ccaToCIHiddenBitAdversary ctBound Q ccaAdv) :=
-  SymmetricCipher.isOraclePPT_ccaToCIHiddenBitAdversary hctBound hQ hccaAdv
+example (bit : Bool) :
+    IsPPT encBool
+      (fun n _ =>
+        echoCipher.ciGame
+          (SymmetricCipher.ccaToCIAdversary id (fun _ => 0) bit zeroCCAAdversary) n) :=
+  echoCipher.isPPT_ciGame
+    (SymmetricCipher.isOraclePPT_ccaToCIAdversary ComputableInPolyTime.id'
+      (ComputableInPolyTime.const 0) bit isOraclePPT_zeroCCAAdversary)
 
--- Quantitative security bounds (Theorem 9.1).
-example (n : ℕ)
-    (hq : (ccaAdv n []).IsQueryBounded (Q n))
-    (hctBoundN : ∀ k ∈ (ProbComp.eval (E.keyGen n)).support,
-      ∀ msg, msg.length = n →
-      ∀ ct ∈ (ProbComp.eval (E.encrypt n k msg)).support, ct.length ≤ ctBound n) :
-    (Game.advantage (ProbComp.eval (E.ccaGame ccaAdv false n))
-        (ProbComp.eval (E.ccaGame ccaAdv true n)) : ℝ) ≤
-      (dyadicSize (Q n) : ℝ) *
+example :
+    IsPPT encBool
+      (fun n _ =>
+        echoCipher.ciGame
+          (SymmetricCipher.ccaToCIHiddenBitAdversary id (fun _ => 0) zeroCCAAdversary) n) :=
+  echoCipher.isPPT_ciGame
+    (SymmetricCipher.isOraclePPT_ccaToCIHiddenBitAdversary ComputableInPolyTime.id'
+      (ComputableInPolyTime.const 0) isOraclePPT_zeroCCAAdversary)
+
+-- Quantitative Theorem 9.1 bounds instantiated on `echoCipher` and `zeroCCAAdversary`, with
+-- `dyadicSize 0 = 2` evaluated and `echoCipher_ctLen` discharging the ciphertext-length premise.
+example (n : ℕ) :
+    (Game.advantage (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary false n))
+        (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary true n)) : ℝ) ≤
+      2 *
         (Game.succProbability
-          (ProbComp.eval (E.ciGame (SymmetricCipher.ccaToCIAdversary ctBound Q false ccaAdv) n)) :
+          (ProbComp.eval
+            (echoCipher.ciGame
+              (SymmetricCipher.ccaToCIAdversary id (fun _ => 0) false zeroCCAAdversary) n)) :
             ℝ) +
       (Game.advantage
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) false n))
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) true n)) :
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) false n))
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) true n)) :
           ℝ) +
-      (dyadicSize (Q n) : ℝ) *
+      2 *
         (Game.succProbability
-          (ProbComp.eval (E.ciGame (SymmetricCipher.ccaToCIAdversary ctBound Q true ccaAdv) n)) :
-            ℝ) :=
-  E.advantage_ccaGame_le ctBound Q ccaAdv n hq hctBoundN
-
-example (n : ℕ)
-    (hq : (ccaAdv n []).IsQueryBounded (Q n))
-    (hctBoundN : ∀ k ∈ (ProbComp.eval (E.keyGen n)).support,
-      ∀ msg, msg.length = n →
-      ∀ ct ∈ (ProbComp.eval (E.encrypt n k msg)).support, ct.length ≤ ctBound n) :
-    (Game.advantage (ProbComp.eval (E.ccaGame ccaAdv false n))
-        (ProbComp.eval (E.ccaGame ccaAdv true n)) : ℝ) ≤
-      2 * (dyadicSize (Q n) : ℝ) *
+          (ProbComp.eval
+            (echoCipher.ciGame
+              (SymmetricCipher.ccaToCIAdversary id (fun _ => 0) true zeroCCAAdversary) n)) :
+            ℝ) := by
+  have hct (k : List Bool) (hk : k ∈ (ProbComp.eval (echoCipher.keyGen n)).support)
+      (msg : List Bool) (hmsg : msg.length = n)
+      (ct : List Bool) (hct : ct ∈ (ProbComp.eval (echoCipher.encrypt n k msg)).support) :
+      ct.length ≤ id n :=
+    (echoCipher_ctLen n k hk msg hmsg ct hct).le
+  have h0 : dyadicSize 0 = 2 := by decide
+  have hd : (dyadicSize 0 : ℝ) = 2 := by exact_mod_cast h0
+  simpa [hd] using
+    echoCipher.advantage_ccaGame_le id (fun _ => 0) zeroCCAAdversary n
+      (isQueryBounded_zeroCCAAdversary n) hct
+
+example (n : ℕ) :
+    (Game.advantage (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary false n))
+        (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary true n)) : ℝ) ≤
+      4 *
         (Game.succProbability
           (ProbComp.eval
-            (E.ciGame (SymmetricCipher.ccaToCIHiddenBitAdversary ctBound Q ccaAdv) n)) : ℝ) +
+            (echoCipher.ciGame
+              (SymmetricCipher.ccaToCIHiddenBitAdversary id (fun _ => 0) zeroCCAAdversary) n)) :
+            ℝ) +
       (Game.advantage
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) false n))
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) true n)) :
-          ℝ) :=
-  E.advantage_ccaGame_le_two_mul ctBound Q ccaAdv n hq hctBoundN
-
--- End-to-end asymptotic composition (Theorem 9.1).
-example (hae : E.AuthenticatedEncryption) : E.INDCCA :=
-  hae.indcca
-
-end CertificatesAndReductions
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) false n))
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) true n)) :
+          ℝ) := by
+  have hct (k : List Bool) (hk : k ∈ (ProbComp.eval (echoCipher.keyGen n)).support)
+      (msg : List Bool) (hmsg : msg.length = n)
+      (ct : List Bool) (hct : ct ∈ (ProbComp.eval (echoCipher.encrypt n k msg)).support) :
+      ct.length ≤ id n :=
+    (echoCipher_ctLen n k hk msg hmsg ct hct).le
+  have hd : 2 * (dyadicSize 0 : ℝ) = 4 := by
+    have h0 : dyadicSize 0 = 2 := by decide
+    rw [h0]
+    norm_num
+  simpa [hd] using
+    echoCipher.advantage_ccaGame_le_two_mul id (fun _ => 0) zeroCCAAdversary n
+      (isQueryBounded_zeroCCAAdversary n) hct
 
 end ComplexityTests.Crypto.AuthenticatedEncryption
diff --git a/ComplexityTests/Crypto/EncryptThenMAC.lean b/ComplexityTests/Crypto/EncryptThenMAC.lean
index 784d92c24..16fa49741 100644
--- a/ComplexityTests/Crypto/EncryptThenMAC.lean
+++ b/ComplexityTests/Crypto/EncryptThenMAC.lean
@@ -12,8 +12,9 @@ import Complexity.Probability.BitString
 
 Provides concrete instantiations of `prfCipher`, `encryptThenMAC`, and `prfEncryptThenMAC`,
 verifies decryption completeness and tamper rejection on concrete inputs, and exercises the
-runtime certificates (`IsOraclePPT`), quantitative bounds, and asymptotic security theorems for
-Boneh–Shoup Theorem 5.2 (`PRF ⇒ INDCPA` for `prfCipher`) and Theorem 9.2 (`Encrypt-then-MAC`).
+composed runtime certificates (`IsPPT`, `IsOraclePPT`) and quantitative security bounds for
+Boneh–Shoup Theorem 5.2 (`PRF ⇒ INDCPA` for `prfCipher`) and Theorem 9.2 (`Encrypt-then-MAC`) on
+`echoPrfCipher`, `echoPrfMAC`, and `echoPrfEtM`.
 -/
 
 namespace ComplexityTests.Crypto.EncryptThenMAC
@@ -93,115 +94,134 @@ example :
     none := by
   rfl
 
-/-! ### API, Certificate, and Non-Vacuity Smoke Checks -/
-
-section CertificatesAndReductions
-
-variable (E : SymmetricCipher) (M : MACScheme)
-  (hctLen : ∀ n ke, ke ∈ (ProbComp.eval (E.keyGen n)).support →
-    ∀ msg, msg.length = n →
-    ∀ c ∈ (ProbComp.eval (E.encrypt n ke msg)).support, c.length = M.msgLen n)
-  {tagBound : ℕ → ℕ} (htagBound : ComputableInPolyTime tagBound encUnary encUnary)
-  {cpaAdv : OracleDistinguisher} (hcpaAdv : IsOraclePPT encBool cpaAdv)
-  {ciAdv : CIAdversary} (hciAdv : IsOraclePPT encBits ciAdv)
-  (family : List Bool → List Bool → List Bool)
-  (hpoly : ComputableInPolyTime (fun p : List Bool × List Bool => family p.1 p.2)
-    (encPair encBits encBits) encBits)
-  (hlen : ∀ key query, query.length = key.length → (family key query).length = key.length)
-  (hprf : PseudorandomFunction family)
-
--- Theorem 9.2 and Theorem 5.2 reduction `IsOraclePPT` certificates.
-example : IsOraclePPT (encPair encBits encBits) (etmToMACForger E M tagBound ciAdv) :=
-  isOraclePPT_etmToMACForger E M htagBound hciAdv
-
-example : IsOraclePPT encBool (etmToCPAAdversary M cpaAdv) :=
-  isOraclePPT_etmToCPAAdversary M hcpaAdv
-
-example (bit : Bool) : IsOraclePPT encBool (cpaToPrfDistinguisher cpaAdv bit) :=
-  isOraclePPT_cpaToPrfDistinguisher hcpaAdv bit
-
--- Quantitative security equations and bounds (Theorem 9.2 and Theorem 5.2).
-example (n : ℕ)
-    (htagBoundN : ∀ km ∈ (ProbComp.eval (M.keyGen n)).support,
-      ∀ c, c.length = M.msgLen n →
-      ∀ tag ∈ (ProbComp.eval (M.sign km c)).support, tag.length ≤ tagBound n) :
-    Game.succProbability (ProbComp.eval ((encryptThenMAC E M hctLen).ciGame ciAdv n)) =
+/-! ### Concrete Reduction Certificates and Quantitative Bounds on `echoPrfCipher` and `echoPrfEtM`
+-/
+
+/-- Concrete reindexed `prfMAC` on `echoFamily` authenticating `2 * n`-bit ciphertexts. -/
+noncomputable def echoPrfMAC : MACScheme :=
+  (prfMAC echoFamily echoFamily_polyTime).reindex (fun n => 2 * n) (by polytime)
+
+/-- Zero-query CPA distinguisher that always outputs `false`. -/
+def zeroCPAAdversary : OracleDistinguisher :=
+  fun _ _ => ProbOracleComp.sample (pure false)
+
+theorem isOraclePPT_zeroCPAAdversary : IsOraclePPT encBool zeroCPAAdversary := by
+  have hbody : IsPPTOn (encPair encUnary encBits) encBool
+      (fun _ : ℕ × List Bool => (pure false : ProbComp Bool)) :=
+    (ComputableTidilyInPolyTime.const false).isPPTOn
+  exact hbody.isOraclePPTOn.isOraclePPT
+
+theorem isQueryBounded_zeroCPAAdversary (n : ℕ) :
+    (zeroCPAAdversary n []).IsQueryBounded 0 :=
+  ProbOracleComp.IsQueryBounded.sample (pure false)
+
+/-- Zero-query CI adversary that outputs `0^n`. -/
+def zeroCIAdversary : CIAdversary :=
+  fun n _ => ProbOracleComp.sample (pure (List.replicate n false))
+
+theorem isOraclePPT_zeroCIAdversary : IsOraclePPT encBits zeroCIAdversary := by
+  have hrep : ComputableTidilyInPolyTime
+      (fun p : ℕ × List Bool => List.replicate p.1 false)
+      (encPair encUnary encBits) encBits := by polytime
+  exact hrep.isPPTOn.isOraclePPTOn.isOraclePPT
+
+-- Composed closed-game `IsPPT` and Theorem 9.2 / Theorem 5.2 reduction `IsOraclePPT` certificates
+-- on `echoPrfCipher` and `echoPrfMAC`.
+example :
+    IsPPT encBool
+      (fun n _ =>
+        echoPrfMAC.sufCmaGame
+          (etmToMACForger echoPrfCipher echoPrfMAC (fun n => 2 * n) zeroCIAdversary) n) :=
+  echoPrfMAC.isPPT_sufCmaGame
+    (isOraclePPT_etmToMACForger echoPrfCipher echoPrfMAC (by polytime) isOraclePPT_zeroCIAdversary)
+
+example (bit : Bool) :
+    IsPPT encBool
+      (fun n _ =>
+        echoPrfCipher.cpaGame (etmToCPAAdversary echoPrfMAC zeroCPAAdversary) bit n) :=
+  echoPrfCipher.isPPT_cpaGame
+    (isOraclePPT_etmToCPAAdversary echoPrfMAC isOraclePPT_zeroCPAAdversary)
+    bit
+
+example (bit : Bool) :
+    IsOraclePPT encBool
+      (cpaToPrfDistinguisher (etmToCPAAdversary echoPrfMAC zeroCPAAdversary) bit) :=
+  isOraclePPT_cpaToPrfDistinguisher
+    (isOraclePPT_etmToCPAAdversary echoPrfMAC isOraclePPT_zeroCPAAdversary) bit
+
+-- Quantitative Theorem 9.2 and Theorem 5.2 equations and bounds instantiated on `echoPrfCipher`,
+-- `echoPrfMAC`, and `echoPrfEtM`.
+example (n : ℕ) :
+    Game.succProbability (ProbComp.eval (echoPrfEtM.ciGame zeroCIAdversary n)) =
       Game.succProbability
-        (ProbComp.eval (M.sufCmaGame (etmToMACForger E M tagBound ciAdv) n)) :=
-  succProbability_ciGame_encryptThenMAC_eq E M hctLen tagBound ciAdv n htagBoundN
+        (ProbComp.eval
+          (echoPrfMAC.sufCmaGame
+            (etmToMACForger echoPrfCipher echoPrfMAC (fun n => 2 * n) zeroCIAdversary) n)) := by
+  have htag (km : List Bool) (hkm : km ∈ (ProbComp.eval (echoPrfMAC.keyGen n)).support)
+      (c : List Bool) (_hc : c.length = echoPrfMAC.msgLen n)
+      (tag : List Bool) (htag : tag ∈ (ProbComp.eval (echoPrfMAC.sign km c)).support) :
+      tag.length ≤ 2 * n := by
+    change km ∈ (ProbComp.eval (BitString.sampleList (2 * n))).support at hkm
+    rw [BitString.eval_sampleList, BitString.mem_support_uniformList_iff] at hkm
+    change tag ∈ (ProbComp.eval (pure (prfOracle echoFamily km.length km c))).support at htag
+    rw [ProbComp.eval_pure, PMF.mem_support_pure_iff] at htag
+    subst htag
+    unfold prfOracle
+    split_ifs with hlen
+    · exact (echoFamily_length km c hlen).le.trans hkm.le
+    · simp
+  exact succProbability_ciGame_encryptThenMAC_eq echoPrfCipher echoPrfMAC
+    (prfCipher_ciphertext_length echoFamily echoFamily_polyTime echoFamily_length)
+    (fun n => 2 * n) zeroCIAdversary n htag
+
+example (n Q : ℕ) (cpaAdv : OracleDistinguisher)
+    (hq : (etmToCPAAdversary echoPrfMAC cpaAdv n []).IsQueryBounded Q) :
+    (Game.advantage
+        (ProbComp.eval (echoPrfEtM.cpaGame cpaAdv false n))
+        (ProbComp.eval (echoPrfEtM.cpaGame cpaAdv true n)) : ℝ) ≤
+      (Game.advantage
+        (ProbComp.eval
+          (prfRealGame echoFamily
+            (cpaToPrfDistinguisher (etmToCPAAdversary echoPrfMAC cpaAdv) false) n))
+        (ProbComp.eval
+          (prfIdealGame
+            (cpaToPrfDistinguisher (etmToCPAAdversary echoPrfMAC cpaAdv) false) n)) : ℝ) +
+      (Game.advantage
+        (ProbComp.eval
+          (prfRealGame echoFamily
+            (cpaToPrfDistinguisher (etmToCPAAdversary echoPrfMAC cpaAdv) true) n))
+        (ProbComp.eval
+          (prfIdealGame
+            (cpaToPrfDistinguisher (etmToCPAAdversary echoPrfMAC cpaAdv) true) n)) : ℝ) +
+      2 * (Q : ℝ) ^ 2 / (2 : ℝ) ^ n := by
+  have heq :
+      Game.advantage
+        (ProbComp.eval (echoPrfEtM.cpaGame cpaAdv false n))
+        (ProbComp.eval (echoPrfEtM.cpaGame cpaAdv true n)) =
+      Game.advantage
+        (ProbComp.eval
+          (echoPrfCipher.cpaGame (etmToCPAAdversary echoPrfMAC cpaAdv) false n))
+        (ProbComp.eval
+          (echoPrfCipher.cpaGame (etmToCPAAdversary echoPrfMAC cpaAdv) true n)) :=
+    advantage_cpaGame_encryptThenMAC_eq echoPrfCipher echoPrfMAC
+      (prfCipher_ciphertext_length echoFamily echoFamily_polyTime echoFamily_length)
+      cpaAdv n
+  rw [heq]
+  exact advantage_cpaGame_prfCipher_le echoFamily echoFamily_polyTime echoFamily_length
+    (etmToCPAAdversary echoPrfMAC cpaAdv) n Q hq
 
 example (n : ℕ) :
-    Game.advantage
-      (ProbComp.eval ((encryptThenMAC E M hctLen).cpaGame cpaAdv false n))
-      (ProbComp.eval ((encryptThenMAC E M hctLen).cpaGame cpaAdv true n)) =
-    Game.advantage
-      (ProbComp.eval (E.cpaGame (etmToCPAAdversary M cpaAdv) false n))
-      (ProbComp.eval (E.cpaGame (etmToCPAAdversary M cpaAdv) true n)) :=
-  advantage_cpaGame_encryptThenMAC_eq E M hctLen cpaAdv n
-
-example (n Q : ℕ) (hq : (cpaAdv n []).IsQueryBounded Q) :
     (Game.advantage
-        (ProbComp.eval ((prfCipher family hpoly hlen).cpaGame cpaAdv false n))
-        (ProbComp.eval ((prfCipher family hpoly hlen).cpaGame cpaAdv true n)) : ℝ) ≤
+        (ProbComp.eval (echoPrfCipher.cpaGame zeroCPAAdversary false n))
+        (ProbComp.eval (echoPrfCipher.cpaGame zeroCPAAdversary true n)) : ℝ) ≤
       (Game.advantage
-        (ProbComp.eval (prfRealGame family (cpaToPrfDistinguisher cpaAdv false) n))
-        (ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher cpaAdv false) n)) : ℝ) +
+        (ProbComp.eval (prfRealGame echoFamily (cpaToPrfDistinguisher zeroCPAAdversary false) n))
+        (ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher zeroCPAAdversary false) n)) : ℝ) +
       (Game.advantage
-        (ProbComp.eval (prfRealGame family (cpaToPrfDistinguisher cpaAdv true) n))
-        (ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher cpaAdv true) n)) : ℝ) +
-      2 * (Q : ℝ) ^ 2 / (2 : ℝ) ^ n :=
-  advantage_cpaGame_prfCipher_le family hpoly hlen cpaAdv n Q hq
-
--- Generic asymptotic compositions (Theorem 9.2).
-example (hmac : M.SUFCMA) : (encryptThenMAC E M hctLen).CiphertextIntegrity :=
-  ciphertextIntegrity_encryptThenMAC E M hctLen hmac
-
-example (hcpa : E.INDCPA) : (encryptThenMAC E M hctLen).INDCPA :=
-  indcpa_encryptThenMAC E M hctLen hcpa
-
-example (hcpa : E.INDCPA) (hmac : M.SUFCMA) :
-    (encryptThenMAC E M hctLen).AuthenticatedEncryption :=
-  authenticatedEncryption_encryptThenMAC E M hctLen hcpa hmac
-
-example (hcpa : E.INDCPA) (hmac : M.SUFCMA) :
-    (encryptThenMAC E M hctLen).INDCCA :=
-  indcca_encryptThenMAC E M hctLen hcpa hmac
-
--- Reindexed `prfMAC` corollaries.
-example {ctLen : ℕ → ℕ}
-    (hctPoly : ComputableInPolyTime ctLen encUnary encUnary)
-    (hctMono : StrictMono ctLen)
-    (hctLenPrf : ∀ n ke, ke ∈ (ProbComp.eval (E.keyGen n)).support →
-      ∀ msg, msg.length = n →
-      ∀ c ∈ (ProbComp.eval (E.encrypt n ke msg)).support, c.length = ctLen n)
-    (hcpa : E.INDCPA) :
-    (encryptThenMAC E
-      ((prfMAC family hprf.polyTime).reindex ctLen hctPoly)
-      hctLenPrf).AuthenticatedEncryption :=
-  authenticatedEncryption_encryptThenMAC_prfMAC E hprf hctPoly hctMono hctLenPrf hcpa
-
-example {ctLen : ℕ → ℕ}
-    (hctPoly : ComputableInPolyTime ctLen encUnary encUnary)
-    (hctMono : StrictMono ctLen)
-    (hctLenPrf : ∀ n ke, ke ∈ (ProbComp.eval (E.keyGen n)).support →
-      ∀ msg, msg.length = n →
-      ∀ c ∈ (ProbComp.eval (E.encrypt n ke msg)).support, c.length = ctLen n)
-    (hcpa : E.INDCPA) :
-    (encryptThenMAC E
-      ((prfMAC family hprf.polyTime).reindex ctLen hctPoly)
-      hctLenPrf).INDCCA :=
-  indcca_encryptThenMAC_prfMAC E hprf hctPoly hctMono hctLenPrf hcpa
-
--- End-to-end non-vacuous instantiation from `PseudorandomFunction` (Theorems 5.2 and 9.2).
-example : (prfCipher family hprf.polyTime hprf.length_eq).INDCPA :=
-  hprf.indcpa_prfCipher
-
-example : (prfEncryptThenMAC family hprf.polyTime hprf.length_eq).AuthenticatedEncryption :=
-  hprf.authenticatedEncryption_prfEncryptThenMAC
-
-example : (prfEncryptThenMAC family hprf.polyTime hprf.length_eq).INDCCA :=
-  hprf.indcca_prfEncryptThenMAC
-
-end CertificatesAndReductions
+        (ProbComp.eval (prfRealGame echoFamily (cpaToPrfDistinguisher zeroCPAAdversary true) n))
+        (ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher zeroCPAAdversary true) n)) : ℝ) := by
+  have h := advantage_cpaGame_prfCipher_le echoFamily echoFamily_polyTime echoFamily_length
+    zeroCPAAdversary n 0 (isQueryBounded_zeroCPAAdversary n)
+  simpa [echoPrfCipher] using h
 
 end ComplexityTests.Crypto.EncryptThenMAC
diff --git a/ComplexityTests/QueryComplexity.lean b/ComplexityTests/QueryComplexity.lean
index 1e2c3eec7..dfac87347 100644
--- a/ComplexityTests/QueryComplexity.lean
+++ b/ComplexityTests/QueryComplexity.lean
@@ -18,21 +18,28 @@ namespace ComplexityTests.QueryComplexity
 open Cslib Cslib.BitString Cslib.QueryComplexity Finset
 open scoped BigOperators
 
--- These are CSLib's measures, used directly by the local decision-tree bounds.
-example {n : ℕ} (f : BooleanFunction n) :
-    DecisionTree.complexity f ≤
-      certificateComplexityFor f false * certificateComplexityFor f true :=
-  DecisionTree.complexity_le_certificateComplexityFor_mul f
-
-example {n : ℕ} (f : BooleanFunction n) :
-    DecisionTree.complexity f ≤ Cslib.QueryComplexity.certificateComplexity f ^ 2 :=
-  DecisionTree.complexity_le_certificateComplexity_sq f
-
-example {n : ℕ} :
-    sensitivity (parity n) = n ∧ blockSensitivity (parity n) = n ∧
-      certificateComplexity (parity n) = n ∧ DecisionTree.complexity (parity n) = n :=
-  ⟨sensitivity_parity, blockSensitivity_parity, certificateComplexity_parity,
-    DecisionTree.complexity_parity⟩
+-- On 2-bit conjunction, 0-certificates have size 1 and 1-certificates have size 2, so the
+-- product bound gives D(and₂) ≤ 1 * 2 = 2. In the second example, the computed
+-- `certificateComplexity and₂ = 2` is the substantive check; the instantiated `C²` bound
+-- `D(and₂) ≤ 4` is weaker than the trivial `complexity_le_card` bound of 2.
+private def and₂ : BooleanFunction 2 := fun x => x 0 && x 1
+
+example :
+    certificateComplexityFor and₂ false = 1 ∧
+      certificateComplexityFor and₂ true = 2 ∧
+      DecisionTree.complexity and₂ ≤ 2 := by
+  have h0 : certificateComplexityFor and₂ false = 1 := by decide
+  have h1 : certificateComplexityFor and₂ true = 2 := by decide
+  refine ⟨h0, h1, ?_⟩
+  simpa [h0, h1] using DecisionTree.complexity_le_certificateComplexityFor_mul and₂
+
+example :
+    certificateComplexity and₂ = 2 ∧ DecisionTree.complexity and₂ ≤ 4 := by
+  have hc : certificateComplexity and₂ = 2 := by decide
+  refine ⟨hc, ?_⟩
+  simpa [hc] using DecisionTree.complexity_le_certificateComplexity_sq and₂
+
+example : sensitivity (parity 3) = 3 ∧ certificateComplexity (parity 3) = 3 := by decide
 
 -- The finite minimum is executable, including empty-coordinate and missing-output cases.
 example : certificateComplexityAt (parity 2) (fun _ => false) = 2 := by decide
@@ -77,9 +84,17 @@ example : {0} ⊆ natTree.queries (fun _ => false) := by
   decide
 
 -- Upstream assignments and generic restrictions need no conversion or alternative encoding.
-example {n : ℕ} (C : Cslib.QueryComplexity.PartialAssignment n) (x : BitString n) :
-    Cslib.QueryComplexity.Agrees C x ↔ Cslib.BitString.PartialAssignment.fill C x = x :=
-  Cslib.BitString.PartialAssignment.agrees_iff_fill_eq
+private def fixZeroFalse : Cslib.QueryComplexity.PartialAssignment 3 :=
+  fun i => if i = 0 then some false else none
+
+example :
+    Cslib.QueryComplexity.Agrees fixZeroFalse ![false, true, false] ∧
+      ¬ Cslib.QueryComplexity.Agrees fixZeroFalse ![true, true, false] := by
+  change Cslib.BitString.PartialAssignment.Agrees fixZeroFalse ![false, true, false] ∧
+    ¬ Cslib.BitString.PartialAssignment.Agrees fixZeroFalse ![true, true, false]
+  rw [Cslib.BitString.PartialAssignment.agrees_iff_fill_eq,
+    Cslib.BitString.PartialAssignment.agrees_iff_fill_eq]
+  decide
 
 example {n : ℕ} (C : Cslib.QueryComplexity.PartialAssignment n) :
     Cslib.QueryComplexity.support C = Cslib.BitString.PartialAssignment.support C := rfl
@@ -96,22 +111,28 @@ example {n : ℕ} (x y : BitString n) (S : Finset (Fin n)) :
     Cslib.BitString.PartialAssignment.fill (Cslib.QueryComplexity.restrict x S) y =
       S.piecewise x y := by simp
 
-example {ι β : Type*} [Finite ι] (C : Cslib.BitString.PartialAssignment ι)
-    (f : (ι → Bool) → β) : DecisionTree.complexity (f ∘ C.fill) ≤ DecisionTree.complexity f :=
-  DecisionTree.complexity_comp_fill_le C f
+example :
+    2 ≤ DecisionTree.complexity (parity 3 ∘ Cslib.BitString.PartialAssignment.fill fixZeroFalse) ∧
+      DecisionTree.complexity (parity 3 ∘ Cslib.BitString.PartialAssignment.fill fixZeroFalse) ≤
+        3 := by
+  have hfree : #(Cslib.BitString.PartialAssignment.free fixZeroFalse) = 2 := by decide
+  refine ⟨?_, ?_⟩
+  · simpa [hfree, Function.comp_def] using
+      DecisionTree.card_free_le_complexity_parity_fill fixZeroFalse
+  · exact (DecisionTree.complexity_comp_fill_le fixZeroFalse (parity 3)).trans_eq
+      DecisionTree.complexity_parity
 
 -- Generic Fourier theory and the native sensitivity corollary coexist.
-example {ι : Type*} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) :
-    totalInfluence (fun x => signVal (f x)) =
-      𝔼 x, (#{i | f (Function.update x i (!x i)) ≠ f x} : ℝ) :=
-  totalInfluence_signVal f
-
-example {n : ℕ} (f : BooleanFunction n) :
-    totalInfluence (fun x => signVal (f x)) = 𝔼 x, (sensitivityAt f x : ℝ) :=
-  totalInfluence_eq_expect_sensitivityAt f
-
-example {n : ℕ} (f : BooleanFunction n) :
-    totalInfluence (fun x => signVal (f x)) ≤ sensitivity f :=
-  totalInfluence_le_sensitivity f
+example (b : Bool) : totalInfluence (fun _ : Bool → Bool => signVal b) = 0 := by
+  rw [totalInfluence_signVal (fun _ : Bool → Bool => b)]
+  simp
+
+example {n : ℕ} : totalInfluence (fun x => signVal (parity n x)) = n := by
+  rw [totalInfluence_eq_expect_sensitivityAt (parity n)]
+  simp [sensitivityAt_parity]
+
+example : totalInfluence (fun x => signVal (and₂ x)) ≤ 2 := by
+  have hs : sensitivity and₂ = 2 := by decide
+  simpa [hs] using totalInfluence_le_sensitivity and₂
 
 end ComplexityTests.QueryComplexity