diff --git a/Complexity.lean b/Complexity.lean
index 6db0c8e90..866bd0252 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -950,7 +950,10 @@ public import Complexity.Computability.Circuit.Pi
 public import Complexity.Computability.Circuit.Pointwise
 public import Complexity.Computability.Circuit.Program
 public import Complexity.Computability.Circuit.Quantum.Basic
+public import Complexity.Computability.Circuit.Quantum.Classical
 public import Complexity.Computability.Circuit.Quantum.Code
+public import Complexity.Computability.Circuit.Quantum.Counter
+public import Complexity.Computability.Circuit.Quantum.Parallel
 public import Complexity.Computability.Circuit.Quantum.Uniform
 public import Complexity.Computability.Circuit.Rational
 public import Complexity.Computability.Circuit.Rational.Affine
@@ -1058,6 +1061,7 @@ public import Complexity.Computability.Complexity.Classes.BPP.Reduction
 public import Complexity.Computability.Complexity.Classes.BPP.WorstCaseHardness
 public import Complexity.Computability.Complexity.Classes.BPPpath
 public import Complexity.Computability.Complexity.Classes.BQP
+public import Complexity.Computability.Complexity.Classes.BQP.Amplification
 public import Complexity.Computability.Complexity.Classes.BooleanHierarchy
 public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Closure
 public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Kadin
@@ -2637,6 +2641,7 @@ public import Complexity.Foundations.Combinatorics.LineCode.Menu.Collision
 public import Complexity.Foundations.Combinatorics.LineCode.Menu.Counting
 public import Complexity.Foundations.Combinatorics.MajorityTree
 public import Complexity.Foundations.Combinatorics.MajorityVote
+public import Complexity.Foundations.Combinatorics.MajorityVote.Weighted
 public import Complexity.Foundations.Combinatorics.Multigraph
 public import Complexity.Foundations.Combinatorics.PacketPacking
 public import Complexity.Foundations.Combinatorics.PartialLabelScores
diff --git a/Complexity/Computability/Circuit/Quantum/Classical.lean b/Complexity/Computability/Circuit/Quantum/Classical.lean
new file mode 100644
index 000000000..73e2bbcad
--- /dev/null
+++ b/Complexity/Computability/Circuit/Quantum/Classical.lean
@@ -0,0 +1,324 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Quantum.Code
+
+/-!
+# Classical gate codes on basis states
+
+The classical gate codes NOT, CNOT and Toffoli of
+`Complexity/Computability/Circuit/Quantum/Code.lean` permute the computational basis: the code
+`(false, t, cs)` flips bit `t` when every bit of `cs` is one
+(`Cslib.Quantum.GateCode.classicalStep`). A list of classical codes therefore maps the basis
+state `|x⟩` to the basis state of the composed permutation
+(`Cslib.Quantum.Circuit.eval_ofCodes_ket`), and it acts on any state by reading amplitudes back
+through the inverse permutation (`Cslib.Quantum.Circuit.eval_ofCodes_apply`). Measuring after a
+classical circuit is measuring before it and then applying the permutation to the outcome
+(`Cslib.Quantum.Circuit.measureProb_eval_ofCodes`).
+
+Bits of a basis string are read by their number (`Cslib.Quantum.readBit`), as in gate codes.
+
+## Main definitions
+
+* `Cslib.Quantum.readBit`: bit `c` of a basis string, `false` past its end.
+* `Cslib.Quantum.GateCode.classicalStep`: the permutation of a classical gate code.
+* `Cslib.Quantum.GateCode.IsClassical`: a list of well-formed classical gate codes.
+* `Cslib.Quantum.GateCode.classicalRun`, `Cslib.Quantum.GateCode.classicalUnrun`: the composed
+  permutation of a list of classical codes and its inverse.
+* `Cslib.Quantum.GateCode.swapCodes`: three CNOT gates moving a qubit into qubit `0`.
+
+## Main results
+
+* `Cslib.Quantum.GateCode.readBit_classicalStep`: a classical code changes only its target.
+* `Cslib.Quantum.Circuit.eval_ofCodes_ket`, `Cslib.Quantum.Circuit.eval_ofCodes_apply`: classical
+  circuits permute basis states.
+* `Cslib.Quantum.Circuit.measureProb_eval_ofCodes`: measuring after a classical circuit.
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum
+
+open Finset
+
+variable {m : ℕ}
+
+/-- Bit number `c` of a basis string, and `false` past its end. -/
+def readBit (x : Fin m → Bool) (c : ℕ) : Bool := (List.ofFn x).getD c false
+
+theorem readBit_of_lt (x : Fin m → Bool) {c : ℕ} (h : c < m) : readBit x c = x ⟨c, h⟩ := by
+  simp [readBit, List.getD_eq_getElem?_getD, h]
+
+theorem readBit_of_le (x : Fin m → Bool) {c : ℕ} (h : m ≤ c) : readBit x c = false := by
+  simp [readBit, List.getD_eq_getElem?_getD, h]
+
+@[simp] theorem readBit_fin (x : Fin m → Bool) (i : Fin m) : readBit x i = x i :=
+  readBit_of_lt x i.2
+
+/-- Basis strings are equal when they have the same bits. -/
+theorem funext_readBit {x y : Fin m → Bool} (h : ∀ c, readBit x c = readBit y c) : x = y :=
+  funext fun i => by simpa using h i
+
+namespace GateCode
+
+/-- The permutation of basis strings of the classical gate code `(false, t, cs)`: bit `t` flips when
+every bit of `cs` is one. It is the identity when `t` is out of range. -/
+def classicalStep (g : GateCode) (x : Fin m → Bool) : Fin m → Bool :=
+  if h : g.2.1 < m then Function.update x ⟨g.2.1, h⟩ (x ⟨g.2.1, h⟩ ^^ g.2.2.all (readBit x))
+  else x
+
+/-- **A classical code changes only its target bit**, flipping it when all its controls are one. -/
+theorem readBit_classicalStep (g : GateCode) (x : Fin m → Bool) (c : ℕ) :
+    readBit (classicalStep g x) c =
+      (readBit x c ^^ (decide (c = g.2.1 ∧ g.2.1 < m) && g.2.2.all (readBit x))) := by
+  unfold classicalStep
+  split_ifs with h
+  · by_cases hc : c < m
+    · rw [readBit_of_lt _ hc, readBit_of_lt _ hc]
+      by_cases hct : c = g.2.1
+      · subst hct
+        simp [h]
+      · rw [Function.update_of_ne (fun h' => hct (congrArg Fin.val h'))]
+        simp [hct]
+    · rw [readBit_of_le _ (not_lt.mp hc), readBit_of_le _ (not_lt.mp hc)]
+      have : c ≠ g.2.1 := fun h' => hc (h' ▸ h)
+      simp [this]
+  · simp [h]
+
+/-- Bits other than the target of a classical code read the same after it acts. -/
+theorem all_readBit_classicalStep {g : GateCode} (x : Fin m → Bool)
+    (cs : List ℕ) (hcs : g.2.1 ∉ cs) :
+    cs.all (readBit (classicalStep g x)) = cs.all (readBit x) := by
+  induction cs with
+  | nil => rfl
+  | cons c cs ih =>
+    rw [List.all_cons, List.all_cons, ih (fun h => hcs (List.mem_cons_of_mem _ h)),
+      readBit_classicalStep]
+    have : c ≠ g.2.1 := fun h => hcs (h ▸ List.mem_cons_self ..)
+    simp [this]
+
+/-- **A classical code is an involution** when its target is not one of its controls. -/
+theorem classicalStep_classicalStep {g : GateCode} (hg : g.2.1 ∉ g.2.2) (x : Fin m → Bool) :
+    classicalStep g (classicalStep g x) = x := by
+  refine funext_readBit fun c => ?_
+  rw [readBit_classicalStep, all_readBit_classicalStep x _ hg, readBit_classicalStep,
+    Bool.xor_assoc, Bool.xor_self, Bool.xor_false]
+
+/-- A list of **classical gate codes**, well formed on `m` qubits: NOT, CNOT and Toffoli gates. -/
+def IsClassical (m : ℕ) (gs : List GateCode) : Prop :=
+  ∀ g ∈ gs, g.1 = false ∧ WellFormed m g
+
+theorem IsClassical.cons {g : GateCode} {gs : List GateCode} :
+    IsClassical m (g :: gs) ↔ (g.1 = false ∧ WellFormed m g) ∧ IsClassical m gs :=
+  List.forall_mem_cons
+
+theorem IsClassical.append {gs hs : List GateCode} :
+    IsClassical m (gs ++ hs) ↔ IsClassical m gs ∧ IsClassical m hs :=
+  List.forall_mem_append
+
+theorem IsClassical.flatMap {β : Type*} {l : List β} {f : β → List GateCode}
+    (h : ∀ b ∈ l, IsClassical m (f b)) : IsClassical m (l.flatMap f) := by
+  intro g hg
+  obtain ⟨b, hb, hg⟩ := List.mem_flatMap.mp hg
+  exact h b hb g hg
+
+/-- The target of a well-formed classical code is not one of its controls. -/
+theorem target_notMem_of_wellFormed {g : GateCode} (h₁ : g.1 = false) (h₂ : WellFormed m g) :
+    g.2.1 ∉ g.2.2 := by
+  obtain ⟨b, t, cs⟩ := g
+  subst h₁
+  exact (List.nodup_cons.mp h₂.2.1).1
+
+/-- The composed permutation of a list of classical codes, applied first to last. -/
+def classicalRun (gs : List GateCode) (x : Fin m → Bool) : Fin m → Bool :=
+  gs.foldl (fun y g => classicalStep g y) x
+
+/-- The inverse of `classicalRun`: the permutations applied last to first. -/
+def classicalUnrun (gs : List GateCode) (y : Fin m → Bool) : Fin m → Bool :=
+  gs.foldr (fun g y => classicalStep g y) y
+
+@[simp] theorem classicalRun_nil (x : Fin m → Bool) : classicalRun [] x = x := rfl
+
+@[simp] theorem classicalRun_cons (g : GateCode) (gs : List GateCode) (x : Fin m → Bool) :
+    classicalRun (g :: gs) x = classicalRun gs (classicalStep g x) := rfl
+
+theorem classicalRun_append (gs hs : List GateCode) (x : Fin m → Bool) :
+    classicalRun (gs ++ hs) x = classicalRun hs (classicalRun gs x) :=
+  List.foldl_append
+
+@[simp] theorem classicalUnrun_nil (y : Fin m → Bool) : classicalUnrun [] y = y := rfl
+
+@[simp] theorem classicalUnrun_cons (g : GateCode) (gs : List GateCode) (y : Fin m → Bool) :
+    classicalUnrun (g :: gs) y = classicalStep g (classicalUnrun gs y) := rfl
+
+theorem classicalUnrun_classicalRun {gs : List GateCode} (h : IsClassical m gs)
+    (x : Fin m → Bool) : classicalUnrun gs (classicalRun gs x) = x := by
+  induction gs generalizing x with
+  | nil => rfl
+  | cons g gs ih =>
+    obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h
+    rw [classicalRun_cons, classicalUnrun_cons, ih h,
+      classicalStep_classicalStep (target_notMem_of_wellFormed h₁ h₂)]
+
+theorem classicalRun_classicalUnrun {gs : List GateCode} (h : IsClassical m gs)
+    (y : Fin m → Bool) : classicalRun gs (classicalUnrun gs y) = y := by
+  induction gs generalizing y with
+  | nil => rfl
+  | cons g gs ih =>
+    obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h
+    rw [classicalUnrun_cons, classicalRun_cons,
+      classicalStep_classicalStep (target_notMem_of_wellFormed h₁ h₂), ih h]
+
+theorem classicalRun_flatMap {β : Type*} (l : List β) (f : β → List GateCode)
+    (x : Fin m → Bool) :
+    classicalRun (l.flatMap f) x = l.foldl (fun y b => classicalRun (f b) y) x :=
+  List.foldl_flatMap
+
+/-- **Classical codes that never read a written bit** add to each bit the controls' values on the
+initial string, one for each code writing that bit. -/
+theorem readBit_classicalRun_of_forall_notMem {gs : List GateCode} (h : IsClassical m gs)
+    (hread : ∀ g ∈ gs, ∀ g' ∈ gs, g.2.1 ∉ g'.2.2) (x : Fin m → Bool) (p : ℕ) :
+    readBit (classicalRun gs x) p =
+      gs.foldl (fun b g => b ^^ (decide (p = g.2.1) && g.2.2.all (readBit x))) (readBit x p) := by
+  induction gs generalizing x with
+  | nil => rfl
+  | cons g gs ih =>
+    obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h
+    have ht : g.2.1 < m := by
+      obtain ⟨b, t, cs⟩ := g
+      subst h₁
+      exact h₂.2.2 t (List.mem_cons_self ..)
+    rw [classicalRun_cons, ih h (fun g₁ hg₁ g₂ hg₂ => hread g₁ (List.mem_cons_of_mem _ hg₁) g₂
+      (List.mem_cons_of_mem _ hg₂)), List.foldl_cons, readBit_classicalStep]
+    simp only [ht, and_true]
+    refine List.foldl_ext _ _ _ fun b g' hg' => ?_
+    rw [all_readBit_classicalStep x _ (hread g (List.mem_cons_self ..) g'
+      (List.mem_cons_of_mem _ hg'))]
+
+/-- An exclusive or over a range in which only the term `i₀` can be nonzero. -/
+theorem foldl_xor_range (T i₀ : ℕ) (f : ℕ → Bool) (b : Bool) (hf : ∀ i < T, i ≠ i₀ → f i = false) :
+    (List.range T).foldl (fun b i => b ^^ f i) b = (b ^^ (decide (i₀ < T) && f i₀)) := by
+  induction T with
+  | zero => simp
+  | succ T ih =>
+    rw [List.range_succ, List.foldl_append, ih fun i hi hne => hf i (by omega) hne]
+    simp only [List.foldl_cons, List.foldl_nil]
+    by_cases hT : T = i₀
+    · subst hT
+      simp
+    · rw [hf T (by omega) hT]
+      by_cases hlt : i₀ < T
+      · simp [hlt, show i₀ < T + 1 by omega]
+      · simp [hlt, show ¬i₀ < T + 1 by omega]
+
+/-- A well-formed classical code denotes a gate that maps `|x⟩` to `|classicalStep g x⟩`. -/
+theorem exists_toPlacedGate?_eval_ket {g : GateCode} (h₁ : g.1 = false) (h₂ : WellFormed m g) :
+    ∃ pg, toPlacedGate? m g = some pg ∧ ∀ x, pg.eval (ket x) = ket (classicalStep g x) := by
+  obtain ⟨pg, hpg⟩ := Option.isSome_iff_exists.mp (isSome_toPlacedGate?_iff.mpr h₂)
+  obtain ⟨b, t, cs⟩ := g
+  subst h₁
+  have ht : t < m := h₂.2.2 t (List.mem_cons_self ..)
+  refine ⟨pg, hpg, fun x => ?_⟩
+  rw [eval_toPlacedGate_ket hpg ht]
+  simp only [classicalStep, ht, ↓reduceDIte]
+  rfl
+
+/-- A well-formed classical code reads each amplitude at the permuted basis string. -/
+theorem exists_toPlacedGate?_eval_apply {g : GateCode} (h₁ : g.1 = false) (h₂ : WellFormed m g) :
+    ∃ pg, toPlacedGate? m g = some pg ∧
+      ∀ (ψ : Qubits m) y, (pg.eval ψ).ofLp y = ψ.ofLp (classicalStep g y) := by
+  obtain ⟨pg, hpg, hket⟩ := exists_toPlacedGate?_eval_ket h₁ h₂
+  refine ⟨pg, hpg, fun ψ y => ?_⟩
+  have hinv := classicalStep_classicalStep (m := m) (target_notMem_of_wellFormed h₁ h₂)
+  have hrow (z : Fin m → Bool) :
+      (pg.matrix : Matrix _ _ ℂ) y z = if z = classicalStep g y then 1 else 0 := by
+    rw [← PlacedGate.eval_ket_apply, hket, ket_apply]
+    refine if_congr ⟨fun h => ?_, fun h => ?_⟩ rfl rfl
+    · rw [h, hinv]
+    · rw [h, hinv]
+  simp only [PlacedGate.eval, unitaryEquiv_apply, Matrix.mulVec, dotProduct, hrow, ite_mul,
+    one_mul, zero_mul, sum_ite_eq', mem_univ, ite_true]
+
+
+/-! ### Swapping a qubit into qubit `0` -/
+
+/-- Three CNOT gates swapping qubit `a` into qubit `0`. -/
+def swapCodes (a : ℕ) : List GateCode := [(false, 0, [a]), (false, a, [0]), (false, 0, [a])]
+
+theorem isClassical_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) :
+    IsClassical N (swapCodes a) := by
+  have h₀ : WellFormed N ((false, 0, [a]) : GateCode) :=
+    ⟨by simp, by simp; omega, by simp; omega⟩
+  have h₁ : WellFormed N ((false, a, [0]) : GateCode) :=
+    ⟨by simp, by simp; omega, by simp; omega⟩
+  intro g hg
+  simp only [swapCodes, List.mem_cons, List.not_mem_nil, or_false] at hg
+  rcases hg with rfl | rfl | rfl
+  · exact ⟨rfl, h₀⟩
+  · exact ⟨rfl, h₁⟩
+  · exact ⟨rfl, h₀⟩
+
+/-- **The swap moves qubit `a` into qubit `0`.** -/
+theorem readBit_classicalRun_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) (X : Fin N → Bool) :
+    readBit (classicalRun (swapCodes a) X) 0 = readBit X a := by
+  simp only [swapCodes, classicalRun_cons, classicalRun_nil, readBit_classicalStep,
+    List.all_cons, List.all_nil, Bool.and_true]
+  have h0 : (0 : ℕ) < N := by omega
+  simp [h0, hN, show a ≠ 0 by omega, show (0 : ℕ) ≠ a by omega]
+
+end GateCode
+
+open GateCode
+
+namespace Circuit
+
+/-- **A classical circuit permutes basis states.** -/
+theorem eval_ofCodes_ket {gs : List GateCode} (h : IsClassical m gs) (x : Fin m → Bool) :
+    eval (ofCodes m gs) (ket x) = ket (classicalRun gs x) := by
+  induction gs generalizing x with
+  | nil => simp
+  | cons g gs ih =>
+    obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h
+    obtain ⟨pg, hpg, hket⟩ := exists_toPlacedGate?_eval_ket h₁ h₂
+    simp only [ofCodes, List.filterMap_cons, hpg, eval_cons, hket, classicalRun_cons]
+    exact ih h _
+
+/-- A classical circuit started in `|x⟩` ends in `|classicalRun gs x⟩`. -/
+theorem run_ofCodes {gs : List GateCode} (h : IsClassical m gs) (x : Fin m → Bool) :
+    run (ofCodes m gs) x = ket (classicalRun gs x) :=
+  eval_ofCodes_ket h x
+
+/-- **A classical circuit reads amplitudes through the inverse permutation.** -/
+theorem eval_ofCodes_apply {gs : List GateCode} (h : IsClassical m gs) (ψ : Qubits m)
+    (y : Fin m → Bool) : (eval (ofCodes m gs) ψ).ofLp y = ψ.ofLp (classicalUnrun gs y) := by
+  induction gs generalizing ψ with
+  | nil => simp
+  | cons g gs ih =>
+    obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h
+    obtain ⟨pg, hpg, happly⟩ := exists_toPlacedGate?_eval_apply h₁ h₂
+    simp only [ofCodes, List.filterMap_cons, hpg, eval_cons, classicalUnrun_cons]
+    rw [← happly]
+    exact ih h _
+
+/-- **Measuring after a classical circuit** is measuring before it and permuting the outcome. -/
+theorem measureProb_eval_ofCodes {gs : List GateCode} (h : IsClassical m gs) (ψ : Qubits m)
+    (S : Finset (Fin m → Bool)) :
+    measureProb (eval (ofCodes m gs) ψ) S =
+      ∑ x, if classicalRun gs x ∈ S then ‖ψ.ofLp x‖ ^ 2 else 0 := by
+  rw [measureProb, ← sum_filter]
+  simp only [eval_ofCodes_apply h]
+  refine sum_nbij' (classicalUnrun gs) (classicalRun gs) (fun y hy => ?_) (fun x hx => ?_)
+    (fun y _ => classicalRun_classicalUnrun h y) (fun x _ => classicalUnrun_classicalRun h x)
+    (fun y _ => rfl)
+  · simpa [classicalRun_classicalUnrun h] using hy
+  · simpa using (mem_filter.mp hx).2
+
+end Circuit
+
+end Cslib.Quantum
diff --git a/Complexity/Computability/Circuit/Quantum/Counter.lean b/Complexity/Computability/Circuit/Quantum/Counter.lean
new file mode 100644
index 000000000..6248614ae
--- /dev/null
+++ b/Complexity/Computability/Circuit/Quantum/Counter.lean
@@ -0,0 +1,227 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Quantum.Classical
+
+/-!
+# A reversible threshold counter
+
+A classical circuit of CNOT and Toffoli gates that counts, in unary, how many of `k` input bits
+are one, up to a threshold `T` (`Cslib.Quantum.Counter.codes`). Its ancillas start at zero: qubit
+`base` is set to one, and stage `s` has `T` fresh qubits, its *levels*
+(`Cslib.Quantum.Counter.level`). After stage `s`, level `i` reads whether more than `i` of the
+first `s` input bits are one. Stage `s + 1` reads the next input bit `b` and sets each new level
+to the old level `i - 1` when `b` is one and to the old level `i` otherwise, with three gates: the
+multiplexer `t ⊕ (b ∧ u) ⊕ (b ∧ t)` of the old levels `t` and `u`. No gate reads a qubit written in
+the same stage, so each stage is computed from the previous one
+(`Cslib.Quantum.GateCode.readBit_classicalRun_of_forall_notMem`).
+
+The last level of the last stage is the threshold function of the input bits
+(`Cslib.Quantum.Counter.readBit_classicalRun_codes`); with `k = 2 r` inputs and `T = r + 1` levels
+it is their strict majority. This is the reversible majority vote used to amplify the success
+probability of quantum circuits.
+
+## Main definitions
+
+* `Cslib.Quantum.Counter.level`, `Cslib.Quantum.Counter.stage`, `Cslib.Quantum.Counter.codes`.
+* `Cslib.Quantum.Counter.count`: the number of input bits that are one.
+
+## Main results
+
+* `Cslib.Quantum.Counter.isClassical_codes`: the counter is a classical circuit.
+* `Cslib.Quantum.Counter.readBit_classicalRun_codes`: it computes the threshold function and
+  leaves the qubits below `base` unchanged.
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum.Counter
+
+open Finset GateCode
+
+variable {N : ℕ}
+
+/-- The qubit of level `i` of stage `s`: after stage `s` it reads whether more than `i` of the
+first `s` input bits are one. -/
+def level (base T s i : ℕ) : ℕ := base + 1 + s * T + i
+
+/-- The qubit of level `i - 1` of stage `s`, where level `-1` is the qubit `base`, set to one. -/
+def below (base T s i : ℕ) : ℕ := if i = 0 then base else level base T s (i - 1)
+
+/-- Stage `s + 1` of the counter, reading the input bit at `b`: level `i` becomes level `i - 1` of
+stage `s` when the bit is one, and level `i` of stage `s` otherwise. -/
+def stage (base T b s : ℕ) : List GateCode :=
+  (List.range T).flatMap fun i =>
+    [(false, level base T (s + 1) i, [level base T s i]),
+      (false, level base T (s + 1) i, [b, below base T s i]),
+      (false, level base T (s + 1) i, [b, level base T s i])]
+
+/-- The counter for the input bits at `src 0, …, src (k - 1)`, with `T` levels and ancillas from
+`base` on: set qubit `base` to one, then run the stages. -/
+def codes (base T : ℕ) (src : ℕ → ℕ) (k : ℕ) : List GateCode :=
+  (false, base, []) :: (List.range k).flatMap fun s => stage base T (src s) s
+
+/-- The number of input bits that are one among the first `s`. -/
+def count (x : Fin N → Bool) (src : ℕ → ℕ) (s : ℕ) : ℕ :=
+  ((range s).filter fun j => readBit x (src j) = true).card
+
+theorem count_succ (x : Fin N → Bool) (src : ℕ → ℕ) (s : ℕ) :
+    count x src (s + 1) = count x src s + if readBit x (src s) = true then 1 else 0 := by
+  unfold count
+  rw [range_add_one, filter_insert]
+  split_ifs with h
+  · rw [card_insert_of_notMem (fun h' => by simpa using (mem_filter.mp h').1)]
+  · rw [Nat.add_zero]
+
+private theorem level_lt {base T s i : ℕ} (hi : i < T) :
+    level base T s i < base + 1 + (s + 1) * T := by
+  unfold level
+  rw [Nat.add_mul, Nat.one_mul]
+  omega
+
+theorem isClassical_stage {base T b s : ℕ} (hb : b < base) (hN : base + 1 + (s + 2) * T ≤ N) :
+    IsClassical N (stage base T b s) := by
+  refine IsClassical.flatMap fun i hi => ?_
+  have hi : i < T := List.mem_range.mp hi
+  have h₁ := level_lt (base := base) (s := s + 1) hi
+  have h₀ : base + 1 + s * T + i < base + 1 + (s + 1) * T * 1 := by
+    rw [Nat.mul_one, Nat.add_mul, Nat.one_mul]
+    omega
+  rw [show s + 2 = s + 1 + 1 by rfl, Nat.add_mul (s + 1), Nat.one_mul] at hN
+  rw [Nat.add_mul, Nat.one_mul] at h₁
+  rw [Nat.mul_one, Nat.add_mul, Nat.one_mul] at h₀
+  have hl : base + 1 + (s + 1) * T + i = base + 1 + s * T + T + i := by
+    rw [Nat.add_mul, Nat.one_mul]
+    omega
+  simp only [IsClassical, List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp,
+    forall_eq, WellFormed, List.length_cons, List.length_nil, List.nodup_cons, List.mem_cons,
+    List.not_mem_nil, List.nodup_nil, level, below, hl]
+  split_ifs with h0 <;> refine ⟨⟨trivial, ?_⟩, ⟨trivial, ?_⟩, ⟨trivial, ?_⟩⟩ <;> simp <;> omega
+
+theorem isClassical_codes {base T k : ℕ} {src : ℕ → ℕ} (hsrc : ∀ s < k, src s < base)
+    (hN : base + 1 + (k + 1) * T ≤ N) : IsClassical N (codes base T src k) := by
+  refine IsClassical.cons.mpr ⟨⟨rfl, ?_⟩, IsClassical.flatMap fun s hs => ?_⟩
+  · have : base < N := by omega
+    simp [WellFormed, this]
+  · have hs : s < k := List.mem_range.mp hs
+    refine isClassical_stage (hsrc s hs) (le_trans ?_ hN)
+    have : (s + 2) * T ≤ (k + 1) * T := Nat.mul_le_mul_right T (by omega)
+    omega
+
+/-- The bits after `s` stages: unchanged below `base`, one at `base`, the threshold values on the
+levels of stage `s`, and zero from the levels of stage `s + 1` on. -/
+private def Invariant (base T : ℕ) (src : ℕ → ℕ) (x y : Fin N → Bool) (s : ℕ) : Prop :=
+  (∀ p < base, readBit y p = readBit x p) ∧ readBit y base = true ∧
+    (∀ i < T, readBit y (level base T s i) = decide (i < count x src s)) ∧
+    ∀ p, base + 1 + (s + 1) * T ≤ p → readBit y p = false
+
+private theorem invariant_zero {base T : ℕ} {src : ℕ → ℕ} (hN : base < N) (x : Fin N → Bool)
+    (hx : ∀ p, base ≤ p → readBit x p = false) :
+    Invariant base T src x (classicalStep (false, base, []) x) 0 := by
+  have hstep (p : ℕ) : readBit (classicalStep (false, base, []) x) p =
+      (readBit x p ^^ decide (p = base)) := by
+    rw [readBit_classicalStep]
+    simp [hN]
+  refine ⟨fun p hp => ?_, ?_, fun i hi => ?_, fun p hp => ?_⟩
+  · rw [hstep]
+    simp [show p ≠ base by omega]
+  · rw [hstep, hx base le_rfl]
+    simp
+  · rw [hstep, hx _ (by unfold level; omega)]
+    simp only [count, level, Nat.zero_mul, Nat.add_zero, range_zero, filter_empty, card_empty,
+      Nat.not_lt_zero, decide_false, Bool.false_xor, decide_eq_false_iff_not]
+    omega
+  · rw [hstep, hx _ (by omega)]
+    simp only [Nat.zero_add, Nat.one_mul] at hp
+    simp [show p ≠ base by omega]
+
+private theorem invariant_succ {base T s : ℕ} {src : ℕ → ℕ} (hsrc : src s < base)
+    (hN : base + 1 + (s + 2) * T ≤ N) {x y : Fin N → Bool} (hy : Invariant base T src x y s) :
+    Invariant base T src x (classicalRun (stage base T (src s) s) y) (s + 1) := by
+  obtain ⟨hlow, hbase, hlev, hhigh⟩ := hy
+  have hcl := isClassical_stage (N := N) hsrc hN
+  rw [show s + 2 = s + 1 + 1 by rfl, Nat.add_mul (s + 1), Nat.one_mul, Nat.add_mul,
+    Nat.one_mul] at hN
+  -- the stage reads no bit it writes
+  have hread : ∀ g ∈ stage base T (src s) s, ∀ g' ∈ stage base T (src s) s, g.2.1 ∉ g'.2.2 := by
+    intro g hg g' hg'
+    simp only [stage, List.mem_flatMap, List.mem_range, List.mem_cons, List.not_mem_nil,
+      or_false] at hg hg'
+    obtain ⟨i, hi, rfl | rfl | rfl⟩ := hg <;> obtain ⟨i', hi', rfl | rfl | rfl⟩ := hg' <;>
+      simp only [level, below, List.mem_cons, List.not_mem_nil, or_false, Nat.add_mul,
+        Nat.one_mul] <;> (try split_ifs) <;> omega
+  -- each bit, as a sum over the levels of the stage
+  have hfold (p : ℕ) : readBit (classicalRun (stage base T (src s) s) y) p =
+      (List.range T).foldl (fun b i => b ^^ (decide (p = level base T (s + 1) i) &&
+        (readBit y (level base T s i) ^^ (readBit y (src s) && readBit y (below base T s i)) ^^
+          (readBit y (src s) && readBit y (level base T s i))))) (readBit y p) := by
+    rw [readBit_classicalRun_of_forall_notMem hcl hread, stage, List.foldl_flatMap]
+    refine List.foldl_ext _ _ _ fun b i _ => ?_
+    simp only [List.foldl_cons, List.foldl_nil, List.all_cons, List.all_nil, Bool.and_true]
+    cases decide (p = level base T (s + 1) i) <;> simp
+  -- bits that the stage does not write
+  have hkeep (p : ℕ) (hp : ∀ i < T, p ≠ level base T (s + 1) i) :
+      readBit (classicalRun (stage base T (src s) s) y) p = readBit y p := by
+    rw [hfold, foldl_xor_range T T _ _ fun i hi _ => by simp [hp i hi]]
+    simp
+  have hlev_ge (i : ℕ) : base + 1 + s * T + T ≤ level base T (s + 1) i := by
+    unfold level
+    rw [Nat.add_mul, Nat.one_mul]
+    omega
+  refine ⟨fun p hp => ?_, ?_, fun i₀ hi₀ => ?_, fun p hp => ?_⟩
+  · rw [hkeep p fun i _ => by have := hlev_ge i; omega, hlow p hp]
+  · rw [hkeep base fun i _ => by have := hlev_ge i; omega, hbase]
+  · have hne (i : ℕ) (hne : i ≠ i₀) : level base T (s + 1) i₀ ≠ level base T (s + 1) i := by
+      unfold level
+      omega
+    have hbelow : readBit y (below base T s i₀) = decide (i₀ ≤ count x src s) := by
+      unfold below
+      split_ifs with h0
+      · subst h0
+        simp [hbase]
+      · rw [hlev _ (by omega)]
+        exact decide_eq_decide.mpr (by omega)
+    rw [hfold, foldl_xor_range T i₀ _ _ fun i _ h => by simp [hne i h],
+      hhigh _ (by have := hlev_ge i₀; rw [Nat.add_mul, Nat.one_mul]; omega),
+      hlev i₀ hi₀, hlow _ hsrc, hbelow, count_succ]
+    simp only [hi₀, decide_true, Bool.true_and, Bool.false_xor]
+    cases hb : readBit x (src s)
+    · simp
+    · by_cases h1 : i₀ < count x src s <;> by_cases h2 : i₀ ≤ count x src s <;>
+        simp [h1, h2]
+  · have hp' : base + 1 + s * T + T + T ≤ p := by
+      simp only [Nat.add_mul, Nat.one_mul] at hp
+      omega
+    rw [hkeep p fun i hi => by unfold level; simp only [Nat.add_mul, Nat.one_mul]; omega,
+      hhigh p (by simp only [Nat.add_mul, Nat.one_mul]; omega)]
+
+/-- **The counter computes the threshold function**: started with zero ancillas from `base` on, it
+leaves the qubits below `base` unchanged, and level `i` of stage `k` reads whether more than `i` of
+the `k` input bits are one. -/
+theorem readBit_classicalRun_codes {base T k : ℕ} {src : ℕ → ℕ} (hsrc : ∀ s < k, src s < base)
+    (hN : base + 1 + (k + 1) * T ≤ N) (x : Fin N → Bool)
+    (hx : ∀ p, base ≤ p → readBit x p = false) :
+    (∀ p < base, readBit (classicalRun (codes base T src k) x) p = readBit x p) ∧
+      ∀ i < T, readBit (classicalRun (codes base T src k) x) (level base T k i) =
+        decide (i < count x src k) := by
+  suffices h : ∀ s ≤ k, Invariant base T src x
+      (classicalRun ((List.range s).flatMap fun s => stage base T (src s) s)
+        (classicalStep (false, base, []) x)) s by
+    obtain ⟨h₁, -, h₃, -⟩ := h k le_rfl
+    exact ⟨h₁, h₃⟩
+  intro s hs
+  induction s with
+  | zero => exact invariant_zero (by omega) x hx
+  | succ s ih =>
+    rw [List.range_succ, List.flatMap_append, List.flatMap_singleton, classicalRun_append]
+    refine invariant_succ (hsrc s (by omega)) (le_trans ?_ hN) (ih (by omega))
+    have : (s + 2) * T ≤ (k + 1) * T := Nat.mul_le_mul_right T (by omega)
+    omega
+
+end Cslib.Quantum.Counter
diff --git a/Complexity/Computability/Circuit/Quantum/Parallel.lean b/Complexity/Computability/Circuit/Quantum/Parallel.lean
new file mode 100644
index 000000000..41df21c32
--- /dev/null
+++ b/Complexity/Computability/Circuit/Quantum/Parallel.lean
@@ -0,0 +1,341 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Quantum.Code
+
+/-!
+# Circuits on parts of a larger register
+
+A circuit on `m` qubits runs on the qubits `e : Fin m ↪ Fin N` of a larger register
+(`Cslib.Quantum.Circuit.mapWires`). Its entries are those of the small circuit on the qubits `e`,
+provided the basis strings agree off `e` (`Cslib.Quantum.Circuit.matrix_mapWires`). Copies of one
+circuit on pairwise disjoint sets of qubits act independently: an entry of the whole is the product
+of the entries of the copies (`Cslib.Quantum.Circuit.matrix_flatMap_mapWires`). This is the tensor
+product structure behind running independent copies of a quantum computation in parallel.
+
+For gate codes, shifting every qubit number by `o` (`Cslib.Quantum.GateCode.shift`) places the
+circuit on the block of qubits `o, …, o + m - 1` (`Cslib.Quantum.Circuit.ofCodes_map_shift`).
+
+## Main definitions
+
+* `Cslib.Quantum.AgreeOff`: two basis strings agree off the range of an embedding.
+* `Cslib.Quantum.glue`: a basis string with part of it replaced.
+* `Cslib.Quantum.PlacedGate.mapWires`, `Cslib.Quantum.Circuit.mapWires`: running on a part of a
+  larger register.
+* `Cslib.Quantum.GateCode.shift`, `Cslib.Quantum.blockEmb`: shifted gate codes and blocks of qubits.
+
+## Main results
+
+* `Cslib.Quantum.sum_agreeOff`: summing over the basis strings that agree with `x` off `e`.
+* `Cslib.Quantum.Circuit.matrix_mapWires`: the entries of a circuit on part of a register.
+* `Cslib.Quantum.Circuit.matrix_flatMap_mapWires`: copies on disjoint parts act independently.
+* `Cslib.Quantum.Circuit.ofCodes_map_shift`: shifted gate codes denote a circuit on a block.
+* `Cslib.Quantum.GateCode.WellFormed.shift`: shifted gate codes are well formed on a larger
+  register.
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum
+
+open Finset
+
+variable {ι : Type*} {m N : ℕ}
+
+/-! ### Agreeing off part of a register -/
+
+
+/-- The basis strings `y` and `x` **agree off** the qubits `e`. -/
+def AgreeOff (e : ι ↪ Fin N) (y x : Fin N → Bool) : Prop :=
+  ∀ j, (∀ i, e i ≠ j) → y j = x j
+
+instance [Fintype ι] (e : ι ↪ Fin N) (y x : Fin N → Bool) : Decidable (AgreeOff e y x) := by
+  unfold AgreeOff; infer_instance
+
+theorem AgreeOff.refl (e : ι ↪ Fin N) (x : Fin N → Bool) : AgreeOff e x x := fun _ _ => rfl
+
+theorem AgreeOff.symm {e : ι ↪ Fin N} {y x : Fin N → Bool} (h : AgreeOff e y x) :
+    AgreeOff e x y := fun j hj => (h j hj).symm
+
+theorem AgreeOff.trans {e : ι ↪ Fin N} {z y x : Fin N → Bool} (h₁ : AgreeOff e z y)
+    (h₂ : AgreeOff e y x) : AgreeOff e z x := fun j hj => (h₁ j hj).trans (h₂ j hj)
+
+section Glue
+
+variable [Fintype ι]
+
+/-- The basis string `x` with the bits `z` on the qubits `e`. -/
+noncomputable def glue (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) : Fin N → Bool :=
+  fun j => if h : ∃ i, e i = j then z h.choose else x j
+
+@[simp] theorem glue_apply_emb (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) (i : ι) :
+    glue e z x (e i) = z i := by
+  have h : ∃ i', e i' = e i := ⟨i, rfl⟩
+  rw [glue, dite_eq_left h, e.injective h.choose_spec]
+
+theorem glue_of_not (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) {j : Fin N}
+    (hj : ∀ i, e i ≠ j) : glue e z x j = x j := by
+  rw [glue, dite_eq_right (by simpa using hj)]
+
+@[simp] theorem glue_comp (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) :
+    glue e z x ∘ e = z :=
+  funext fun i => glue_apply_emb e z x i
+
+theorem agreeOff_glue (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) :
+    AgreeOff e (glue e z x) x := fun _ hj => glue_of_not e z x hj
+
+theorem glue_comp_of_agreeOff {e : ι ↪ Fin N} {y x : Fin N → Bool} (h : AgreeOff e y x) :
+    glue e (y ∘ e) x = y := by
+  funext j
+  by_cases hj : ∃ i, e i = j
+  · obtain ⟨i, rfl⟩ := hj
+    simp
+  · push Not at hj
+    rw [glue_of_not e _ x hj, h j hj]
+
+/-- **Summing over the basis strings that agree with `x` off `e`** is summing over their bits on
+`e`. -/
+theorem sum_agreeOff [DecidableEq ι] {R : Type*} [AddCommMonoid R] (e : ι ↪ Fin N)
+    (x : Fin N → Bool) (H : (Fin N → Bool) → R) :
+    ∑ y, (if AgreeOff e y x then H y else 0) = ∑ z : ι → Bool, H (glue e z x) := by
+  rw [← sum_filter]
+  refine sum_nbij' (· ∘ e) (glue e · x) (fun _ _ => mem_univ _)
+    (fun z _ => mem_filter.mpr ⟨mem_univ _, agreeOff_glue e z x⟩)
+    (fun y hy => glue_comp_of_agreeOff (mem_filter.mp hy).2) (fun z _ => glue_comp e z x)
+    (fun y hy => by rw [glue_comp_of_agreeOff (mem_filter.mp hy).2])
+
+/-- Summing a function of the bits on `e` over the basis strings that agree with `x` off `e`. -/
+theorem sum_agreeOff_comp [DecidableEq ι] {R : Type*} [AddCommMonoid R]
+    (e : ι ↪ Fin N) (x : Fin N → Bool) (F : (ι → Bool) → R) :
+    ∑ y, (if AgreeOff e y x then F (y ∘ e) else 0) = ∑ z, F z := by
+  rw [sum_agreeOff e x fun y => F (y ∘ e)]
+  simp
+
+end Glue
+
+/-! ### Circuits on part of a register -/
+
+/-- The placed gate `g` on the qubits `e` of a larger register. -/
+def PlacedGate.mapWires (e : Fin m ↪ Fin N) (g : PlacedGate m) : PlacedGate N :=
+  ⟨g.arity, g.gate, g.wires.trans e⟩
+
+/-- **The entries of a gate on part of a register** are those of the gate on the qubits `e`, when
+the basis strings agree off `e`. -/
+theorem PlacedGate.matrix_mapWires (e : Fin m ↪ Fin N) (g : PlacedGate m) (y x : Fin N → Bool) :
+    ((g.mapWires e).matrix : Matrix _ _ ℂ) y x =
+      if AgreeOff e y x then (g.matrix : Matrix _ _ ℂ) (y ∘ e) (x ∘ e) else 0 := by
+  rw [matrix_apply, matrix_apply]
+  have hiff : (∀ j, (¬∃ i, (g.mapWires e).wires i = j) → y j = x j) ↔
+      AgreeOff e y x ∧ ∀ j, (¬∃ i, g.wires i = j) → (y ∘ e) j = (x ∘ e) j := by
+    constructor
+    · intro h
+      refine ⟨fun j hj => h j ?_, fun j hj => h (e j) ?_⟩
+      · rintro ⟨i, rfl⟩
+        exact hj _ rfl
+      · rintro ⟨i, hi⟩
+        exact hj ⟨i, e.injective hi⟩
+    · rintro ⟨h₁, h₂⟩ j hj
+      by_cases hj' : ∃ j', e j' = j
+      · obtain ⟨j', rfl⟩ := hj'
+        exact h₂ j' fun ⟨i, hi⟩ => hj ⟨i, by rw [← hi]; rfl⟩
+      · exact h₁ j fun i hi => hj' ⟨i, hi⟩
+  rw [if_congr hiff rfl rfl, ite_and]
+  rfl
+
+/-- A circuit maps the basis state `|x⟩` to its column `x`. -/
+theorem Circuit.eval_ket_apply (C : Circuit m) (x y : Fin m → Bool) :
+    (Circuit.eval C (ket x)).ofLp y = (Circuit.matrix C : Matrix _ _ ℂ) y x := by
+  simp [Circuit.eval, Matrix.mulVec, dotProduct]
+
+/-- A circuit on `m` qubits with a list of gate codes; the codes of a concatenation of lists. -/
+theorem Circuit.ofCodes_flatMap {β : Type*} (l : List β) (f : β → List GateCode) :
+    Circuit.ofCodes m (l.flatMap f) = l.flatMap fun b => Circuit.ofCodes m (f b) := by
+  induction l with
+  | nil => rfl
+  | cons b l ih => rw [List.flatMap_cons, List.flatMap_cons, Circuit.ofCodes_append, ih]
+
+/-- The circuit `C` on the qubits `e` of a larger register. -/
+def Circuit.mapWires (e : Fin m ↪ Fin N) (C : Circuit m) : Circuit N :=
+  C.map (PlacedGate.mapWires e)
+
+@[simp] theorem Circuit.mapWires_nil (e : Fin m ↪ Fin N) : Circuit.mapWires e [] = [] := rfl
+
+@[simp] theorem Circuit.mapWires_cons (e : Fin m ↪ Fin N) (g : PlacedGate m) (C : Circuit m) :
+    Circuit.mapWires e (g :: C) = g.mapWires e :: Circuit.mapWires e C := rfl
+
+/-- **The entries of a circuit on part of a register** are those of the circuit on the qubits `e`,
+when the basis strings agree off `e`. -/
+theorem Circuit.matrix_mapWires (e : Fin m ↪ Fin N) (C : Circuit m) (y x : Fin N → Bool) :
+    (Circuit.matrix (Circuit.mapWires e C) : Matrix _ _ ℂ) y x =
+      if AgreeOff e y x then (Circuit.matrix C : Matrix _ _ ℂ) (y ∘ e) (x ∘ e) else 0 := by
+  induction C generalizing y x with
+  | nil =>
+    simp only [mapWires_nil, matrix_nil, OneMemClass.coe_one, Matrix.one_apply]
+    by_cases hyx : y = x
+    · subst hyx
+      simp [AgreeOff.refl]
+    · rw [ite_eq_right hyx]
+      split_ifs with h h'
+      · exact absurd (by rw [← glue_comp_of_agreeOff h, h', glue_comp_of_agreeOff
+          (AgreeOff.refl e x)]) hyx
+      · rfl
+      · rfl
+  | cons g C ih =>
+    simp only [mapWires_cons, matrix_cons, Submonoid.coe_mul, Matrix.mul_apply, ih,
+      PlacedGate.matrix_mapWires, ite_mul, zero_mul, mul_ite, mul_zero]
+    split_ifs with hyx
+    · have hiff (z : Fin N → Bool) : AgreeOff e y z ↔ AgreeOff e z x :=
+        ⟨fun h => h.symm.trans hyx, fun h => hyx.trans h.symm⟩
+      simp only [hiff, ← ite_and, and_self]
+      exact sum_agreeOff_comp e x fun w => (Circuit.matrix C : Matrix _ _ ℂ) (y ∘ e) w *
+        (g.matrix : Matrix _ _ ℂ) w (x ∘ e)
+    · refine sum_eq_zero fun z _ => ?_
+      split_ifs with h₁ h₂ <;> first | rfl | exact absurd (h₂.trans h₁) hyx
+
+/-- **Copies of a circuit on disjoint parts of a register act independently**: an entry of the
+whole is the product of the entries of the copies, when the basis strings agree off all parts. -/
+theorem Circuit.matrix_flatMap_mapWires (C : Circuit m) (L : List (Fin m ↪ Fin N))
+    (hL : L.Pairwise fun e e' => ∀ i i', e i ≠ e' i') (y x : Fin N → Bool) :
+    (Circuit.matrix (L.flatMap (Circuit.mapWires · C)) : Matrix _ _ ℂ) y x =
+      if ∀ j, (∀ e ∈ L, ∀ i, e i ≠ j) → y j = x j then
+        (L.map fun e : Fin m ↪ Fin N => (Circuit.matrix C : Matrix _ _ ℂ) (y ∘ ⇑e) (x ∘ ⇑e)).prod
+      else 0 := by
+  induction L generalizing y x with
+  | nil =>
+    simp only [List.flatMap_nil, matrix_nil, OneMemClass.coe_one, Matrix.one_apply,
+      List.not_mem_nil, IsEmpty.forall_iff, implies_true, forall_const, List.map_nil,
+      List.prod_nil, funext_iff]
+  | cons e L ih =>
+    obtain ⟨he, hL⟩ := List.pairwise_cons.mp hL
+    rw [List.flatMap_cons, matrix_append, Submonoid.coe_mul, Matrix.mul_apply]
+    simp only [ih hL, matrix_mapWires, ite_mul, zero_mul, mul_ite, mul_zero, ← ite_and]
+    -- the only intermediate basis string is `y` on `e` and `x` elsewhere
+    set z₀ : Fin N → Bool := fun j => if ∃ i, e i = j then y j else x j
+    have hdisj (e' : Fin m ↪ Fin N) (he' : e' ∈ L) (i i' : Fin m) : e' i ≠ e i' :=
+      fun h => he e' he' i' i h.symm
+    rw [sum_eq_single z₀]
+    · have hz₀e : z₀ ∘ e = y ∘ e := funext fun i => ite_eq_left ⟨i, rfl⟩
+      have hz₀x : AgreeOff e z₀ x := fun j hj => ite_eq_right (by simpa using hj)
+      have hz₀L (e' : Fin m ↪ Fin N) (he' : e' ∈ L) : z₀ ∘ e' = x ∘ e' :=
+        funext fun i => ite_eq_right fun ⟨i', hi'⟩ => hdisj e' he' i i' hi'.symm
+      have hcond : (∀ j, (∀ e' ∈ L, ∀ i, e' i ≠ j) → y j = z₀ j) ↔
+          ∀ j, (∀ e' ∈ e :: L, ∀ i, e' i ≠ j) → y j = x j := by
+        constructor
+        · intro h j hj
+          have := h j fun e' he' => hj e' (List.mem_cons_of_mem _ he')
+          rwa [show z₀ j = x j from
+            ite_eq_right (by simpa using fun i => hj e (List.mem_cons_self ..) i)] at this
+        · intro h j hj
+          by_cases hj' : ∃ i, e i = j
+          · exact (ite_eq_left hj').symm
+          · rw [show z₀ j = x j from ite_eq_right hj']
+            refine h j fun e' he' => ?_
+            rcases List.mem_cons.mp he' with rfl | he'
+            · simpa using hj'
+            · exact hj e' he'
+      simp only [hz₀x, true_and, hcond, hz₀e, List.map_cons, List.prod_cons]
+      split_ifs
+      · rw [List.map_congr_left fun e' he' => by rw [hz₀L e' he'], mul_comm]
+      · rfl
+    · intro z _ hz
+      refine ite_eq_right fun ⟨h₁, h₂⟩ => hz (funext fun j => ?_)
+      by_cases hj : ∃ i, e i = j
+      · rw [show z₀ j = y j from ite_eq_left hj]
+        obtain ⟨i, rfl⟩ := hj
+        exact (h₂ (e i) fun e' he' i' => hdisj e' he' i' i).symm
+      · rw [show z₀ j = x j from ite_eq_right hj]
+        exact h₁ j (by simpa using hj)
+    · exact fun h => absurd (mem_univ _) h
+
+/-! ### Shifted gate codes -/
+
+/-- The gate code `g` with every qubit number increased by `o`. -/
+def GateCode.shift (o : ℕ) (g : GateCode) : GateCode := (g.1, g.2.1 + o, g.2.2.map (· + o))
+
+/-- The block of qubits `o, …, o + m - 1` of an `N`-qubit register. -/
+def blockEmb (o : ℕ) (h : o + m ≤ N) : Fin m ↪ Fin N :=
+  ⟨fun i => ⟨i + o, by omega⟩, fun i j hij => Fin.ext (by simpa using congrArg Fin.val hij)⟩
+
+@[simp] theorem blockEmb_apply_val (o : ℕ) (h : o + m ≤ N) (i : Fin m) :
+    (blockEmb o h i : ℕ) = i + o := rfl
+
+/-- **A shifted well-formed gate code denotes the gate on the shifted block.** -/
+theorem GateCode.toPlacedGate?_shift {o : ℕ} (h : o + m ≤ N) {g : GateCode}
+    (hg : WellFormed m g) :
+    toPlacedGate? N (g.shift o) = (toPlacedGate? m g).map (PlacedGate.mapWires (blockEmb o h)) := by
+  have key {k : ℕ} (U : Gate k) (A : Fin k ↪ Fin m) (A' : Fin k ↪ Fin N)
+      (hA : ∀ i, (A' i : ℕ) = A i + o) :
+      (⟨k, U, A'⟩ : PlacedGate N) = PlacedGate.mapWires (blockEmb o h) ⟨k, U, A⟩ := by
+    simp only [PlacedGate.mapWires, PlacedGate.mk.injEq, heq_eq_eq, true_and]
+    exact Function.Embedding.ext fun i => Fin.ext (hA i)
+  match g, hg with
+  | (true, t, []), hg =>
+    have ht : t < m := hg.1
+    simp only [shift, toPlacedGate?, ht, ↓reduceDIte, show t + o < N by omega, Option.map_some,
+      List.map_nil, Option.some.injEq]
+    exact key _ _ _ fun i => by fin_cases i; rfl
+  | (true, t, _ :: _), hg => exact absurd hg.2 (List.cons_ne_nil _ _)
+  | (false, t, []), hg =>
+    have ht : t < m := hg.2.2 t (List.mem_cons_self ..)
+    simp only [shift, toPlacedGate?, ht, ↓reduceDIte, show t + o < N by omega, Option.map_some,
+      List.map_nil, Option.some.injEq]
+    exact key _ _ _ fun i => by fin_cases i; rfl
+  | (false, t, [c]), hg =>
+    obtain ⟨-, hnd, hlt⟩ := hg
+    have ht : t < m := hlt t (by simp)
+    have hc : c < m := hlt c (by simp)
+    have hct : c ≠ t := by simp at hnd; omega
+    simp only [shift, toPlacedGate?, List.map_cons, List.map_nil,
+      dite_eq_left (show c < m ∧ t < m ∧ c ≠ t from ⟨hc, ht, hct⟩),
+      dite_eq_left (show c + o < N ∧ t + o < N ∧ c + o ≠ t + o by omega), Option.map_some,
+      Option.some.injEq]
+    exact key _ _ _ fun i => by fin_cases i <;> rfl
+  | (false, t, [c₁, c₂]), hg =>
+    obtain ⟨-, hnd, hlt⟩ := hg
+    have ht : t < m := hlt t (by simp)
+    have hc₁ : c₁ < m := hlt c₁ (by simp)
+    have hc₂ : c₂ < m := hlt c₂ (by simp)
+    simp only [List.nodup_cons, List.mem_cons, List.not_mem_nil, or_false, List.nodup_nil,
+      not_false_eq_true, and_true] at hnd
+    simp only [shift, toPlacedGate?, List.map_cons, List.map_nil,
+      dite_eq_left (show c₁ < m ∧ c₂ < m ∧ t < m ∧ c₁ ≠ c₂ ∧ c₁ ≠ t ∧ c₂ ≠ t by omega),
+      dite_eq_left (show c₁ + o < N ∧ c₂ + o < N ∧ t + o < N ∧ c₁ + o ≠ c₂ + o ∧ c₁ + o ≠ t + o ∧
+        c₂ + o ≠ t + o by omega), Option.map_some, Option.some.injEq]
+    exact key _ _ _ fun i => by fin_cases i <;> rfl
+  | (false, t, _ :: _ :: _ :: _), hg => exact absurd hg.1 (by simp)
+
+/-- A well-formed gate code, shifted by `o`, is well formed on a register of at least `o + m`
+qubits. -/
+theorem GateCode.WellFormed.shift {o : ℕ} (h : o + m ≤ N) {g : GateCode} (hg : WellFormed m g) :
+    WellFormed N (g.shift o) := by
+  obtain ⟨_ | _, t, cs⟩ := g
+  · obtain ⟨hlen, hnd, hlt⟩ := hg
+    refine ⟨by simpa [GateCode.shift] using hlen, ?_, ?_⟩
+    · simpa [GateCode.shift, List.map_cons] using
+        hnd.map (f := (· + o)) (fun a b hab => by simpa using hab)
+    · intro i hi
+      simp only [List.mem_cons, List.mem_map] at hi
+      rcases hi with rfl | ⟨c, hc, rfl⟩
+      · have := hlt t (List.mem_cons_self ..)
+        omega
+      · have := hlt c (List.mem_cons_of_mem _ hc)
+        omega
+  · obtain ⟨ht, rfl⟩ := hg
+    exact ⟨show t + o < N by omega, rfl⟩
+
+/-- **Shifted gate codes denote the circuit on a block**: shifting a well-formed circuit's qubit
+numbers by `o` runs it on the qubits `o, …, o + m - 1`. -/
+theorem Circuit.ofCodes_map_shift {o : ℕ} (h : o + m ≤ N) {gs : List GateCode}
+    (hgs : ∀ g ∈ gs, GateCode.WellFormed m g) :
+    Circuit.ofCodes N (gs.map (GateCode.shift o)) =
+      (Circuit.ofCodes m gs).mapWires (blockEmb o h) := by
+  simp only [ofCodes, mapWires, List.filterMap_map, List.map_filterMap]
+  exact List.filterMap_congr fun g hg => GateCode.toPlacedGate?_shift h (hgs g hg)
+
+end Cslib.Quantum
diff --git a/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean
new file mode 100644
index 000000000..ba8badb39
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean
@@ -0,0 +1,618 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.BQP
+public import Complexity.Computability.Circuit.Quantum.Counter
+public import Complexity.Computability.Circuit.Quantum.Parallel
+import Complexity.Foundations.Combinatorics.MajorityVote.Weighted
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+
+/-!
+# Error reduction for `BQP`
+
+The error `1 / 3` in the definition of `BQP` (`Cslib.Complexity.BQP`) can be made exponentially
+small: `A ∈ BQP enc` exactly when for every polynomial `q` some uniform family accepts members with
+probability at least `1 - 2^{-q(n)}` and other instances with probability at most `2^{-q(n)}`, where
+`n` is the length of the encoded instance (`Cslib.Complexity.mem_BQP_iff_forall_errorExponent`).
+
+This is the majority-vote error reduction of `BPP`
+(`Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent`), carried out inside a quantum
+circuit, since acceptance is the measurement of a single qubit at the end. The amplified family
+(`Cslib.Quantum.UniformCircuitFamily.amplify`) runs `2 r` copies of the circuit side by side and
+takes a reversible majority vote of their answers. On inputs of length `n` its register holds the
+input, `2 r` blocks of the original width `w`, and the ancillas of a threshold counter:
+
+1. CNOT gates copy the input into each block (`Cslib.Quantum.Amplify.copyCodes`);
+2. each block runs the original circuit, with its qubit numbers shifted
+   (`Cslib.Quantum.Amplify.copiesCodes`);
+3. a reversible counter computes whether more than `r` of the blocks' first qubits are one
+   (`Cslib.Quantum.Counter.codes`);
+4. three CNOT gates swap that answer into qubit `0` (`Cslib.Quantum.GateCode.swapCodes`).
+
+The copies act on disjoint blocks, so their measurement outcomes are independent
+(`Cslib.Quantum.Circuit.matrix_flatMap_mapWires`), and the classical steps permute the outcomes. The
+acceptance probability of the amplified family is therefore the probability that a strict majority
+of `2 r` independent trials succeed, each with the original acceptance probability
+(`Cslib.Quantum.UniformCircuitFamily.acceptProb_amplify`). The exponential-moment bound
+`Cslib.sum_prod_le_of_card_filter_le` makes the error at most `(8 / 9) ^ r`, and `r = 6 q` gives
+`2^{-q}`.
+
+## Main definitions
+
+* `Cslib.Quantum.Amplify.codes`, `Cslib.Quantum.Amplify.width`: the amplified circuit.
+* `Cslib.Quantum.UniformCircuitFamily.amplify`: the amplified family.
+
+## Main results
+
+* `Cslib.Quantum.UniformCircuitFamily.acceptProb_amplify`: the acceptance probability of the
+  amplified family is that of a strict majority of independent copies.
+* `Cslib.Complexity.mem_BQP_iff_forall_errorExponent`: error reduction for `BQP`.
+
+The argument is the standard one; no source locator is claimed for it. `BQP` itself follows
+[Bernstein, Vazirani][BernsteinVazirani1997] and [Arora, Barak][AroraBarak09] (see
+`Cslib.Complexity.BQP`).
+
+## References
+
+* [E. Bernstein, U. Vazirani, *Quantum complexity theory*][BernsteinVazirani1997]
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum
+
+open Finset GateCode Turing.MultiTapeTM
+
+namespace Amplify
+
+/-- CNOT gates copying the first `n` qubits into the blocks `1, …, k` of width `w`. -/
+def copyCodes (n w k : ℕ) : List GateCode :=
+  (List.range k).flatMap fun j => (List.range n).map fun i => (false, i + (j + 1) * w, [i])
+
+/-- The circuit `gs` on each of the blocks `1, …, k` of width `w`. -/
+def copiesCodes (w k : ℕ) (gs : List GateCode) : List GateCode :=
+  (List.range k).flatMap fun j => gs.map (shift ((j + 1) * w))
+
+/-- The first ancilla of the counter, after the input block and `2 r` copies of width `w`. -/
+def base (w r : ℕ) : ℕ := (2 * r + 1) * w
+
+/-- The register width of the amplified circuit: the blocks and the counter's ancillas. -/
+def width (w r : ℕ) : ℕ := base w r + 1 + (2 * r + 1) * (r + 1)
+
+/-- The counter's qubit that reads whether more than `r` of the `2 r` copies accept. -/
+def answer (w r : ℕ) : ℕ := Counter.level (base w r) (r + 1) (2 * r) r
+
+/-- **The amplified circuit**: copy the input of length `n` into `2 r` blocks of width `w`, run
+the circuit `gs` on each, count the blocks whose first qubit is one, and swap the strict majority
+into qubit `0`. -/
+def codes (n w r : ℕ) (gs : List GateCode) : List GateCode :=
+  copyCodes n w (2 * r) ++ (copiesCodes w (2 * r) gs ++
+    (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ swapCodes (answer w r)))
+
+variable {n w r : ℕ}
+
+theorem base_eq (w r : ℕ) : base w r = 2 * r * w + w := by
+  unfold base
+  rw [Nat.add_mul, Nat.one_mul]
+
+theorem block_lt {j i : ℕ} (hj : j < 2 * r) (hi : i < w) :
+    i + (j + 1) * w < base w r := by
+  have := Nat.mul_le_mul_right w (show j + 1 ≤ 2 * r by omega)
+  rw [base_eq]
+  omega
+
+theorem base_lt_width : base w r < width w r := by
+  unfold width
+  omega
+
+theorem answer_lt_width : answer w r < width w r := by
+  unfold answer width Counter.level
+  have : 2 * r * (r + 1) + r < (2 * r + 1) * (r + 1) := by
+    rw [Nat.add_mul (2 * r), Nat.one_mul]
+    omega
+  omega
+
+theorem base_le_answer : base w r ≤ answer w r := by
+  unfold answer Counter.level
+  omega
+
+/-- The blocks `1, …, 2 r` of the amplified register. -/
+def blocks (w r : ℕ) : Fin (2 * r) × Fin w ↪ Fin (width w r) where
+  toFun p := ⟨p.2 + (p.1 + 1) * w, (block_lt p.1.2 p.2.2).trans base_lt_width⟩
+  inj' p p' h := by
+    have h' : (p.2 : ℕ) + (p.1 + 1) * w = p'.2 + (p'.1 + 1) * w := congrArg Fin.val h
+    have hw : 0 < w := Nat.lt_of_le_of_lt (Nat.zero_le _) p.2.2
+    have hmod := congrArg (· % w) h'
+    have hdiv := congrArg (· / w) h'
+    simp only [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt p.2.2,
+      Nat.mod_eq_of_lt p'.2.2] at hmod
+    simp only [Nat.add_mul_div_right _ _ hw, Nat.div_eq_of_lt p.2.2,
+      Nat.div_eq_of_lt p'.2.2] at hdiv
+    exact Prod.ext (Fin.ext (by omega)) (Fin.ext hmod)
+
+@[simp] theorem blocks_apply_val (p : Fin (2 * r) × Fin w) :
+    (blocks w r p : ℕ) = p.2 + (p.1 + 1) * w := rfl
+
+theorem block_le_width {j : ℕ} (hj : j < 2 * r) : (j + 1) * w + w ≤ width w r := by
+  have := Nat.mul_le_mul_right w (show j + 1 ≤ 2 * r by omega)
+  have : base w r < width w r := base_lt_width
+  rw [base_eq] at this
+  omega
+
+/-- Block `j` of the amplified register. -/
+def block (j : Fin (2 * r)) : Fin w ↪ Fin (width w r) :=
+  blockEmb ((j + 1) * w) (block_le_width j.2)
+
+theorem block_apply (j : Fin (2 * r)) (i : Fin w) : block j i = blocks w r (j, i) := rfl
+
+/-! ### The classical steps -/
+
+theorem isClassical_copyCodes (hn : n ≤ w) (hw : 0 < w) :
+    IsClassical (width w r) (copyCodes n w (2 * r)) := by
+  refine IsClassical.flatMap fun j hj => fun g hg => ?_
+  obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hg
+  have hj : j < 2 * r := List.mem_range.mp hj
+  have hi : i < n := List.mem_range.mp hi
+  have hlt := (block_lt (r := r) hj (show i < w by omega)).trans base_lt_width
+  have : 0 < (j + 1) * w := Nat.mul_pos (by omega) hw
+  refine ⟨rfl, by simp, ?_, ?_⟩
+  · simp only [List.nodup_cons, List.mem_cons, List.not_mem_nil, or_false, List.nodup_nil,
+      not_false_eq_true, and_true]
+    omega
+  · simp only [List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq]
+    omega
+
+/-- **The copy step puts the input in every block**, and leaves the other qubits unchanged. -/
+theorem readBit_classicalRun_copyCodes (hn : n ≤ w) (hw : 0 < w) (X : Fin (width w r) → Bool)
+    (hX : ∀ p, n ≤ p → readBit X p = false) (p : ℕ) :
+    readBit (classicalRun (copyCodes n w (2 * r)) X) p =
+      if ∃ j < 2 * r, ∃ i < w, p = i + (j + 1) * w then readBit X (p % w) else readBit X p := by
+  have hread : ∀ g ∈ copyCodes n w (2 * r), ∀ g' ∈ copyCodes n w (2 * r), g.2.1 ∉ g'.2.2 := by
+    intro g hg g' hg'
+    simp only [copyCodes, List.mem_flatMap, List.mem_map, List.mem_range] at hg hg'
+    obtain ⟨j, hj, i, hi, rfl⟩ := hg
+    obtain ⟨j', hj', i', hi', rfl⟩ := hg'
+    have : w ≤ (j + 1) * w := Nat.le_mul_of_pos_left w (by omega)
+    simp only [List.mem_cons, List.not_mem_nil, or_false]
+    omega
+  rw [readBit_classicalRun_of_forall_notMem (isClassical_copyCodes hn hw) hread, copyCodes,
+    List.foldl_flatMap]
+  -- each block contributes the exclusive or of its copies of the input bits
+  have hinner (b : Bool) (j : ℕ) :
+      ((List.range n).map fun i => ((false, i + (j + 1) * w, [i]) : GateCode)).foldl
+        (fun b g => b ^^ (decide (p = g.2.1) && g.2.2.all (readBit X))) b =
+      (b ^^ (decide (∃ i < n, p = i + (j + 1) * w) && readBit X (p % w))) := by
+    rw [List.foldl_map]
+    by_cases hp : ∃ i < n, p = i + (j + 1) * w
+    · obtain ⟨i₀, hi₀, rfl⟩ := hp
+      rw [foldl_xor_range n i₀ _ _ fun i _ hne => by simp [Ne.symm hne]]
+      simp [hi₀, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (show i₀ < w by omega)]
+    · have hp' : ∀ i < n, p ≠ i + (j + 1) * w := fun i hi h => hp ⟨i, hi, h⟩
+      rw [foldl_xor_range n n _ _ fun i hi _ => by simp [hp' i hi]]
+      simp [hp]
+  simp only [hinner]
+  by_cases hp : ∃ j < 2 * r, ∃ i < w, p = i + (j + 1) * w
+  · obtain ⟨j₀, hj₀, i₀, hi₀, rfl⟩ := hp
+    rw [ite_eq_left ⟨j₀, hj₀, i₀, hi₀, rfl⟩, foldl_xor_range (2 * r) j₀ _ _ fun j _ hne => ?_]
+    · have hw' : w ≤ (j₀ + 1) * w := Nat.le_mul_of_pos_left w (by omega)
+      rw [hX _ (by omega), Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hi₀]
+      by_cases hi : i₀ < n
+      · simp [hj₀, hi]
+      · simp [hj₀, hi, hX i₀ (by omega)]
+    · simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not]
+      left
+      rintro ⟨i, hi, h⟩
+      have hmod := congrArg (· / w) h
+      simp only [Nat.add_mul_div_right _ _ hw, Nat.div_eq_of_lt hi₀,
+        Nat.div_eq_of_lt (show i < w by omega)] at hmod
+      omega
+  · rw [ite_eq_right hp, foldl_xor_range (2 * r) (2 * r) _ _ fun j hj _ => ?_]
+    · simp
+    · simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not]
+      exact Or.inl fun ⟨i, hi, h⟩ => hp ⟨j, hj, i, by omega, h⟩
+
+theorem isClassical_counter_swap (hw : 0 < w) :
+    IsClassical (width w r) (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++
+      swapCodes (answer w r)) := by
+  refine IsClassical.append.mpr ⟨Counter.isClassical_codes (fun s hs => ?_) le_rfl,
+    isClassical_swapCodes ?_ answer_lt_width⟩
+  · have := block_lt (r := r) hs hw
+    omega
+  · have : 0 < base w r := Nat.mul_pos (by omega) hw
+    have := base_le_answer (w := w) (r := r)
+    omega
+
+/-- **The classical steps accept by strict majority**: on a register whose qubits from the counter
+on are zero, the counter and the swap leave in qubit `0` whether more than `r` of the blocks' first
+qubits are one. -/
+theorem readBit_classicalRun_counter_swap (hw : 0 < w) (Y : Fin (width w r) → Bool)
+    (hY : ∀ p, base w r ≤ p → readBit Y p = false) :
+    readBit (classicalRun (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++
+      swapCodes (answer w r)) Y) 0 =
+      decide (r < Counter.count Y (fun s => (s + 1) * w) (2 * r)) := by
+  rw [classicalRun_append, readBit_classicalRun_swapCodes _ answer_lt_width]
+  · exact (Counter.readBit_classicalRun_codes (fun s hs => by
+      have := block_lt (r := r) hs hw; omega) le_rfl Y hY).2 r (by omega)
+  · have : 0 < base w r := Nat.mul_pos (by omega) hw
+    have := base_le_answer (w := w) (r := r)
+    omega
+
+/-! ### The parallel copies -/
+
+theorem ofCodes_copiesCodes {gs : List GateCode} (hgs : ∀ g ∈ gs, WellFormed w g) :
+    Circuit.ofCodes (width w r) (copiesCodes w (2 * r) gs) =
+      ((List.finRange (2 * r)).map block).flatMap (Circuit.mapWires · (Circuit.ofCodes w gs)) := by
+  rw [copiesCodes, Circuit.ofCodes_flatMap, ← List.map_coe_finRange_eq_range, List.flatMap_map,
+    List.flatMap_map]
+  congr 1
+  funext j
+  exact Circuit.ofCodes_map_shift _ hgs
+
+theorem pairwise_block :
+    ((List.finRange (2 * r)).map (block (w := w))).Pairwise fun e e' => ∀ i i', e i ≠ e' i' := by
+  rw [List.pairwise_map]
+  refine (List.nodup_finRange _).imp fun {j j'} hjj' i i' h => hjj' ?_
+  rw [block_apply, block_apply] at h
+  exact congrArg Prod.fst ((blocks w r).injective h)
+
+end Amplify
+
+/-! ### Acceptance probability of the amplified circuit -/
+
+/-- Grouping a sum over tuples by a function of their entries. -/
+private theorem sum_mul_prod_fiberwise {α κ R : Type*} [Fintype α] [Fintype κ] [DecidableEq κ]
+    [CommSemiring R] {k : ℕ} (φ : α → κ) (f : α → R) (G : (Fin k → κ) → R) :
+    ∑ y : Fin k → α, G (fun j => φ (y j)) * ∏ j, f (y j) =
+      ∑ b : Fin k → κ, G b * ∏ j, ∑ z ∈ univ.filter (fun z => φ z = b j), f z := by
+  simp_rw [prod_univ_sum, mul_sum]
+  rw [← sum_fiberwise univ (fun y : Fin k → α => fun j => φ (y j))]
+  refine sum_congr rfl fun b _ => ?_
+  have hset : Fintype.piFinset (fun j => univ.filter fun z => φ z = b j) =
+      univ.filter fun y : Fin k → α => (fun j => φ (y j)) = b := by
+    ext y
+    simp [Fintype.mem_piFinset, funext_iff]
+  rw [hset]
+  refine sum_congr rfl fun y hy => ?_
+  rw [(mem_filter.mp hy).2]
+
+open Amplify in
+/-- **The acceptance probability of the amplified circuit** is the probability that more than `r`
+of `2 r` independent runs of the original circuit accept. -/
+theorem acceptProb_amplify_codes {n w r : ℕ} {gs : List GateCode} (hw : 0 < w) (hn : n ≤ w)
+    (hgs : ∀ g ∈ gs, WellFormed w g) (x : List Bool) (hx : x.length = n) :
+    acceptProb (width w r) (codes n w r gs) x =
+      ∑ b : Fin (2 * r) → Bool with r < (univ.filter fun j => b j = true).card,
+        ∏ j, if b j then acceptProb w gs x else 1 - acceptProb w gs x := by
+  set N := width w r
+  set C := Circuit.ofCodes w gs
+  set a : (Fin w → Bool) → ℂ := fun z => (Circuit.run C (inputState w x)).ofLp z
+  set X := classicalRun (copyCodes n w (2 * r)) (inputState N x) with hXdef
+  have hgetD (p : ℕ) (hp : n ≤ p) : x.getD p false = false := by
+    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)]
+    rfl
+  have hX₀ (p : ℕ) : readBit (inputState N x) p = x.getD p false := by
+    by_cases hp : p < N
+    · rw [readBit_of_lt _ hp]
+      rfl
+    · rw [readBit_of_le _ (not_lt.mp hp), hgetD]
+      have := (base_lt_width (w := w) (r := r))
+      have : w ≤ base w r := by unfold base; exact Nat.le_mul_of_pos_left w (by omega)
+      omega
+  have hXbit (p : ℕ) := readBit_classicalRun_copyCodes (r := r) hn hw (inputState N x)
+    (fun p hp => by rw [hX₀, hgetD p hp]) p
+  -- the copy step puts the input in every block and keeps zeros from the counter on
+  have hXblock (j : Fin (2 * r)) : X ∘ block j = inputState w x := by
+    funext i
+    have h := hXbit (i + (j + 1) * w)
+    rw [ite_eq_left ⟨j, j.2, i, i.2, rfl⟩, Nat.add_mul_mod_self_right,
+      Nat.mod_eq_of_lt i.2, hX₀] at h
+    rw [Function.comp_apply, show X (block j i) = readBit X (block j i) from
+      (readBit_fin _ _).symm, block_apply, blocks_apply_val, h]
+    rfl
+  have hXhigh (p : ℕ) (hp : base w r ≤ p) : readBit X p = false := by
+    rw [hXbit, ite_eq_right, hX₀, hgetD]
+    · have : w ≤ base w r := by unfold base; exact Nat.le_mul_of_pos_left w (by omega)
+      omega
+    · rintro ⟨j, hj, i, hi, rfl⟩
+      exact absurd hp (not_le.mpr (block_lt hj hi))
+  -- the amplitudes of the copies are products
+  have hamp (Y : Fin N → Bool) :
+      (Circuit.eval (Circuit.ofCodes N (copiesCodes w (2 * r) gs)) (ket X)).ofLp Y =
+        if AgreeOff (blocks w r) Y X then ∏ j, a (Y ∘ block j) else 0 := by
+    rw [Circuit.eval_ket_apply, ofCodes_copiesCodes hgs,
+      Circuit.matrix_flatMap_mapWires _ _ pairwise_block]
+    have hcond : (∀ p, (∀ e ∈ (List.finRange (2 * r)).map block, ∀ i, e i ≠ p) → Y p = X p) ↔
+        AgreeOff (blocks w r) Y X := by
+      simp only [List.mem_map, List.mem_finRange, true_and, forall_exists_index,
+        forall_apply_eq_imp_iff, AgreeOff, Prod.forall, block_apply]
+    rw [if_congr hcond rfl rfl, List.map_map, ← Fin.prod_univ_def]
+    refine if_congr Iff.rfl (prod_congr rfl fun j _ => ?_) rfl
+    simp only [Function.comp_apply, hXblock, a, Circuit.run, Circuit.eval_ket_apply]
+    rfl
+  -- the acceptance probability as a sum over the blocks' outcomes
+  unfold acceptProb
+  rw [codes, Circuit.ofCodes_append, Circuit.ofCodes_append, Circuit.run, Circuit.eval_append,
+    Circuit.eval_append, Circuit.eval_ofCodes_ket (isClassical_copyCodes hn hw),
+    Circuit.measureProb_eval_ofCodes (isClassical_counter_swap hw), ← hXdef]
+  simp only [hamp]
+  have hterm (Y : Fin N → Bool) :
+      (if classicalRun (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++
+          swapCodes (answer w r)) Y ∈ accepting N then
+        ‖(if AgreeOff (blocks w r) Y X then ∏ j, a (Y ∘ block j) else 0)‖ ^ 2 else 0) =
+      if AgreeOff (blocks w r) Y X then
+        (if r < (univ.filter fun j : Fin (2 * r) => (Y ∘ blocks w r) (j, ⟨0, hw⟩) = true).card
+          then (1 : ℝ) else 0) * ∏ j, ‖a (fun i => (Y ∘ blocks w r) (j, i))‖ ^ 2
+      else 0 := by
+    by_cases hY : AgreeOff (blocks w r) Y X
+    · have hYhigh (p : ℕ) (hp : base w r ≤ p) : readBit Y p = false := by
+        rw [← hXhigh p hp]
+        by_cases hpN : p < N
+        · rw [readBit_of_lt _ hpN, readBit_of_lt _ hpN]
+          refine hY _ fun q h => ?_
+          have := congrArg Fin.val h
+          simp only [blocks_apply_val] at this
+          exact absurd hp (not_le.mpr (this ▸ block_lt q.1.2 q.2.2))
+        · rw [readBit_of_le _ (not_lt.mp hpN), readBit_of_le _ (not_lt.mp hpN)]
+      have hbit (j : Fin (2 * r)) : readBit Y ((j + 1) * w) = (Y ∘ blocks w r) (j, ⟨0, hw⟩) := by
+        rw [Function.comp_apply, ← readBit_fin Y (blocks w r (j, ⟨0, hw⟩)), blocks_apply_val]
+        simp only [Nat.zero_add]
+      have hcount : Counter.count Y (fun s => (s + 1) * w) (2 * r) =
+          (univ.filter fun j : Fin (2 * r) => (Y ∘ blocks w r) (j, ⟨0, hw⟩) = true).card := by
+        unfold Counter.count
+        rw [← card_map Fin.valEmbedding]
+        congr 1
+        ext s
+        simp only [mem_filter, mem_range, mem_map, mem_univ, true_and, Fin.valEmbedding_apply,
+          Function.comp_apply]
+        constructor
+        · rintro ⟨hs, h⟩
+          exact ⟨⟨s, hs⟩, (hbit ⟨s, hs⟩).symm.trans h, rfl⟩
+        · rintro ⟨j, h, rfl⟩
+          exact ⟨j.2, (hbit j).trans h⟩
+      have hacc : (classicalRun (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++
+          swapCodes (answer w r)) Y ∈ accepting N) ↔
+          r < (univ.filter fun j : Fin (2 * r) => (Y ∘ blocks w r) (j, ⟨0, hw⟩) = true).card := by
+        have h0 : 0 < N := by have := base_lt_width (w := w) (r := r); omega
+        rw [mem_accepting h0, ← readBit_fin (classicalRun _ Y) (⟨0, h0⟩ : Fin N)]
+        change readBit _ 0 = true ↔ _
+        rw [readBit_classicalRun_counter_swap hw Y hYhigh, hcount, decide_eq_true_iff]
+      simp only [hY, ite_true, hacc, norm_prod, ← prod_pow]
+      split_ifs <;> simp [block_apply, Function.comp_def]
+    · simp [hY]
+  simp only [hterm]
+  rw [sum_agreeOff_comp (blocks w r) X fun z =>
+    (if r < (univ.filter fun j : Fin (2 * r) => z (j, ⟨0, hw⟩) = true).card then (1 : ℝ) else 0) *
+      ∏ j, ‖a (fun i => z (j, i))‖ ^ 2]
+  rw [Fintype.sum_equiv (Equiv.curry (Fin (2 * r)) (Fin w) Bool) (fun z =>
+    (if r < (univ.filter fun j => z (j, ⟨0, hw⟩) = true).card then (1 : ℝ) else 0) *
+      ∏ j, ‖a (fun i => z (j, i))‖ ^ 2) (fun y =>
+    (if r < (univ.filter fun j => y j ⟨0, hw⟩ = true).card then (1 : ℝ) else 0) *
+      ∏ j, ‖a (y j)‖ ^ 2) fun z => rfl]
+  refine (sum_mul_prod_fiberwise (fun z : Fin w → Bool => z ⟨0, hw⟩) (fun z => ‖a z‖ ^ 2)
+    fun b => if r < (univ.filter fun j => b j = true).card then (1 : ℝ) else 0).trans ?_
+  -- the outcome probabilities of one copy
+  have hone : ∑ z, ‖a z‖ ^ 2 = 1 := by
+    rw [← measureProb, measureProb_univ, Circuit.norm_run, one_pow]
+  have htrue : ∑ z ∈ univ.filter (fun z : Fin w → Bool => z ⟨0, hw⟩ = true), ‖a z‖ ^ 2 =
+      acceptProb w gs x := by
+    unfold acceptProb measureProb
+    congr 1
+    ext z
+    simp [mem_accepting hw]
+  have hfalse : ∑ z ∈ univ.filter (fun z : Fin w → Bool => z ⟨0, hw⟩ = false), ‖a z‖ ^ 2 =
+      1 - acceptProb w gs x := by
+    rw [← hone, ← htrue, ← sum_filter_add_sum_filter_not univ (fun z : Fin w → Bool =>
+      z ⟨0, hw⟩ = true)]
+    simp
+  rw [sum_filter]
+  refine sum_congr rfl fun b _ => ?_
+  rw [ite_mul, one_mul, zero_mul]
+  refine if_congr Iff.rfl (prod_congr rfl fun j _ => ?_) rfl
+  cases b j
+  · exact hfalse
+  · exact htrue
+
+namespace Amplify
+
+/-! ### The amplified circuit is constructed in polynomial time -/
+
+variable {γ : Type} {enc : γ ↪ List Bool}
+
+theorem computableInPolyTime_copyCodes {n w k : γ → ℕ}
+    (hn : ComputableInPolyTime n enc encUnary) (hw : ComputableInPolyTime w enc encUnary)
+    (hk : ComputableInPolyTime k enc encUnary) :
+    ComputableInPolyTime (fun c => copyCodes (n c) (w c) (k c)) enc (encList encGateCode) := by
+  unfold copyCodes
+  fun_prop
+
+theorem computableInPolyTime_copiesCodes {w k : γ → ℕ} {gs : γ → List GateCode}
+    (hw : ComputableInPolyTime w enc encUnary) (hk : ComputableInPolyTime k enc encUnary)
+    (hgs : ComputableInPolyTime gs enc (encList encGateCode)) :
+    ComputableInPolyTime (fun c => copiesCodes (w c) (k c) (gs c)) enc (encList encGateCode) := by
+  have hshift (o : ℕ) : shift o = fun g => (g.1, g.2.1 + o, g.2.2.map (· + o)) := rfl
+  simp only [copiesCodes, hshift]
+  fun_prop
+
+theorem computableInPolyTime_stage {base T b s : γ → ℕ}
+    (hbase : ComputableInPolyTime base enc encUnary) (hT : ComputableInPolyTime T enc encUnary)
+    (hb : ComputableInPolyTime b enc encUnary) (hs : ComputableInPolyTime s enc encUnary) :
+    ComputableInPolyTime (fun c => Counter.stage (base c) (T c) (b c) (s c)) enc
+      (encList encGateCode) := by
+  simp only [Counter.stage, Counter.level, Counter.below]
+  fun_prop
+
+theorem computableInPolyTime_counter {w r : γ → ℕ}
+    (hw : ComputableInPolyTime w enc encUnary) (hr : ComputableInPolyTime r enc encUnary) :
+    ComputableInPolyTime (fun c => Counter.codes (base (w c) (r c)) (r c + 1)
+      (fun s => (s + 1) * w c) (2 * r c)) enc (encList encGateCode) := by
+  have hstage := computableInPolyTime_stage (enc := encPair enc encUnary)
+    (base := fun p => base (w p.1) (r p.1)) (T := fun p => r p.1 + 1)
+    (b := fun p => (p.2 + 1) * w p.1) (s := fun p => p.2)
+    (by unfold base; fun_prop) (by fun_prop) (by fun_prop) (by fun_prop)
+  have hbase : ComputableInPolyTime (fun c => base (w c) (r c)) enc encUnary := by
+    unfold base
+    fun_prop
+  unfold Counter.codes
+  fun_prop
+
+theorem computableInPolyTime_codes {n w r : γ → ℕ} {gs : γ → List GateCode}
+    (hn : ComputableInPolyTime n enc encUnary) (hw : ComputableInPolyTime w enc encUnary)
+    (hr : ComputableInPolyTime r enc encUnary)
+    (hgs : ComputableInPolyTime gs enc (encList encGateCode)) :
+    ComputableInPolyTime (fun c => codes (n c) (w c) (r c) (gs c)) enc (encList encGateCode) := by
+  have h₁ := computableInPolyTime_copyCodes hn hw (k := fun c => 2 * r c) (by fun_prop)
+  have h₂ := computableInPolyTime_copiesCodes hw (k := fun c => 2 * r c) (by fun_prop) hgs
+  have h₃ := computableInPolyTime_counter hw hr
+  have h₄ : ComputableInPolyTime (fun c => swapCodes (answer (w c) (r c))) enc
+      (encList encGateCode) := by
+    simp only [swapCodes, answer, Counter.level, base]
+    fun_prop
+  unfold codes
+  fun_prop
+
+end Amplify
+
+namespace UniformCircuitFamily
+
+open Amplify
+
+/-- **The amplified family**: on inputs of length `n`, `2 r(n)` copies of the family's circuit run
+side by side, and a reversible majority vote of their answers is measured. -/
+def amplify (F : UniformCircuitFamily) (r : ℕ → ℕ)
+    (hr : ComputableInPolyTime r encUnary encUnary) : UniformCircuitFamily where
+  width n := Amplify.width (F.width n) (r n)
+  gates n := codes n (F.width n) (r n) (F.gates n)
+  computableInPolyTime_width := by
+    have := F.computableInPolyTime_width
+    simp only [Amplify.width, base]
+    fun_prop
+  computableInPolyTime_gates :=
+    computableInPolyTime_codes (by fun_prop) F.computableInPolyTime_width hr
+      F.computableInPolyTime_gates
+  le_width n := by
+    have := F.le_width n
+    have : F.width n ≤ base (F.width n) (r n) := Nat.le_mul_of_pos_left _ (by omega)
+    have := base_lt_width (w := F.width n) (r := r n)
+    omega
+  width_pos n := Nat.lt_of_le_of_lt (Nat.zero_le _) base_lt_width
+  wellFormed n g hg := by
+    have hw := F.width_pos n
+    rcases List.mem_append.mp hg with hg | hg
+    · exact (isClassical_copyCodes (F.le_width n) hw g hg).2
+    rcases List.mem_append.mp hg with hg | hg
+    · obtain ⟨j, hj, hg⟩ := List.mem_flatMap.mp hg
+      obtain ⟨g, hg', rfl⟩ := List.mem_map.mp hg
+      exact (F.wellFormed n g hg').shift (block_le_width (List.mem_range.mp hj))
+    · exact (isClassical_counter_swap hw g hg).2
+
+/-- **The acceptance probability of the amplified family** is the probability that more than
+`r(n)` of `2 r(n)` independent runs of the family accept, on inputs of length `n`. -/
+theorem acceptProb_amplify (F : UniformCircuitFamily) {r : ℕ → ℕ}
+    (hr : ComputableInPolyTime r encUnary encUnary) (x : List Bool) :
+    (F.amplify r hr).acceptProb x =
+      ∑ b : Fin (2 * r x.length) → Bool with r x.length < (univ.filter fun j => b j = true).card,
+        ∏ j, if b j then F.acceptProb x else 1 - F.acceptProb x :=
+  acceptProb_amplify_codes (F.width_pos _) (F.le_width _) (F.wellFormed _) x rfl
+
+/-- The trials of the majority vote: success with probability `p`. -/
+private theorem sum_bernoulli (p : ℝ) : ∑ c : Bool, (if c then p else 1 - p) = 1 := by
+  simp
+
+/-- **Amplifying acceptance**: a family accepting with probability at least `2 / 3` gives a family
+accepting with probability at least `1 - (8 / 9) ^ r(n)`. -/
+theorem one_sub_le_acceptProb_amplify (F : UniformCircuitFamily) {r : ℕ → ℕ}
+    (hr : ComputableInPolyTime r encUnary encUnary) {x : List Bool}
+    (hx : 2 / 3 ≤ F.acceptProb x) :
+    1 - (8 / 9) ^ r x.length ≤ (F.amplify r hr).acceptProb x := by
+  set p := F.acceptProb x
+  set R := r x.length
+  have hq : ∀ c : Bool, 0 ≤ if c then p else 1 - p := fun c => by
+    have := F.acceptProb_le_one x
+    cases c <;> simp <;> linarith
+  have hbad := sum_prod_le_of_card_filter_le (fun c : Bool => if c then p else 1 - p) hq
+    (sum_bernoulli p) {true} (by simpa using (by linarith : (2 : ℝ) ≤ 3 * p)) R
+  simp only [mem_singleton] at hbad
+  have htotal := (Fintype.sum_pow (fun c : Bool => if c then p else 1 - p) (2 * R)).symm
+  rw [sum_bernoulli, one_pow, ← sum_filter_add_sum_filter_not univ
+    (fun b : Fin (2 * R) → Bool => R < (univ.filter fun j => b j = true).card)] at htotal
+  simp only [not_lt] at htotal
+  rw [acceptProb_amplify]
+  linarith
+
+/-- **Amplifying rejection**: a family accepting with probability at most `1 / 3` gives a family
+accepting with probability at most `(8 / 9) ^ r(n)`. -/
+theorem acceptProb_amplify_le (F : UniformCircuitFamily) {r : ℕ → ℕ}
+    (hr : ComputableInPolyTime r encUnary encUnary) {x : List Bool}
+    (hx : F.acceptProb x ≤ 1 / 3) :
+    (F.amplify r hr).acceptProb x ≤ (8 / 9) ^ r x.length := by
+  set p := F.acceptProb x
+  have hq : ∀ c : Bool, 0 ≤ if c then p else 1 - p := fun c => by
+    have := F.acceptProb_nonneg x
+    cases c <;> simp <;> linarith
+  have hbad := sum_prod_le_of_card_filter_le (fun c : Bool => if c then p else 1 - p) hq
+    (sum_bernoulli p) {false} (by simpa using (by linarith : (2 : ℝ) ≤ 3 * (1 - p))) (r x.length)
+  simp only [mem_singleton] at hbad
+  rw [acceptProb_amplify]
+  refine le_trans (sum_le_sum_of_subset_of_nonneg (fun b hb => ?_)
+    fun b _ _ => prod_nonneg fun j _ => hq _) hbad
+  rw [mem_filter] at hb ⊢
+  refine ⟨mem_univ _, ?_⟩
+  have := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * r x.length))))
+    (fun j => b j = true)
+  have e : (univ.filter fun j => ¬b j = true) = univ.filter fun j => b j = false := by
+    ext j
+    simp
+  rw [e, card_univ, Fintype.card_fin] at this
+  omega
+
+end UniformCircuitFamily
+
+end Cslib.Quantum
+
+namespace Cslib.Complexity
+
+open Quantum Turing.MultiTapeTM
+
+variable {α : Type} {enc : α ↪ List Bool}
+
+/-- `(8 / 9) ^ (6 m) ≤ 2 ^ (-m)`, since `2 * 8 ^ 6 < 9 ^ 6`. -/
+private theorem eight_ninths_pow_le (m : ℕ) : ((8 : ℝ) / 9) ^ (6 * m) ≤ ((2 : ℝ) ^ m)⁻¹ := by
+  rw [pow_mul, ← inv_pow]
+  exact pow_le_pow_left₀ (by positivity) (by norm_num) m
+
+/-- **Error reduction for `BQP`**: a problem is in `BQP` exactly when, for every polynomial `q`,
+some polynomial-time uniform family accepts the encodings of members with probability at least
+`1 - 2^{-q(n)}` and those of other instances with probability at most `2^{-q(n)}`, where `n` is the
+length of the encoding. -/
+theorem mem_BQP_iff_forall_errorExponent {A : Set α} :
+    A ∈ BQP enc ↔ ∀ q : Polynomial ℕ, ∃ F : UniformCircuitFamily, ∀ a,
+      (a ∈ A → 1 - ((2 : ℝ) ^ q.eval (enc a).length)⁻¹ ≤ F.acceptProb (enc a)) ∧
+      (a ∉ A → F.acceptProb (enc a) ≤ ((2 : ℝ) ^ q.eval (enc a).length)⁻¹) := by
+  constructor
+  · rintro ⟨F, hF⟩ q
+    have hr : ComputableInPolyTime (fun n => 6 * q.eval n) encUnary encUnary := by fun_prop
+    refine ⟨F.amplify _ hr, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩
+    · exact le_trans (by linarith [eight_ninths_pow_le (q.eval (enc a).length)])
+        (F.one_sub_le_acceptProb_amplify hr ((hF a).1 ha))
+    · exact (F.acceptProb_amplify_le hr ((hF a).2 ha)).trans (eight_ninths_pow_le _)
+  · intro h
+    obtain ⟨F, hF⟩ := h (Polynomial.C 2)
+    refine ⟨F, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩
+    · have := (hF a).1 ha
+      simp only [Polynomial.eval_C] at this
+      norm_num at this ⊢
+      linarith
+    · have := (hF a).2 ha
+      simp only [Polynomial.eval_C] at this
+      norm_num at this ⊢
+      linarith
+
+end Cslib.Complexity
diff --git a/Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean b/Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean
new file mode 100644
index 000000000..b81adc03e
--- /dev/null
+++ b/Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Basic.Real.Basic
+import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Majority votes over independent trials
+
+Repeat a trial `2 r` times independently, where each trial has outcome `ω ∈ Ω` with probability
+`q ω` and is *good* with probability at least `2 / 3`. Then at most half of the trials are good with
+probability at most `(8 / 9) ^ r` (`Cslib.sum_prod_le_of_card_filter_le`). This is the weighted form
+of `Cslib.card_filter_card_filter_le_le`, where `q` is uniform, with the same exponential-moment
+proof: weight the bad outcomes by `2`, so that the expected weight of a tuple is at most
+`(4 / 3) ^ (2 r)` while a tuple with at most `r` good entries has weight at least `2 ^ r`.
+
+## Main results
+
+* `Cslib.sum_prod_le_of_card_filter_le`: the bound.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 7.4][AroraBarak09]
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+open Finset
+
+variable {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
+
+/-- The weight of an outcome in the exponential-moment bound: `1` when good, `2` when bad. -/
+private def voteWeight (G : Finset Ω) (a : Ω) : ℝ := if a ∈ G then 1 else 2
+
+omit [Fintype Ω] in
+private theorem voteWeight_nonneg (G : Finset Ω) (a : Ω) : 0 ≤ voteWeight G a := by
+  unfold voteWeight
+  split_ifs <;> norm_num
+
+omit [Fintype Ω] in
+/-- A tuple with at most `r` of its `2 r` entries good has weight at least `2 ^ r`. -/
+private theorem two_pow_le_prod_voteWeight (G : Finset Ω) {r : ℕ} (ω : Fin (2 * r) → Ω)
+    (hω : (univ.filter fun i => ω i ∈ G).card ≤ r) : (2 : ℝ) ^ r ≤ ∏ i, voteWeight G (ω i) := by
+  simp only [voteWeight]
+  rw [prod_ite, prod_const_one, prod_const, one_mul]
+  refine pow_le_pow_right₀ (by norm_num) ?_
+  have := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * r))))
+    (fun i => ω i ∈ G)
+  rw [card_univ, Fintype.card_fin] at this
+  omega
+
+/-- The expected weight of one trial is at most `4 / 3`. -/
+private theorem sum_mul_voteWeight_le (q : Ω → ℝ) (hsum : ∑ ω, q ω = 1) (G : Finset Ω)
+    (hG : 2 ≤ 3 * ∑ ω ∈ G, q ω) : ∑ a, q a * voteWeight G a ≤ 4 / 3 := by
+  have hsplit : ∑ a, q a * voteWeight G a = 2 - ∑ a ∈ G, q a := by
+    simp only [voteWeight, mul_ite, mul_one]
+    rw [sum_ite, filter_mem_eq_inter, univ_inter, ← sum_mul, mul_comm]
+    have h := sum_filter_add_sum_filter_not (univ : Finset Ω) (fun a => a ∈ G) q
+    rw [filter_mem_eq_inter, univ_inter, hsum] at h
+    linarith
+  linarith
+
+/-- **Majority votes over independent trials.** If each trial is good with probability at least
+`2 / 3`, then at most half of `2 r` independent trials are good with probability at most
+`(8 / 9) ^ r`. -/
+theorem sum_prod_le_of_card_filter_le (q : Ω → ℝ) (hq : ∀ ω, 0 ≤ q ω) (hsum : ∑ ω, q ω = 1)
+    (G : Finset Ω) (hG : 2 ≤ 3 * ∑ ω ∈ G, q ω) (r : ℕ) :
+    ∑ ω : Fin (2 * r) → Ω with (univ.filter fun i => ω i ∈ G).card ≤ r, ∏ i, q (ω i) ≤
+      (8 / 9) ^ r := by
+  have hmean₀ : 0 ≤ ∑ a, q a * voteWeight G a :=
+    sum_nonneg fun a _ => mul_nonneg (hq a) (voteWeight_nonneg G a)
+  have h2r : (0 : ℝ) < 2 ^ r := by positivity
+  rw [← mul_le_mul_iff_of_pos_left h2r]
+  calc 2 ^ r * ∑ ω : Fin (2 * r) → Ω with (univ.filter fun i => ω i ∈ G).card ≤ r,
+        ∏ i, q (ω i)
+      ≤ ∑ ω : Fin (2 * r) → Ω with (univ.filter fun i => ω i ∈ G).card ≤ r,
+          ∏ i, (q (ω i) * voteWeight G (ω i)) := by
+        rw [mul_sum]
+        refine sum_le_sum fun ω hω => ?_
+        rw [prod_mul_distrib, mul_comm]
+        exact mul_le_mul_of_nonneg_left (two_pow_le_prod_voteWeight G ω (mem_filter.mp hω).2)
+          (prod_nonneg fun i _ => hq _)
+    _ ≤ ∑ ω : Fin (2 * r) → Ω, ∏ i, (q (ω i) * voteWeight G (ω i)) :=
+        sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun ω _ _ =>
+          prod_nonneg fun i _ => mul_nonneg (hq _) (voteWeight_nonneg G _)
+    _ = (∑ a, q a * voteWeight G a) ^ (2 * r) :=
+        (Fintype.sum_pow (fun a => q a * voteWeight G a) (2 * r)).symm
+    _ ≤ (4 / 3) ^ (2 * r) := pow_le_pow_left₀ hmean₀ (sum_mul_voteWeight_le q hsum G hG) _
+    _ = 2 ^ r * (8 / 9) ^ r := by
+        rw [pow_mul, ← mul_pow]
+        norm_num
+
+end Cslib
diff --git a/ComplexityTests/BQPAmplification.lean b/ComplexityTests/BQPAmplification.lean
new file mode 100644
index 000000000..11fafe503
--- /dev/null
+++ b/ComplexityTests/BQPAmplification.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Classes.BQP.Amplification
+import ComplexityTests.BQP
+
+/-! Error reduction for `BQP`: the reversible counter on a concrete register, the exact
+acceptance probability of a majority vote over two fair coins, and exponentially small error for a
+language in `BQP`. -/
+
+namespace ComplexityTests.BQPAmplification
+
+open Cslib Cslib.Quantum Cslib.Complexity Finset Turing.MultiTapeTM
+open ComplexityTests.BQP
+
+/-! ### The counter -/
+
+-- Two input bits at qubits `0, 1`, one of them set; two levels from `base = 2` on, on `9` qubits.
+-- After both stages, level `0` (more than zero inputs set) is one and level `1` is zero.
+example : readBit (GateCode.classicalRun (Counter.codes 2 2 id 2)
+    (fun i : Fin 9 => decide (i = 0))) (Counter.level 2 2 2 0) = true := by decide
+example : readBit (GateCode.classicalRun (Counter.codes 2 2 id 2)
+    (fun i : Fin 9 => decide (i = 0))) (Counter.level 2 2 2 1) = false := by decide
+-- With both inputs set, level `1` is one.
+example : readBit (GateCode.classicalRun (Counter.codes 2 2 id 2)
+    (fun i : Fin 9 => decide (i.val < 2))) (Counter.level 2 2 2 1) = true := by decide
+
+/-! ### A majority of two fair coins -/
+
+/-- Both of two fair coins land heads with probability `1 / 4`: amplifying the family that
+measures `H|0⟩` by a strict majority of two copies. -/
+theorem acceptProb_amplify_hadamardOnce (x : List Bool) :
+    (hadamardOnce.amplify (fun _ => 1) (ComputableInPolyTime.const _)).acceptProb x = 1 / 4 := by
+  rw [UniformCircuitFamily.acceptProb_amplify, acceptProb_hadamardOnce]
+  have hhalf (c : Bool) : (if c = true then (1 / 2 : ℝ) else 1 - 1 / 2) = 1 / 2 := by
+    cases c <;> norm_num
+  simp only [hhalf, prod_const, card_univ, Fintype.card_fin, sum_const, nsmul_eq_mul]
+  have hcard : (univ.filter fun b : Fin (2 * 1) → Bool =>
+      1 < (univ.filter fun j => b j = true).card).card = 1 := by decide
+  rw [hcard]
+  norm_num
+
+/-! ### Exponentially small error -/
+
+-- The words starting with one are accepted with probability at least `1 - 2^{-q(n)}`, and the
+-- others with probability at most `2^{-q(n)}`, for every polynomial `q`.
+example (q : Polynomial ℕ) : ∃ F : UniformCircuitFamily, ∀ x,
+    (x ∈ FirstBit → 1 - ((2 : ℝ) ^ q.eval (encBits x).length)⁻¹ ≤ F.acceptProb (encBits x)) ∧
+    (x ∉ FirstBit → F.acceptProb (encBits x) ≤ ((2 : ℝ) ^ q.eval (encBits x).length)⁻¹) :=
+  mem_BQP_iff_forall_errorExponent.mp firstBit_mem_BQP q
+
+end ComplexityTests.BQPAmplification