diff --git a/Complexity.lean b/Complexity.lean
index 6c8ef02a1..5e5eb5890 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1658,6 +1658,7 @@ public import Complexity.Computability.GenericRAM.Native.Certificate
 public import Complexity.Computability.GenericRAM.Native.Combinators
 public import Complexity.Computability.GenericRAM.Native.Degree
 public import Complexity.Computability.GenericRAM.Native.ExhaustiveCountFallback
+public import Complexity.Computability.GenericRAM.Native.ExpTimePolySpace
 public import Complexity.Computability.GenericRAM.Native.HeavyBranchFold
 public import Complexity.Computability.GenericRAM.Native.IndexFold
 public import Complexity.Computability.GenericRAM.Native.MeasurementFold
diff --git a/Complexity/Computability/Circuit/Quantum/Code.lean b/Complexity/Computability/Circuit/Quantum/Code.lean
index 0ee18bbd6..2694fb099 100644
--- a/Complexity/Computability/Circuit/Quantum/Code.lean
+++ b/Complexity/Computability/Circuit/Quantum/Code.lean
@@ -29,7 +29,9 @@ definition of uniform circuit families.
 A run starts in the basis state `|x 0^{m - n}⟩` holding the input word `x` of length `n` on the
 first qubits (`Cslib.Quantum.inputState`), and accepts when the final measurement finds qubit `0`
 in state `1` (`Cslib.Quantum.accepting`, `Cslib.Quantum.acceptProb`), as in
-[Arora, Barak][AroraBarak09], Chapter 10.
+[Arora, Barak][AroraBarak09], Chapter 10. More generally, `Cslib.Quantum.onesProb` is the
+probability that the final measurement finds every qubit of a list `S` in state `1`, the events on
+which postselected classes condition.
 
 Classical reversible gates permute basis states, updating the bit of their target
 (`Cslib.Quantum.GateCode.eval_toPlacedGate_ket`). Appending a NOT gate on qubit `0` exchanges
@@ -42,6 +44,8 @@ acceptance and rejection (`Cslib.Quantum.acceptProb_append_not`).
 * `Cslib.Quantum.Circuit.ofCodes`: the circuit denoted by a list of gate codes.
 * `Cslib.Quantum.inputState`, `Cslib.Quantum.accepting`, `Cslib.Quantum.acceptProb`: the input
   basis state, the accepting outcomes and the acceptance probability.
+* `Cslib.Quantum.onesAt`, `Cslib.Quantum.onesProb`: the outcomes in which every qubit of a list
+  reads `1`, and their probability; acceptance is the case of qubit `0`.
 
 ## Main results
 
@@ -249,28 +253,55 @@ theorem Circuit.ofCodes_append (gs hs : List GateCode) :
 first qubits (truncated when `x` is longer than `m`). -/
 def inputState (m : ℕ) (x : List Bool) : Fin m → Bool := fun i => x.getD i false
 
+/-- The outcomes in which every qubit of `S` reads `1`. -/
+def onesAt (m : ℕ) (S : List ℕ) : Finset (Fin m → Bool) :=
+  univ.filter fun y => ∀ j ∈ S, ∃ h : j < m, y ⟨j, h⟩ = true
+
+/-- The probability that the final measurement of the circuit with gate codes `gs` on `m` qubits,
+started in `|x 0^{m - n}⟩`, finds every qubit of `S` in state `1`. The acceptance probability is the
+case `S = [0]` (`Cslib.Quantum.acceptProb_eq_onesProb`). -/
+noncomputable def onesProb (m : ℕ) (gs : List GateCode) (S : List ℕ) (x : List Bool) : ℝ :=
+  measureProb (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (onesAt m S)
+
+theorem onesProb_nonneg (m : ℕ) (gs : List GateCode) (S : List ℕ) (x : List Bool) :
+    0 ≤ onesProb m gs S x :=
+  measureProb_nonneg _ _
+
+theorem onesProb_le_one (m : ℕ) (gs : List GateCode) (S : List ℕ) (x : List Bool) :
+    onesProb m gs S x ≤ 1 := by
+  have h := measureProb_le_measureProb_univ
+    (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (onesAt m S)
+  rwa [measureProb_univ, Circuit.norm_run, one_pow] at h
+
+/-- The event of no condition is certain. -/
+@[simp] theorem onesProb_nil (m : ℕ) (gs : List GateCode) (x : List Bool) :
+    onesProb m gs [] x = 1 := by
+  rw [onesProb, show onesAt m [] = univ by simp [onesAt], measureProb_univ, Circuit.norm_run,
+    one_pow]
+
 /-- The accepting outcomes: qubit `0` reads `1`. -/
-def accepting (m : ℕ) : Finset (Fin m → Bool) :=
-  univ.filter fun y => ∃ h : 0 < m, y ⟨0, h⟩ = true
+def accepting (m : ℕ) : Finset (Fin m → Bool) := onesAt m [0]
 
 /-- The **acceptance probability** of the circuit with gate codes `gs` on `m` qubits on input `x`:
 started in `|x 0^{m - n}⟩`, the final measurement finds qubit `0` in state `1`. -/
 noncomputable def acceptProb (m : ℕ) (gs : List GateCode) (x : List Bool) : ℝ :=
   measureProb (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (accepting m)
 
+theorem acceptProb_eq_onesProb (m : ℕ) (gs : List GateCode) (x : List Bool) :
+    acceptProb m gs x = onesProb m gs [0] x :=
+  rfl
+
 theorem acceptProb_nonneg (m : ℕ) (gs : List GateCode) (x : List Bool) :
     0 ≤ acceptProb m gs x :=
-  measureProb_nonneg _ _
+  onesProb_nonneg m gs [0] x
 
 theorem acceptProb_le_one (m : ℕ) (gs : List GateCode) (x : List Bool) :
-    acceptProb m gs x ≤ 1 := by
-  have h := measureProb_le_measureProb_univ
-    (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (accepting m)
-  rwa [measureProb_univ, Circuit.norm_run, one_pow] at h
+    acceptProb m gs x ≤ 1 :=
+  onesProb_le_one m gs [0] x
 
 theorem mem_accepting (hm : 0 < m) {y : Fin m → Bool} :
     y ∈ accepting m ↔ y ⟨0, hm⟩ = true := by
-  simp [accepting, hm]
+  simp [accepting, onesAt, hm]
 
 /-- The probability of the rejecting outcomes is one minus the acceptance probability. -/
 private theorem measureProb_compl_accepting (ψ : Qubits m) (hψ : ‖ψ‖ = 1) :
diff --git a/Complexity/Computability/Circuit/Quantum/PathNetwork.lean b/Complexity/Computability/Circuit/Quantum/PathNetwork.lean
index 82a2a6ddd..6f96a84ab 100644
--- a/Complexity/Computability/Circuit/Quantum/PathNetwork.lean
+++ b/Complexity/Computability/Circuit/Quantum/PathNetwork.lean
@@ -20,7 +20,9 @@ import Mathlib.Logic.Equiv.Fin.Basic
 
 The acceptance gap of a list of gate codes (`Cslib.Quantum.acceptGap`) is the contraction of an
 explicit Boolean tensor network (`Cslib.Quantum.PathNetwork.network`) built from the circuit and a
-mirror copy of it (`Cslib.Quantum.PathNetwork.contraction_network`). This is the form in which the
+mirror copy of it (`Cslib.Quantum.PathNetwork.contraction_network`). More generally, for a list `S`
+of *measured* qubits, the network computes the projected gap `Cslib.Quantum.onesGap S` of the event
+that every qubit of `S` reads `1`; acceptance is the case `S = [0]`. This is the form in which the
 contraction algorithm of [OpenAI2026ETH], Theorem D.1, simulates quantum circuits exactly.
 
 **Occurrences.** The *qubits* of a gate code are its target and then its controls
@@ -41,9 +43,9 @@ occurrences from `base gs i` on. The last occurrence of qubit `j` before positio
   otherwise; for a classical gate it is the indicator that the outputs are the gate applied to the
   inputs.
 * **Glue vertices (rows).** The link edges of the last occurrence of each qubit in the two copies
-  meet at a glue vertex with the equality tensor, or, for qubit `0`, the tensor that requires both
-  bits to be one. A *scalar* vertex without ports requires the input bit of qubit `0` to be one when
-  no gate touches qubit `0`.
+  meet at a glue vertex with the equality tensor, or, for a measured qubit, the tensor that requires
+  both bits to be one. A *scalar* vertex without ports requires the input bit of every measured
+  qubit that no gate touches to be one.
 * **Segment vertices (columns).** Each segment joins its out and link edges with the equality
   tensor.
 
@@ -51,8 +53,8 @@ So every edge joins a row to a column, every vertex has at most six ports, and u
 cost nothing. The gate tables are bounded tables for the degree bound six
 (`Cslib.Circuits.Frontier.ExplicitTensorNetwork.boundedTable`). With `neg = -1`, an assignment of
 nonzero weight is a pair of paths of the path sum
-(`Cslib.Quantum.pathRun`) ending in the same register with qubit `0` equal to one, and its weight
-is the product of their signs, so the contraction is `acceptGap`
+(`Cslib.Quantum.pathRun`) ending in the same register with every measured qubit equal to one, and
+its weight is the product of their signs, so the contraction is `onesGap S`
 (`Cslib.Quantum.PathNetwork.contraction_network`). The network is defined for any value `neg` of
 the Hadamard sign, so that over `ℕ` it can carry `2 ^ P - 1`, which is `-1` modulo `2 ^ P`
 (`Cslib.Quantum.PathNetwork.contraction_network_mod`).
@@ -73,10 +75,10 @@ the Hadamard sign, so that over `ℕ` it can carry `2 ^ P - 1`, which is `-1` mo
 * `Cslib.Quantum.PathNetwork.lastOcc_succ`, `Cslib.Quantum.PathNetwork.lastOcc_eq_some`,
   `Cslib.Quantum.PathNetwork.lastOcc_eq_none`: last occurrences.
 * `Cslib.Quantum.PathNetwork.contraction_network`: with the Hadamard sign `-1`, the contraction
-  is the acceptance gap.
+  is the projected gap.
 * `Cslib.Quantum.PathNetwork.network_mapTables`,
   `Cslib.Quantum.PathNetwork.contraction_network_mod`: over `ℕ`, with the Hadamard sign
-  `2 ^ P - 1`, the contraction modulo `2 ^ P` is the acceptance gap once `P` exceeds the number
+  `2 ^ P - 1`, the contraction modulo `2 ^ P` is the projected gap once `P` exceeds the number
   of Hadamard gates.
 * `Cslib.Quantum.PathNetwork.numEdges_network`,
   `Cslib.Quantum.PathNetwork.length_vertices_network`,
@@ -157,28 +159,29 @@ of `j`, or the bit of its input port. -/
 /-- The table on two ports that requires both bits to be one. -/
 @[expose] def acceptTable : List R := [0, 0, 0, 1]
 
-/-- The glue vertex of occurrence `w`: when `w` is the last occurrence of its qubit, it joins the
-link edges of `w` in the two copies, requiring equal bits, and both bits one for qubit `0`. -/
-@[expose] def glueVertex (gs : List GateCode) (w : ℕ) : List ℕ × List R :=
+/-- The glue vertex of occurrence `w`, for the list `S` of measured qubits: when `w` is the last
+occurrence of its qubit, it joins the link edges of `w` in the two copies, requiring equal bits,
+and both bits one for a qubit of `S`. -/
+@[expose] def glueVertex (S : List ℕ) (gs : List GateCode) (w : ℕ) : List ℕ × List R :=
   if lastOcc (occurrences gs) ((occurrences gs).getD w 0) (occurrences gs).length = some w then
     ([2 * w + 1, 2 * ((occurrences gs).length + w) + 1],
-      if (occurrences gs).getD w 0 = 0 then acceptTable else eqTable)
+      if (occurrences gs).getD w 0 ∈ S then acceptTable else eqTable)
   else ([], [1])
 
-/-- The scalar vertex: when no gate touches qubit `0`, it requires the input bit of qubit `0` to be
+/-- The scalar vertex: it requires the input bit of every qubit of `S` that no gate touches to be
 one. -/
-@[expose] def scalarVertex (X : List Bool) (gs : List GateCode) : List ℕ × List R :=
-  ([], [if 0 ∈ occurrences gs ∨ X.getD 0 false = true then 1 else 0])
+@[expose] def scalarVertex (S : List ℕ) (X : List Bool) (gs : List GateCode) : List ℕ × List R :=
+  ([], [if ∀ j ∈ S, j ∈ occurrences gs ∨ X.getD j false = true then 1 else 0])
 
-/-- **The network of a circuit** with the input register `X` and the Hadamard sign `neg`, with its
-number of rows: the gate vertices of the two copies, the glue vertices and the scalar vertex, then
-the segment vertices. -/
-@[expose] def network (neg : R) (X : List Bool) (gs : List GateCode) :
+/-- **The network of a circuit** with the measured qubits `S`, the input register `X` and the
+Hadamard sign `neg`, with its number of rows: the gate vertices of the two copies, the glue
+vertices and the scalar vertex, then the segment vertices. -/
+@[expose] def network (neg : R) (S : List ℕ) (X : List Bool) (gs : List GateCode) :
     ℕ × ExplicitTensorNetwork R :=
   (2 * gs.length + (occurrences gs).length + 1, ⟨2 * (2 * (occurrences gs).length),
     (List.range gs.length).map (gateVertex neg X gs 0) ++
         (List.range gs.length).map (gateVertex neg X gs 1) ++
-        (List.range (occurrences gs).length).map (glueVertex gs) ++ [scalarVertex X gs] ++
+        (List.range (occurrences gs).length).map (glueVertex S gs) ++ [scalarVertex S X gs] ++
       (List.range (2 * (occurrences gs).length)).map fun w => ([2 * w, 2 * w + 1], eqTable)⟩)
 
 end Vertices
@@ -563,19 +566,19 @@ private theorem entry_gateVertex (neg : R) (X : List Bool) (gs : List GateCode)
     omega
 
 /-- The glue condition on the final bits `a` and `b` of the qubit `j` in the two copies: they are
-equal, and one for qubit `0`. -/
-private def GlueOK (a b : Bool) (j : ℕ) : Prop := a = b ∧ (j = 0 → a = true)
+equal, and one for a qubit of `S`. -/
+private def GlueOK (S : List ℕ) (a b : Bool) (j : ℕ) : Prop := a = b ∧ (j ∈ S → a = true)
 
-private instance (a b : Bool) (j : ℕ) : Decidable (GlueOK a b j) := by
+private instance (S : List ℕ) (a b : Bool) (j : ℕ) : Decidable (GlueOK S a b j) := by
   unfold GlueOK
   infer_instance
 
 /-- **The entry of a glue vertex** when edge `e` carries `Z (e / 2)`. -/
-private theorem entry_glueVertex (gs : List GateCode) (w : ℕ) (Z : ℕ → Bool) :
-    entry (glueVertex gs w : List ℕ × List R).2
-        ((glueVertex gs w : List ℕ × List R).1.map fun e => Z (e / 2)) =
+private theorem entry_glueVertex (S : List ℕ) (gs : List GateCode) (w : ℕ) (Z : ℕ → Bool) :
+    entry (glueVertex S gs w : List ℕ × List R).2
+        ((glueVertex S gs w : List ℕ × List R).1.map fun e => Z (e / 2)) =
       if (lastOcc (occurrences gs) ((occurrences gs).getD w 0) (occurrences gs).length = some w →
-          GlueOK (Z w) (Z ((occurrences gs).length + w)) ((occurrences gs).getD w 0))
+          GlueOK S (Z w) (Z ((occurrences gs).length + w)) ((occurrences gs).getD w 0))
         then (1 : R) else 0 := by
   unfold glueVertex
   by_cases hl : lastOcc (occurrences gs) ((occurrences gs).getD w 0) (occurrences gs).length =
@@ -583,17 +586,17 @@ private theorem entry_glueVertex (gs : List GateCode) (w : ℕ) (Z : ℕ → Boo
   · simp only [hl, ↓reduceIte, List.map_cons, List.map_nil, true_implies,
       show (2 * w + 1) / 2 = w by omega,
       show (2 * ((occurrences gs).length + w) + 1) / 2 = (occurrences gs).length + w by omega]
-    by_cases h0 : (occurrences gs).getD w 0 = 0
+    by_cases h0 : (occurrences gs).getD w 0 ∈ S
     · simp only [h0, ↓reduceIte, GlueOK, true_implies]
       cases Z w <;> cases Z ((occurrences gs).length + w) <;> rfl
     · simp only [h0, ↓reduceIte, GlueOK, entry_eqTable, false_implies, and_true]
   · simp only [hl, ↓reduceIte, false_implies]
     rfl
 
-private theorem entry_scalarVertex (X : List Bool) (gs : List GateCode) :
-    entry (scalarVertex X gs : List ℕ × List R).2 ((scalarVertex X gs : List ℕ × List R).1.map
-        fun _ => false) =
-      if 0 ∈ occurrences gs ∨ X.getD 0 false = true then 1 else 0 := rfl
+private theorem entry_scalarVertex (S : List ℕ) (X : List Bool) (gs : List GateCode) :
+    entry (scalarVertex S X gs : List ℕ × List R).2
+        ((scalarVertex S X gs : List ℕ × List R).1.map fun _ => false) =
+      if ∀ j ∈ S, j ∈ occurrences gs ∨ X.getD j false = true then 1 else 0 := rfl
 
 end Entries
 
@@ -614,15 +617,15 @@ private theorem getD_foldl_pathStep_of_not_mem (gs : List GateCode) {j : ℕ}
 
 /-- The condition of the glue and scalar vertices on the final registers `r` and `r'` of the two
 copies. -/
-private def FinalOK (X : List Bool) (gs : List GateCode) (r r' : ℕ → Bool) : Prop :=
+private def FinalOK (S : List ℕ) (X : List Bool) (gs : List GateCode) (r r' : ℕ → Bool) : Prop :=
   (∀ w < (occurrences gs).length,
     lastOcc (occurrences gs) ((occurrences gs).getD w 0) (occurrences gs).length = some w →
-      GlueOK (r ((occurrences gs).getD w 0)) (r' ((occurrences gs).getD w 0))
+      GlueOK S (r ((occurrences gs).getD w 0)) (r' ((occurrences gs).getD w 0))
         ((occurrences gs).getD w 0)) ∧
-    (0 ∈ occurrences gs ∨ X.getD 0 false = true)
+    ∀ j ∈ S, j ∈ occurrences gs ∨ X.getD j false = true
 
-private instance (X : List Bool) (gs : List GateCode) (r r' : ℕ → Bool) :
-    Decidable (FinalOK X gs r r') := by
+private instance (S : List ℕ) (X : List Bool) (gs : List GateCode) (r r' : ℕ → Bool) :
+    Decidable (FinalOK S X gs r r') := by
   unfold FinalOK
   infer_instance
 
@@ -636,13 +639,13 @@ private theorem mem_iff_getD (qs : List ℕ) (j : ℕ) :
     exact ⟨w, hw, (List.getD_eq_getElem _ _ hw).symm⟩
 
 /-- **The glue condition on two final registers** that agree with the input register off the
-touched qubits: the registers are equal and qubit `0` is one. -/
-private theorem finalOK_iff (X : List Bool) (gs : List GateCode) {s s' : List Bool}
+touched qubits: the registers are equal and every qubit of `S` is one. -/
+private theorem finalOK_iff (S : List ℕ) (X : List Bool) (gs : List GateCode) {s s' : List Bool}
     (hs : s.length = X.length) (hs' : s'.length = X.length)
     (hu : ∀ j ∉ occurrences gs, s.getD j false = X.getD j false)
     (hu' : ∀ j ∉ occurrences gs, s'.getD j false = X.getD j false) :
-    FinalOK X gs (fun j => s.getD j false) (fun j => s'.getD j false) ↔
-      s = s' ∧ s.headD false = true := by
+    FinalOK S X gs (fun j => s.getD j false) (fun j => s'.getD j false) ↔
+      s = s' ∧ ∀ j ∈ S, s.getD j false = true := by
   set qs := occurrences gs
   -- a touched qubit has a last occurrence
   have hlast (j : ℕ) (hj : j ∈ qs) : ∃ w < qs.length, qs.getD w 0 = j ∧
@@ -654,32 +657,26 @@ private theorem finalOK_iff (X : List Bool) (gs : List GateCode) {s s' : List Bo
     | some w =>
       obtain ⟨hw, hwj, -⟩ := lastOcc_eq_some hl
       exact ⟨w, hw, hwj, hwj ▸ hl⟩
-  have hhead : s.headD false = s.getD 0 false := by cases s <;> rfl
   constructor
-  · rintro ⟨hglue, h0⟩
-    have heq (j : ℕ) : s.getD j false = s'.getD j false ∧ (j = 0 → j ∈ qs →
-        s.getD 0 false = true) := by
+  · rintro ⟨hglue, hS⟩
+    have heq (j : ℕ) : s.getD j false = s'.getD j false ∧ (j ∈ S → j ∈ qs →
+        s.getD j false = true) := by
       by_cases hj : j ∈ qs
       · obtain ⟨w, hw, rfl, hl⟩ := hlast j hj
-        obtain ⟨h1, h2⟩ := hglue w hw hl
-        exact ⟨h1, fun h _ => h ▸ h2 h⟩
+        exact ⟨(hglue w hw hl).1, fun h _ => (hglue w hw hl).2 h⟩
       · exact ⟨(hu j hj).trans (hu' j hj).symm, fun _ h => absurd h hj⟩
-    refine ⟨List.ext_getElem (hs.trans hs'.symm) fun j h₁ h₂ => ?_, ?_⟩
+    refine ⟨List.ext_getElem (hs.trans hs'.symm) fun j h₁ h₂ => ?_, fun j hj => ?_⟩
     · have := (heq j).1
       rwa [List.getD_eq_getElem _ _ h₁, List.getD_eq_getElem _ _ h₂] at this
-    · rw [hhead]
-      by_cases h : 0 ∈ qs
-      · exact (heq 0).2 rfl h
-      · rw [hu 0 h]
-        exact h0.resolve_left h
-  · rintro ⟨rfl, hs0⟩
-    refine ⟨fun w _ _ => ⟨rfl, fun h => ?_⟩, ?_⟩
-    · change s.getD (qs.getD w 0) false = true
-      rw [h, ← hhead]
-      exact hs0
-    by_cases h : 0 ∈ qs
+    · by_cases h : j ∈ qs
+      · exact (heq j).2 hj h
+      · rw [hu j h]
+        exact (hS j hj).resolve_left h
+  · rintro ⟨rfl, hs1⟩
+    refine ⟨fun w _ _ => ⟨rfl, hs1 _⟩, fun j hj => ?_⟩
+    by_cases h : j ∈ qs
     · exact Or.inl h
-    · exact Or.inr ((hu 0 h).symm.trans (hhead ▸ hs0))
+    · exact Or.inr ((hu j h).symm.trans (hs1 j hj))
 
 /-! ### The contraction -/
 
@@ -725,12 +722,13 @@ private theorem map_pairFun_right {N : ℕ} (a b : Fin N → Bool) :
   simp only [List.length_map, List.length_range] at h₁
   simp [show N + u < 2 * N by omega]
 
-/-- **The contraction of the network is the acceptance gap.** With `-1` as the Hadamard sign, over
-any commutative ring, the contraction of the network of well-formed gate codes on the input
-register `X` is `acceptGap gs X`. -/
-theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List GateCode)
-    (hgs : ∀ g ∈ gs, g.WellFormed X.length) :
-    (network (-1 : R) X gs).2.contraction = (acceptGap gs X : R) := by
+/-- **The contraction of the network is the projected gap.** With `-1` as the Hadamard sign, over
+any commutative ring, the contraction of the network of well-formed gate codes with the measured
+qubits `S` on the input register `X` is `onesGap S gs X`; for `S = [0]` it is the acceptance gap
+`Cslib.Quantum.acceptGap`. -/
+theorem contraction_network {R : Type*} [CommRing R] (S : List ℕ) (X : List Bool)
+    (gs : List GateCode) (hgs : ∀ g ∈ gs, g.WellFormed X.length) :
+    (network (-1 : R) S X gs).2.contraction = (onesGap S gs X : R) := by
   set qs := occurrences gs with hqs
   set N := qs.length with hN
   set Xf : ℕ → Bool := fun j => X.getD j false
@@ -759,10 +757,10 @@ theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List
     exact List.map_congr_left fun i hi =>
       entry_gateVertex _ X gs c i (hq3 i (List.mem_range.mp hi)) Z
   -- the glue and scalar vertices
-  have hG (Z : ℕ → Bool) : ((List.range N).map (glueVertex gs)).map
+  have hG (Z : ℕ → Bool) : ((List.range N).map (glueVertex S gs)).map
       (fun v => entry (v : List ℕ × List R).2 (v.1.map fun e => Z (e / 2))) =
         (List.range N).map fun w => if (lastOcc qs (qs.getD w 0) N = some w →
-          GlueOK (reg qs Xf (fun u => Z (0 * N + u)) N (qs.getD w 0))
+          GlueOK S (reg qs Xf (fun u => Z (0 * N + u)) N (qs.getD w 0))
             (reg qs Xf (fun u => Z (1 * N + u)) N (qs.getD w 0)) (qs.getD w 0)) then 1 else 0 := by
     rw [List.map_map]
     refine List.map_congr_left fun w _ => ?_
@@ -773,15 +771,15 @@ theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List
   have hrows (Z : ℕ → Bool) :
       (((List.range gs.length).map (gateVertex (-1 : R) X gs 0) ++
           (List.range gs.length).map (gateVertex (-1 : R) X gs 1) ++
-          (List.range N).map (glueVertex gs) ++ [scalarVertex X gs]).map
+          (List.range N).map (glueVertex S gs) ++ [scalarVertex S X gs]).map
         fun v : List ℕ × List R => entry v.2 (v.1.map fun e => Z (e / 2))).prod =
       P (fun u => Z (0 * N + u)) * (P (fun u => Z (1 * N + u)) *
-        if FinalOK X gs (reg qs Xf (fun u => Z (0 * N + u)) N)
+        if FinalOK S X gs (reg qs Xf (fun u => Z (0 * N + u)) N)
           (reg qs Xf (fun u => Z (1 * N + u)) N) then 1 else 0) := by
     simp only [List.map_append, List.prod_append, hP, hG, List.prod_map_boole, List.map_cons,
       List.map_nil, List.prod_cons, List.prod_nil, mul_one]
-    rw [show entry (scalarVertex X gs : List ℕ × List R).2 ((scalarVertex X gs).1.map
-      fun e => Z (e / 2)) = if 0 ∈ qs ∨ X.getD 0 false = true then 1 else 0 from rfl]
+    rw [show entry (scalarVertex S X gs : List ℕ × List R).2 ((scalarVertex S X gs).1.map
+      fun e => Z (e / 2)) = if ∀ j ∈ S, j ∈ qs ∨ X.getD j false = true then 1 else 0 from rfl]
     simp only [P, FinalOK, ← hqs, ← hN, ite_and, List.mem_range]
     split_ifs <;> ring
   -- the pair reduction and the two halves
@@ -790,7 +788,7 @@ theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List
   rw [contraction_append_pairs]
   refine (sum_pair N fun Z => (((List.range gs.length).map (gateVertex (-1 : R) X gs 0) ++
       (List.range gs.length).map (gateVertex (-1 : R) X gs 1) ++
-      (List.range N).map (glueVertex gs) ++ [scalarVertex X gs]).map
+      (List.range N).map (glueVertex S gs) ++ [scalarVertex S X gs]).map
     fun v : List ℕ × List R => entry v.2 (v.1.map fun e => Z (e / 2))).prod).trans ?_
   simp only [hrows]
   -- each copy is a run along the occurrences
@@ -799,14 +797,14 @@ theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List
     prod_gateEntry_mul (-1 : R) gs Xf y Φ
   have hstep (a b : Fin N → Bool) :
       P (fun u => pairFun a b (0 * N + u)) * (P (fun u => pairFun a b (1 * N + u)) *
-        if FinalOK X gs (reg qs Xf (fun u => pairFun a b (0 * N + u)) N)
+        if FinalOK S X gs (reg qs Xf (fun u => pairFun a b (0 * N + u)) N)
           (reg qs Xf (fun u => pairFun a b (1 * N + u)) N) then 1 else 0) =
       trajWeight (-1) gs Xf (List.ofFn a) fun r0 =>
-        trajWeight (-1) gs Xf (List.ofFn b) fun r1 => if FinalOK X gs r0 r1 then 1 else 0 := by
+        trajWeight (-1) gs Xf (List.ofFn b) fun r1 => if FinalOK S X gs r0 r1 then 1 else 0 := by
     have h1 := hB (fun u => pairFun a b (1 * N + u)) fun r1 =>
-      if FinalOK X gs (reg qs Xf (fun u => pairFun a b (0 * N + u)) N) r1 then (1 : R) else 0
+      if FinalOK S X gs (reg qs Xf (fun u => pairFun a b (0 * N + u)) N) r1 then (1 : R) else 0
     have h0 := hB (fun u => pairFun a b (0 * N + u)) fun r0 =>
-      trajWeight (-1) gs Xf (List.ofFn b) fun r1 => if FinalOK X gs r0 r1 then (1 : R) else 0
+      trajWeight (-1) gs Xf (List.ofFn b) fun r1 => if FinalOK S X gs r0 r1 then (1 : R) else 0
     simp only [map_pairFun_left, map_pairFun_right] at h0 h1
     rw [h1]
     exact h0
@@ -818,30 +816,33 @@ theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List
     rwa [sgn, ite_eq_right Bool.false_ne_true, one_mul] at this
   have hinner (a : Fin N → Bool) : ∑ b : Fin N → Bool, (trajWeight (-1) gs Xf (List.ofFn a)
       fun r0 => trajWeight (-1) gs Xf (List.ofFn b) fun r1 =>
-        if FinalOK X gs r0 r1 then (1 : R) else 0) =
+        if FinalOK S X gs r0 r1 then (1 : R) else 0) =
       trajWeight (-1) gs Xf (List.ofFn a) fun r0 =>
         ∑ π' : Fin (hadamardCount gs) → Bool, sgn (gs.foldl pathStep (X, List.ofFn π', false)).2.2 *
-          if FinalOK X gs r0 (fun j => (gs.foldl pathStep (X, List.ofFn π', false)).1.getD j false)
+          if FinalOK S X gs r0
+            (fun j => (gs.foldl pathStep (X, List.ofFn π', false)).1.getD j false)
             then 1 else 0 := by
     rw [← trajWeight_sum]
     congr 1
     funext r0
     exact hC _
   simp only [hstep, hinner]
-  rw [hC, acceptGap, Int.cast_sum]
+  rw [hC, onesGap, Int.cast_sum]
   refine Finset.sum_congr rfl fun π _ => ?_
   rw [Int.cast_sum, Finset.mul_sum]
   refine Finset.sum_congr rfl fun π' _ => ?_
   set f := gs.foldl pathStep (X, List.ofFn π, false)
   set f' := gs.foldl pathStep (X, List.ofFn π', false)
-  have hok := finalOK_iff X gs (s := f.1) (s' := f'.1) (length_foldl_pathStep _ _ _ _)
+  have hok := finalOK_iff S X gs (s := f.1) (s' := f'.1) (length_foldl_pathStep _ _ _ _)
     (length_foldl_pathStep _ _ _ _) (fun j hj => getD_foldl_pathStep_of_not_mem gs hj _ _ _)
     (fun j hj => getD_foldl_pathStep_of_not_mem gs hj _ _ _)
-  have hterm : acceptTerm gs X (List.ofFn π) (List.ofFn π') =
-      if f.1 = f'.1 ∧ f.1.headD false = true then (if f.2.2 ^^ f'.2.2 then -1 else 1) else 0 :=
+  have hterm : onesTerm S gs X (List.ofFn π) (List.ofFn π') =
+      if f.1 = f'.1 ∧ ∀ j ∈ S, f.1.getD j false = true then
+        (if f.2.2 ^^ f'.2.2 then -1 else 1) else 0 := by
+    simp only [onesTerm, pathRun, List.all_eq_true]
     rfl
   rw [hterm]
-  by_cases hc : f.1 = f'.1 ∧ f.1.headD false = true
+  by_cases hc : f.1 = f'.1 ∧ ∀ j ∈ S, f.1.getD j false = true
   · rw [ite_eq_left (hok.mpr hc), ite_eq_left hc]
     cases f.2.2 <;> cases f'.2.2 <;> simp [sgn]
   · rw [ite_eq_right (mt hok.mp hc), ite_eq_right hc]
@@ -850,9 +851,9 @@ theorem contraction_network {R : Type*} [CommRing R] (X : List Bool) (gs : List
 /-! ### Residues of the contraction over `ℕ` -/
 
 /-- **Mapping the tables maps the Hadamard sign.** -/
-theorem network_mapTables {R S : Type*} [CommSemiring R] [CommSemiring S] (ψ : R →+* S) (neg : R)
-    (X : List Bool) (gs : List GateCode) :
-    (network neg X gs).2.mapTables ψ = (network (ψ neg) X gs).2 := by
+theorem network_mapTables {R R' : Type*} [CommSemiring R] [CommSemiring R'] (ψ : R →+* R')
+    (neg : R) (S : List ℕ) (X : List Bool) (gs : List GateCode) :
+    (network neg S X gs).2.mapTables ψ = (network (ψ neg) S X gs).2 := by
   have hgate (c i : ℕ) : (fun v : List ℕ × List R => (v.1, v.2.map ψ)) (gateVertex neg X gs c i) =
       gateVertex (ψ neg) X gs c i := by
     simp only [gateVertex, boundedTable, List.map_map]
@@ -860,8 +861,8 @@ theorem network_mapTables {R S : Type*} [CommSemiring R] [CommSemiring S] (ψ :
     funext idx
     simp only [Function.comp_apply, gateEntry]
     split_ifs <;> simp
-  have hglue (w : ℕ) : (fun v : List ℕ × List R => (v.1, v.2.map ψ)) (glueVertex gs w) =
-      glueVertex gs w := by
+  have hglue (w : ℕ) : (fun v : List ℕ × List R => (v.1, v.2.map ψ)) (glueVertex S gs w) =
+      glueVertex S gs w := by
     simp only [glueVertex]
     split_ifs <;> simp [acceptTable, eqTable]
   simp only [network, ExplicitTensorNetwork.mapTables, List.map_append, List.map_map,
@@ -870,23 +871,24 @@ theorem network_mapTables {R S : Type*} [CommSemiring R] [CommSemiring S] (ψ :
   congr 3
   split_ifs <;> simp
 
-/-- **The residue of the contraction over `ℕ` is the acceptance gap.** With `2 ^ P - 1`, which is
+/-- **The residue of the contraction over `ℕ` is the projected gap.** With `2 ^ P - 1`, which is
 `-1` modulo `2 ^ P`, as the Hadamard sign, and `P` larger than the number of Hadamard gates, the
-contraction of the network of well-formed gate codes on a nonempty input register `X`, reduced
-modulo `2 ^ P`, is the acceptance gap. -/
-theorem contraction_network_mod (X : List Bool) (hX : 0 < X.length) (gs : List GateCode)
+contraction of the network of well-formed gate codes with the measured qubits `S` on the input
+register `X`, reduced modulo `2 ^ P`, is the projected gap. -/
+theorem contraction_network_mod (S : List ℕ) (X : List Bool) (gs : List GateCode)
     (hgs : ∀ g ∈ gs, g.WellFormed X.length) {P : ℕ} (hP : hadamardCount gs < P) :
-    (network (2 ^ P - 1 : ℕ) X gs).2.contraction % 2 ^ P = (acceptGap gs X).toNat := by
-  obtain ⟨h0, h1⟩ := acceptGap_nonneg_and_le hX gs hgs
-  have hlt : (acceptGap gs X).toNat < 2 ^ P := by
-    have : (acceptGap gs X).toNat ≤ 2 ^ hadamardCount gs := Int.toNat_le.mpr (by exact_mod_cast h1)
+    (network (2 ^ P - 1 : ℕ) S X gs).2.contraction % 2 ^ P = (onesGap S gs X).toNat := by
+  obtain ⟨h0, h1⟩ := onesGap_nonneg_and_le S gs hgs
+  have hlt : (onesGap S gs X).toNat < 2 ^ P := by
+    have : (onesGap S gs X).toNat ≤ 2 ^ hadamardCount gs :=
+      Int.toNat_le.mpr (by exact_mod_cast h1)
     exact this.trans_lt (Nat.pow_lt_pow_right (by norm_num) hP)
-  have hcast : ((network (2 ^ P - 1 : ℕ) X gs).2.contraction : ZMod (2 ^ P)) =
-      ((acceptGap gs X).toNat : ZMod (2 ^ P)) := by
+  have hcast : ((network (2 ^ P - 1 : ℕ) S X gs).2.contraction : ZMod (2 ^ P)) =
+      ((onesGap S gs X).toNat : ZMod (2 ^ P)) := by
     have hneg : ((2 ^ P - 1 : ℕ) : ZMod (2 ^ P)) = -1 := by
       rw [Nat.cast_sub Nat.one_le_two_pow, ZMod.natCast_self, Nat.cast_one, zero_sub]
     rw [← Nat.coe_castRingHom, ExplicitTensorNetwork.map_contraction, network_mapTables,
-      Nat.coe_castRingHom, hneg, contraction_network X gs hgs, ← Int.toNat_of_nonneg h0]
+      Nat.coe_castRingHom, hneg, contraction_network S X gs hgs, ← Int.toNat_of_nonneg h0]
     simp
   rw [ZMod.natCast_eq_natCast_iff'] at hcast
   rw [hcast, Nat.mod_eq_of_lt hlt]
@@ -925,22 +927,23 @@ theorem length_occurrences_le {m : ℕ} {gs : List GateCode} (hgs : ∀ g ∈ gs
 
 variable {R : Type*} [Zero R] [One R]
 
-@[simp] theorem fst_network (neg : R) (X : List Bool) (gs : List GateCode) :
-    (network neg X gs).1 = 2 * gs.length + (occurrences gs).length + 1 := rfl
+@[simp] theorem fst_network (neg : R) (S : List ℕ) (X : List Bool) (gs : List GateCode) :
+    (network neg S X gs).1 = 2 * gs.length + (occurrences gs).length + 1 := rfl
 
 /-- **Four edges per occurrence.** -/
-@[simp] theorem numEdges_network (neg : R) (X : List Bool) (gs : List GateCode) :
-    (network neg X gs).2.numEdges = 2 * (2 * (occurrences gs).length) := rfl
+@[simp] theorem numEdges_network (neg : R) (S : List ℕ) (X : List Bool) (gs : List GateCode) :
+    (network neg S X gs).2.numEdges = 2 * (2 * (occurrences gs).length) := rfl
 
-theorem vertices_network (neg : R) (X : List Bool) (gs : List GateCode) :
-    (network neg X gs).2.vertices =
+theorem vertices_network (neg : R) (S : List ℕ) (X : List Bool) (gs : List GateCode) :
+    (network neg S X gs).2.vertices =
       (List.range gs.length).map (gateVertex neg X gs 0) ++
         (List.range gs.length).map (gateVertex neg X gs 1) ++
-        (List.range (occurrences gs).length).map (glueVertex gs) ++ [scalarVertex X gs] ++
+        (List.range (occurrences gs).length).map (glueVertex S gs) ++ [scalarVertex S X gs] ++
       (List.range (2 * (occurrences gs).length)).map fun w => ([2 * w, 2 * w + 1], eqTable) := rfl
 
-@[simp] theorem length_vertices_network (neg : R) (X : List Bool) (gs : List GateCode) :
-    (network neg X gs).2.vertices.length =
+@[simp] theorem length_vertices_network (neg : R) (S : List ℕ) (X : List Bool)
+    (gs : List GateCode) :
+    (network neg S X gs).2.vertices.length =
       2 * gs.length + 3 * (occurrences gs).length + 1 := by
   simp only [vertices_network, List.length_append, List.length_map, List.length_range,
     List.length_singleton]
@@ -948,8 +951,8 @@ theorem vertices_network (neg : R) (X : List Bool) (gs : List GateCode) :
 
 /-- **Degree at most six**: a gate vertex has at most two ports per qubit, and the other vertices
 at most two ports. -/
-theorem maxDegree_network_le (neg : R) (X : List Bool) {gs : List GateCode}
-    (hgs : ∀ g ∈ gs, (qubits g).length ≤ 3) : (network neg X gs).2.maxDegree ≤ 6 := by
+theorem maxDegree_network_le (neg : R) (S : List ℕ) (X : List Bool) {gs : List GateCode}
+    (hgs : ∀ g ∈ gs, (qubits g).length ≤ 3) : (network neg S X gs).2.maxDegree ≤ 6 := by
   refine (ExplicitTensorNetwork.maxDegree_le_iff _).mpr fun v hv => ?_
   simp only [vertices_network, List.mem_append, List.mem_map, List.mem_range,
     List.mem_singleton] at hv
@@ -964,9 +967,9 @@ theorem maxDegree_network_le (neg : R) (X : List Bool) {gs : List GateCode}
   · simp
 
 /-- **Full tables**: every table lists `2 ^ (number of ports)` entries. -/
-theorem length_table_network (neg : R) (X : List Bool) {gs : List GateCode}
+theorem length_table_network (neg : R) (S : List ℕ) (X : List Bool) {gs : List GateCode}
     (hgs : ∀ g ∈ gs, (qubits g).length ≤ 3) :
-    ∀ v ∈ (network neg X gs).2.vertices, v.2.length = 2 ^ v.1.length := by
+    ∀ v ∈ (network neg S X gs).2.vertices, v.2.length = 2 ^ v.1.length := by
   intro v hv
   simp only [vertices_network, List.mem_append, List.mem_map, List.mem_range,
     List.mem_singleton] at hv
@@ -1210,16 +1213,16 @@ private theorem count_gatePorts_link {gs : List GateCode} (i : ℕ)
     exact Or.inr ⟨_, hj, u, hw, rfl⟩
 
 /-- The glue vertices have only link edges among their ports. -/
-private theorem count_glueVertex_out (gs : List GateCode) (w v : ℕ) :
-    (glueVertex gs w : List ℕ × List R).1.count (2 * v) = 0 := by
+private theorem count_glueVertex_out (S : List ℕ) (gs : List GateCode) (w v : ℕ) :
+    (glueVertex S gs w : List ℕ × List R).1.count (2 * v) = 0 := by
   unfold glueVertex
   split_ifs <;> simp only [List.count_cons, List.count_nil, beq_iff_eq] <;> split_ifs <;> omega
 
 /-- The link edge of occurrence `u` in copy `c` is a port of the glue vertex of `w` exactly when
 `w = u` is the last occurrence of its qubit. -/
-private theorem count_glueVertex_link (gs : List GateCode) {w c u : ℕ}
+private theorem count_glueVertex_link (S : List ℕ) (gs : List GateCode) {w c u : ℕ}
     (hw : w < (occurrences gs).length) (hc : c < 2) (hu : u < (occurrences gs).length) :
-    (glueVertex gs w : List ℕ × List R).1.count (2 * (c * (occurrences gs).length + u) + 1) =
+    (glueVertex S gs w : List ℕ × List R).1.count (2 * (c * (occurrences gs).length + u) + 1) =
       if lastOcc (occurrences gs) ((occurrences gs).getD w 0) (occurrences gs).length = some w ∧
         w = u then 1 else 0 := by
   unfold glueVertex
@@ -1241,9 +1244,9 @@ private theorem sum_range_base (gs : List GateCode) {u : ℕ} (hu : u < (occurre
 
 /-- **The network is rows-first bipartite** with the gate, glue and scalar vertices as rows, when
 the qubits of every gate are distinct. -/
-theorem isRowsFirstBipartite_network (neg : R) (X : List Bool) {gs : List GateCode}
+theorem isRowsFirstBipartite_network (neg : R) (S : List ℕ) (X : List Bool) {gs : List GateCode}
     (hnd : ∀ g ∈ gs, (qubits g).Nodup) :
-    (network neg X gs).2.IsRowsFirstBipartite (network neg X gs).1 := by
+    (network neg S X gs).2.IsRowsFirstBipartite (network neg S X gs).1 := by
   have hnd' (i : ℕ) (hi : i ∈ List.range gs.length) : (qubits (gs.getD i default)).Nodup :=
     hnd _ (List.getD_eq_getElem _ default (List.mem_range.mp hi) ▸
       List.getElem_mem (List.mem_range.mp hi))
@@ -1297,7 +1300,7 @@ theorem isRowsFirstBipartite_network (neg : R) (X : List Bool) {gs : List GateCo
           (show 0 < 2 by omega) hu,
         List.map_congr_left fun i hi => count_gatePorts_link i (hnd' i hi) hc
           (show 1 < 2 by omega) hu,
-        List.map_congr_left fun w hw => count_glueVertex_link gs (List.mem_range.mp hw) hc hu,
+        List.map_congr_left fun w hw => count_glueVertex_link S gs (List.mem_range.mp hw) hc hu,
         List.sum_map_ite_and, List.sum_map_ite_and]
       have hglue : ((List.range (occurrences gs).length).map fun w =>
           if lastOcc (occurrences gs) ((occurrences gs).getD w 0) (occurrences gs).length =
diff --git a/Complexity/Computability/Circuit/Quantum/PathNetworkPolyTime.lean b/Complexity/Computability/Circuit/Quantum/PathNetworkPolyTime.lean
index 8c1d0379d..737167d55 100644
--- a/Complexity/Computability/Circuit/Quantum/PathNetworkPolyTime.lean
+++ b/Complexity/Computability/Circuit/Quantum/PathNetworkPolyTime.lean
@@ -18,6 +18,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary
 public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TakeDropUnary
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
@@ -32,8 +33,8 @@ import Complexity.Foundations.Data.List.FilterMap
 # The network of a circuit in polynomial time
 
 The network of a list of gate codes (`Cslib.Quantum.PathNetwork.network`) is computable in
-polynomial time from the gate codes, the input register and the Hadamard sign, with its number of
-rows in binary and the network in the encoding of the contraction algorithm
+polynomial time from the gate codes, the measured qubits, the input register and the Hadamard sign,
+with its number of rows in binary and the network in the encoding of the contraction algorithm
 (`ExplicitTensorNetwork.encExplicitNetwork`). Every port and last occurrence is a search or a map
 over the occurrences of qubits, written in unary, and every table is a map over the first `2 ^ 6`
 numbers, a constant list.
@@ -81,11 +82,11 @@ private theorem inBit_eq (X : List Bool) (gs : List GateCode) (c i idx : ℕ) :
   unfold inBit inPort
   cases lastOcc (occurrences gs) j (base gs i) <;> rfl
 
-private theorem scalarVertex_eq (X : List Bool) (gs : List GateCode) :
-    (scalarVertex X gs : List ℕ × List ℕ) =
-      ([], [if ((occurrences gs).any fun q => decide (q = 0)) || X.getD 0 false then 1
+private theorem scalarVertex_eq (S : List ℕ) (X : List Bool) (gs : List GateCode) :
+    (scalarVertex S X gs : List ℕ × List ℕ) =
+      ([], [if (S.all fun j => decide (j ∈ occurrences gs) || X.getD j false) then 1
         else 0]) := by
-  simp only [scalarVertex, List.any_eq_true, decide_eq_true_eq, exists_eq_right, Bool.or_eq_true]
+  simp only [scalarVertex, List.all_eq_true, Bool.or_eq_true, decide_eq_true_eq]
 
 /-- The encoding of networks is the encoding of their number of edges and vertices. -/
 private theorem computableInPolyTime_equivProd_symm :
@@ -194,8 +195,10 @@ theorem computableInPolyTime_gateVertex {neg : α → ℕ} {X : α → List Bool
       (allWithInput htl (snd _ _)))) htl)) (const 1) (const 0)
 
 /-- **Glue vertices are polynomial-time.** -/
-theorem computableInPolyTime_glueVertex {w : α → ℕ} (hw : ComputableInPolyTime w inp encUnary) :
-    ComputableInPolyTime (fun a => (glueVertex (gs a) (w a) : List ℕ × List ℕ)) inp
+theorem computableInPolyTime_glueVertex {S : α → List ℕ}
+    (hS : ComputableInPolyTime S inp (encList encUnary)) {w : α → ℕ}
+    (hw : ComputableInPolyTime w inp encUnary) :
+    ComputableInPolyTime (fun a => (glueVertex (S a) (gs a) (w a) : List ℕ × List ℕ)) inp
       (encPair (encList encNat) (encList encNat)) := by
   have hqs := computableInPolyTime_occurrences hgs
   have hN := (length_list _).comp hqs
@@ -204,27 +207,30 @@ theorem computableInPolyTime_glueVertex {w : α → ℕ} (hw : ComputableInPolyT
   refine ite_decide (decide_eq' (computableInPolyTime_lastOcc hqs hq hN) (optionSome _ |>.comp hw))
     ((ports_unary_to_binary (cons' (unary_add' (unary_mul' (const 2) hw) (const 1))
       (cons' (unary_add' (unary_mul' (const 2) (unary_add' hN hw)) (const 1)) (const [])))).prod
-      (ite_decide (decide_eq' hq (const 0)) (const _) (const _))) (const _)
+      (ite_decide (decide_mem hS hq) (const _) (const _))) (const _)
 
 end Vertices
 
 /-- **The scalar vertex is polynomial-time.** -/
-theorem computableInPolyTime_scalarVertex {X : α → List Bool} {gs : α → List GateCode}
+theorem computableInPolyTime_scalarVertex {S : α → List ℕ} {X : α → List Bool}
+    {gs : α → List GateCode} (hS : ComputableInPolyTime S inp (encList encUnary))
     (hX : ComputableInPolyTime X inp encBits)
     (hgs : ComputableInPolyTime gs inp (encList encGateCode)) :
-    ComputableInPolyTime (fun a => (scalarVertex (X a) (gs a) : List ℕ × List ℕ)) inp
+    ComputableInPolyTime (fun a => (scalarVertex (S a) (X a) (gs a) : List ℕ × List ℕ)) inp
       (encPair (encList encNat) (encList encNat)) := by
   simp only [scalarVertex_eq]
-  refine (const []).prod (cons' (ite_decide (decide_eq' (bool_or.comp
-    ((anyWithInput (computableInPolyTime_occurrences hgs) (decide_eq' (snd _ _) (const 0))).prod
-    (bitsGetDWithInput hX (const 0) false))) (const true)) (const 1) (const 0)) (const []))
-
-/-- **The network of a circuit is polynomial-time** in the gate codes, the input register and the
-Hadamard sign, with its number of rows in binary. -/
-theorem computableInPolyTime_network {neg : α → ℕ} {X : α → List Bool} {gs : α → List GateCode}
-    (hneg : ComputableInPolyTime neg inp encNat) (hX : ComputableInPolyTime X inp encBits)
+  refine (const []).prod (cons' (ite_decide (decide_eq' (allWithInput hS (bool_or.comp
+    ((decide_mem (computableInPolyTime_occurrences (hgs.comp (fst _ _))) (snd _ _)).prod
+    (bitsGetDWithInput (hX.comp (fst _ _)) (snd _ _) false)))) (const true)) (const 1) (const 0))
+    (const []))
+
+/-- **The network of a circuit is polynomial-time** in the gate codes, the measured qubits, the
+input register and the Hadamard sign, with its number of rows in binary. -/
+theorem computableInPolyTime_network {neg : α → ℕ} {S : α → List ℕ} {X : α → List Bool}
+    {gs : α → List GateCode} (hneg : ComputableInPolyTime neg inp encNat)
+    (hS : ComputableInPolyTime S inp (encList encUnary)) (hX : ComputableInPolyTime X inp encBits)
     (hgs : ComputableInPolyTime gs inp (encList encGateCode)) :
-    ComputableInPolyTime (fun a => network (neg a) (X a) (gs a)) inp
+    ComputableInPolyTime (fun a => network (neg a) (S a) (X a) (gs a)) inp
       (encPair encNat ExplicitTensorNetwork.encExplicitNetwork) := by
   have hL := (length_list _).comp hgs
   have hN := (length_list _).comp (computableInPolyTime_occurrences hgs)
@@ -236,15 +242,15 @@ theorem computableInPolyTime_network {neg : α → ℕ} {X : α → List Bool} {
   have hverts : ComputableInPolyTime (fun a =>
       (List.range (gs a).length).map (gateVertex (neg a) (X a) (gs a) 0) ++
         (List.range (gs a).length).map (gateVertex (neg a) (X a) (gs a) 1) ++
-        (List.range (occurrences (gs a)).length).map (glueVertex (gs a)) ++
-        [scalarVertex (X a) (gs a)] ++
+        (List.range (occurrences (gs a)).length).map (glueVertex (S a) (gs a)) ++
+        [scalarVertex (S a) (X a) (gs a)] ++
       (List.range (2 * (occurrences (gs a)).length)).map fun w =>
         (([2 * w, 2 * w + 1], eqTable) : List ℕ × List ℕ)) inp
       (encList (encPair (encList encNat) (encList encNat))) :=
     listAppend' (listAppend' (listAppend' (listAppend' (hgate 0) (hgate 1))
       (mapWithInput (range.comp hN) (computableInPolyTime_glueVertex (hgs.comp (fst _ _))
-        (snd _ _))))
-      (cons' (computableInPolyTime_scalarVertex hX hgs) (const [])))
+        (hS.comp (fst _ _)) (snd _ _))))
+      (cons' (computableInPolyTime_scalarVertex hS hX hgs) (const [])))
       (mapWithInput (range.comp (unary_mul' (const 2) hN))
         ((ports_unary_to_binary (cons' (unary_mul' (const 2) (snd _ _))
           (cons' (unary_add' (unary_mul' (const 2) (snd _ _)) (const 1)) (const [])))).prod
diff --git a/Complexity/Computability/Circuit/Quantum/PathSum.lean b/Complexity/Computability/Circuit/Quantum/PathSum.lean
index d2c2c2e73..ead1a98fb 100644
--- a/Complexity/Computability/Circuit/Quantum/PathSum.lean
+++ b/Complexity/Computability/Circuit/Quantum/PathSum.lean
@@ -28,22 +28,28 @@ Squaring and summing over the accepting outcomes, the acceptance probability is
 *pairs* of paths that end in the same accepting register, divided by `2^h`
 (`Cslib.Quantum.acceptProb_eq_acceptGap`). Both counts are integers computed from polynomial-time
 simulations, which places `BQP` in the counting classes
-(`Complexity/Computability/Complexity/Classes/BQP/Counting.lean`).
+(`Complexity/Computability/Complexity/Classes/BQP/Counting.lean`). The same holds for the
+probability that every qubit of a list `S` reads `1`, with the pairs of paths ending in the same
+register in which every qubit of `S` is one (`Cslib.Quantum.onesProb_eq_onesGap`); the acceptance
+gap is the case `S = [0]`.
 
 ## Main definitions
 
 * `Cslib.Quantum.pathStep`, `Cslib.Quantum.pathRun`: the path simulation.
 * `Cslib.Quantum.hadamardCount`: the number of Hadamard gates.
 * `Cslib.Quantum.pathTerm`, `Cslib.Quantum.pathGap`: the signed path count of an amplitude.
-* `Cslib.Quantum.acceptTerm`, `Cslib.Quantum.acceptGap`: the signed count of pairs of paths of the
-  acceptance probability.
+* `Cslib.Quantum.onesTerm`, `Cslib.Quantum.onesGap`: the signed count of pairs of paths of the
+  probability that every qubit of a list reads `1`.
+* `Cslib.Quantum.acceptGap`: its case of qubit `0`, for the acceptance probability.
 
 ## Main results
 
 * `Cslib.Quantum.ofFn_inputState`: the input basis state is the input word padded with zeros.
 * `Cslib.Quantum.run_ofCodes_apply`: amplitudes are path sums.
-* `Cslib.Quantum.acceptProb_eq_acceptGap`: the acceptance probability is `acceptGap / 2^h`.
-* `Cslib.Quantum.acceptGap_nonneg_and_le`: so the acceptance gap lies between `0` and `2^h`.
+* `Cslib.Quantum.onesProb_eq_onesGap`, `Cslib.Quantum.acceptProb_eq_acceptGap`: probabilities are
+  projected gaps over `2^h`.
+* `Cslib.Quantum.onesGap_nonneg_and_le`, `Cslib.Quantum.onesGap_nil_eq_two_pow`: so projected
+  gaps lie between `0` and `2^h`, with `2^h` for the empty list.
 * `Cslib.Quantum.acceptGap_nil`: the acceptance gap of the empty circuit is the bit of qubit `0`.
 
 ## References
@@ -117,21 +123,36 @@ def pathTerm (gs : List GateCode) (x y π : List Bool) : ℤ :=
 def pathGap (gs : List GateCode) (x y : List Bool) : ℤ :=
   ∑ π : Fin (hadamardCount gs) → Bool, pathTerm gs x y (List.ofFn π)
 
-/-- The signed contribution of a pair of paths to the acceptance probability: the product of
-their signs when both end in the same register with qubit `0` equal to one, and `0` otherwise. -/
-def acceptTerm (gs : List GateCode) (x π π' : List Bool) : ℤ :=
+/-- The signed contribution of a pair of paths to the probability that every qubit of `S` reads
+`1`: the product of their signs when both end in the same register with every qubit of `S` equal
+to one, and `0` otherwise. -/
+def onesTerm (S : List ℕ) (gs : List GateCode) (x π π' : List Bool) : ℤ :=
   match pathRun gs x π, pathRun gs x π' with
   | (s, σ), (s', σ') =>
-    if s = s' ∧ s.headD false = true then (if σ ^^ σ' then -1 else 1) else 0
+    if s = s' ∧ (S.all fun j => s.getD j false) = true then (if σ ^^ σ' then -1 else 1) else 0
 
-/-- The acceptance gap: the sum of `acceptTerm` over all pairs of paths. -/
-def acceptGap (gs : List GateCode) (x : List Bool) : ℤ :=
+/-- The **projected gap** of `S`: the sum of `onesTerm S` over all pairs of paths. -/
+def onesGap (S : List ℕ) (gs : List GateCode) (x : List Bool) : ℤ :=
   ∑ π : Fin (hadamardCount gs) → Bool, ∑ π' : Fin (hadamardCount gs) → Bool,
-    acceptTerm gs x (List.ofFn π) (List.ofFn π')
+    onesTerm S gs x (List.ofFn π) (List.ofFn π')
+
+/-- The acceptance gap: the projected gap of qubit `0`. -/
+def acceptGap (gs : List GateCode) (x : List Bool) : ℤ := onesGap [0] gs x
+
+/-- The contribution of a pair of paths to the acceptance gap: the product of their signs when both
+end in the same register with qubit `0` equal to one, and `0` otherwise. -/
+theorem onesTerm_zero (gs : List GateCode) (x π π' : List Bool) :
+    onesTerm [0] gs x π π' =
+      if (pathRun gs x π).1 = (pathRun gs x π').1 ∧ (pathRun gs x π).1.headD false = true then
+        (if (pathRun gs x π).2 ^^ (pathRun gs x π').2 then -1 else 1) else 0 := by
+  simp only [onesTerm, List.all_cons, List.all_nil, Bool.and_true]
+  generalize pathRun gs x π = r
+  obtain ⟨s, σ⟩ := r
+  cases s <;> rfl
 
 /-- The acceptance gap of the empty circuit is the bit of qubit `0`. -/
 theorem acceptGap_nil (x : List Bool) : acceptGap [] x = if x.headD false then 1 else 0 := by
-  simp only [acceptGap, hadamardCount_nil, acceptTerm,
+  simp only [acceptGap, onesGap, hadamardCount_nil, onesTerm_zero,
     pathRun, List.ofFn_zero, List.foldl_nil, true_and, Bool.xor_self, Bool.false_eq_true,
     ↓reduceIte]
   cases x.headD false <;> rfl
@@ -244,20 +265,21 @@ private theorem pathTerm_eq (gs : List GateCode) (x y π : List Bool) :
       if (pathRun gs x π).1 = y then (if (pathRun gs x π).2 then -1 else 1) else 0 :=
   rfl
 
-private theorem acceptTerm_eq (gs : List GateCode) (x π π' : List Bool) :
-    acceptTerm gs x π π' =
-      if (pathRun gs x π).1 = (pathRun gs x π').1 ∧ (pathRun gs x π).1.headD false = true then
+private theorem onesTerm_eq (S : List ℕ) (gs : List GateCode) (x π π' : List Bool) :
+    onesTerm S gs x π π' =
+      if (pathRun gs x π).1 = (pathRun gs x π').1 ∧
+          (S.all fun j => (pathRun gs x π).1.getD j false) = true then
         (if (pathRun gs x π).2 ^^ (pathRun gs x π').2 then -1 else 1) else 0 :=
   rfl
 
-/-- Summing the products of two path contributions over the accepting outcomes gives the
-contribution of the pair. -/
-private theorem sum_accepting_pathTerm_mul (hm : 0 < m) (gs : List GateCode) (x π π' : List Bool)
+/-- Summing the products of two path contributions over the outcomes in which every qubit of `S`
+reads `1` gives the contribution of the pair. -/
+private theorem sum_onesAt_pathTerm_mul (S : List ℕ) (gs : List GateCode) (x π π' : List Bool)
     (hx : x.length = m) :
-    ∑ y ∈ accepting m, pathTerm gs x (List.ofFn y) π * pathTerm gs x (List.ofFn y) π' =
-      acceptTerm gs x π π' := by
+    ∑ y ∈ onesAt m S, pathTerm gs x (List.ofFn y) π * pathTerm gs x (List.ofFn y) π' =
+      onesTerm S gs x π π' := by
   have hs : (pathRun gs x π).1.length = m := (length_foldl_pathStep gs x π false).trans hx
-  simp only [pathTerm_eq, acceptTerm_eq]
+  simp only [pathTerm_eq, onesTerm_eq]
   generalize pathRun gs x π = r at hs ⊢
   generalize pathRun gs x π' = r'
   obtain ⟨s, σ⟩ := r
@@ -271,14 +293,13 @@ private theorem sum_accepting_pathTerm_mul (hm : 0 < m) (gs : List GateCode) (x
   have hiff (y : Fin m → Bool) : s = List.ofFn y ↔ y = y₀ := by
     rw [hs₀, List.ofFn_inj, eq_comm]
   simp only [hiff, ite_mul, zero_mul]
-  rw [Finset.sum_ite_eq' (accepting m) y₀]
-  have hacc : y₀ ∈ accepting m ↔ s.headD false = true := by
-    rw [mem_accepting hm]
-    simp only [y₀]
-    cases s with
-    | nil => simp at hs; omega
-    | cons b s => rfl
-  by_cases h₀ : y₀ ∈ accepting m
+  rw [Finset.sum_ite_eq' (onesAt m S) y₀]
+  have hacc : y₀ ∈ onesAt m S ↔ (S.all fun j => s.getD j false) = true := by
+    simp only [onesAt, Finset.mem_filter, Finset.mem_univ, true_and, List.all_eq_true, y₀]
+    refine forall₂_congr fun j _ => ⟨fun ⟨_, h⟩ => h, fun h => ⟨?_, h⟩⟩
+    by_contra hj
+    simp [List.getD_eq_getElem?_getD, List.getElem?_eq_none (show s.length ≤ j by omega)] at h
+  by_cases h₀ : y₀ ∈ onesAt m S
   · simp only [h₀, ite_true, ← hs₀, hacc.mp h₀, and_true]
     by_cases hss : s = s'
     · subst hss
@@ -286,23 +307,24 @@ private theorem sum_accepting_pathTerm_mul (hm : 0 < m) (gs : List GateCode) (x
     · simp [hss, Ne.symm hss]
   · simp only [h₀, ite_false, mt hacc.mpr h₀, Bool.false_eq_true, and_false]
 
-/-- The squared amplitude gaps of the accepting outcomes sum to the acceptance gap. -/
-private theorem sum_accepting_pathGap_sq (hm : 0 < m) (gs : List GateCode) (x : List Bool)
+/-- The squared amplitude gaps of the outcomes in which every qubit of `S` reads `1` sum to the
+projected gap of `S`. -/
+private theorem sum_onesAt_pathGap_sq (S : List ℕ) (gs : List GateCode) (x : List Bool)
     (hx : x.length = m) :
-    ∑ y ∈ accepting m, pathGap gs x (List.ofFn y) ^ 2 = acceptGap gs x := by
-  simp only [pathGap, sq, Finset.sum_mul_sum, acceptGap]
+    ∑ y ∈ onesAt m S, pathGap gs x (List.ofFn y) ^ 2 = onesGap S gs x := by
+  simp only [pathGap, sq, Finset.sum_mul_sum, onesGap]
   rw [Finset.sum_comm]
   refine Finset.sum_congr rfl fun π _ => ?_
   rw [Finset.sum_comm]
-  exact Finset.sum_congr rfl fun π' _ => sum_accepting_pathTerm_mul hm gs x _ _ hx
+  exact Finset.sum_congr rfl fun π' _ => sum_onesAt_pathTerm_mul S gs x _ _ hx
 
-/-- **The acceptance probability is a gap over `2^h`**: for well-formed codes on `m > 0` qubits,
-the acceptance probability is `acceptGap` divided by `2^h`, where `h` counts the Hadamard
+/-- **Probabilities are projected gaps over `2^h`**: for well-formed codes, the probability that
+every qubit of `S` reads `1` is `onesGap S` divided by `2^h`, where `h` counts the Hadamard
 gates. -/
-theorem acceptProb_eq_acceptGap (hm : 0 < m) (gs : List GateCode)
-    (hgs : ∀ g ∈ gs, g.WellFormed m) (x : List Bool) :
-    acceptProb m gs x =
-      (acceptGap gs (List.ofFn (inputState m x)) : ℝ) / 2 ^ hadamardCount gs := by
+theorem onesProb_eq_onesGap (gs : List GateCode) (hgs : ∀ g ∈ gs, g.WellFormed m) (S : List ℕ)
+    (x : List Bool) :
+    onesProb m gs S x =
+      (onesGap S gs (List.ofFn (inputState m x)) : ℝ) / 2 ^ hadamardCount gs := by
   have hnorm (g : ℤ) :
       ‖(g : ℂ) * (((Real.sqrt 2)⁻¹ : ℝ) : ℂ) ^ hadamardCount gs‖ ^ 2 =
         (g : ℝ) ^ 2 / 2 ^ hadamardCount gs := by
@@ -310,20 +332,28 @@ theorem acceptProb_eq_acceptGap (hm : 0 < m) (gs : List GateCode)
       abs_of_nonneg (Real.sqrt_nonneg 2), Complex.norm_intCast, mul_pow, sq_abs, ← pow_mul,
       mul_comm (hadamardCount gs) 2, pow_mul, inv_pow, Real.sq_sqrt (by norm_num), inv_pow,
       div_eq_mul_inv]
-  rw [acceptProb, measureProb]
+  rw [onesProb, measureProb]
   simp only [run_ofCodes_apply gs hgs, hnorm, ← Finset.sum_div]
   congr 1
-  exact_mod_cast sum_accepting_pathGap_sq hm gs _ (by simp)
+  exact_mod_cast sum_onesAt_pathGap_sq S gs _ (by simp)
+
+/-- **The acceptance probability is a gap over `2^h`**: for well-formed codes on `m` qubits, the
+acceptance probability is `acceptGap` divided by `2^h`, where `h` counts the Hadamard gates. -/
+theorem acceptProb_eq_acceptGap (gs : List GateCode) (hgs : ∀ g ∈ gs, g.WellFormed m)
+    (x : List Bool) :
+    acceptProb m gs x =
+      (acceptGap gs (List.ofFn (inputState m x)) : ℝ) / 2 ^ hadamardCount gs := by
+  rw [acceptGap, acceptProb_eq_onesProb, onesProb_eq_onesGap gs hgs]
 
-/-- **The acceptance gap is a count between `0` and `2 ^ h`** for well-formed codes on a nonempty
-register `X`, since it is `2 ^ h` times a probability. -/
-theorem acceptGap_nonneg_and_le {X : List Bool} (hX : 0 < X.length) (gs : List GateCode)
+/-- **A projected gap is a count between `0` and `2 ^ h`** for well-formed codes on the register
+`X`, since it is `2 ^ h` times a probability. -/
+theorem onesGap_nonneg_and_le (S : List ℕ) {X : List Bool} (gs : List GateCode)
     (hgs : ∀ g ∈ gs, g.WellFormed X.length) :
-    0 ≤ acceptGap gs X ∧ acceptGap gs X ≤ 2 ^ hadamardCount gs := by
-  have h := acceptProb_eq_acceptGap hX gs hgs X
+    0 ≤ onesGap S gs X ∧ onesGap S gs X ≤ 2 ^ hadamardCount gs := by
+  have h := onesProb_eq_onesGap gs hgs S X
   rw [ofFn_inputState le_rfl, Nat.sub_self, List.replicate_zero, List.append_nil] at h
-  have h0 := acceptProb_nonneg X.length gs X
-  have h1 := acceptProb_le_one X.length gs X
+  have h0 := onesProb_nonneg X.length gs S X
+  have h1 := onesProb_le_one X.length gs S X
   have hpos : (0 : ℝ) < 2 ^ hadamardCount gs := by positivity
   rw [h] at h0 h1
   constructor
@@ -331,4 +361,13 @@ theorem acceptGap_nonneg_and_le {X : List Bool} (hX : 0 < X.length) (gs : List G
   · rw [div_le_one hpos] at h1
     exact_mod_cast h1
 
+/-- **The projected gap of no condition is `2 ^ h`**, the squared norm of the final state. -/
+theorem onesGap_nil_eq_two_pow {X : List Bool} (gs : List GateCode)
+    (hgs : ∀ g ∈ gs, g.WellFormed X.length) :
+    onesGap [] gs X = 2 ^ hadamardCount gs := by
+  have h := onesProb_eq_onesGap gs hgs [] X
+  rw [ofFn_inputState le_rfl, Nat.sub_self, List.replicate_zero, List.append_nil,
+    onesProb_nil, eq_div_iff (by positivity), one_mul] at h
+  exact_mod_cast h.symm
+
 end Cslib.Quantum
diff --git a/Complexity/Computability/Circuit/Quantum/Uniform.lean b/Complexity/Computability/Circuit/Quantum/Uniform.lean
index b612a5435..b1e274f3c 100644
--- a/Complexity/Computability/Circuit/Quantum/Uniform.lean
+++ b/Complexity/Computability/Circuit/Quantum/Uniform.lean
@@ -32,6 +32,11 @@ polynomially bounded. On an input word `x` the family runs its circuit for `n =
 `|x 0^{m - n}⟩` and accepts when the final measurement finds qubit `0` in state `1`
 (`Cslib.Quantum.UniformCircuitFamily.acceptProb`).
 
+Postselected classes condition on a second measured qubit: the postselected acceptance probability
+is the probability that qubit `0` reads `1` given that qubit `1` does
+(`Cslib.Quantum.UniformCircuitFamily.postselectedAcceptProb`), as in
+[Aaronson][Aaronson2005Postselection], Definition 1, with the two qubits exchanged.
+
 Appending a NOT gate on qubit `0` gives a family with complementary acceptance probability
 (`Cslib.Quantum.UniformCircuitFamily.appendNot`).
 
@@ -40,6 +45,9 @@ Appending a NOT gate on qubit `0` gives a family with complementary acceptance p
 * `Cslib.Quantum.encGateCode`: the encoding of gate codes.
 * `Cslib.Quantum.UniformCircuitFamily`: polynomial-time uniform families of circuits.
 * `Cslib.Quantum.UniformCircuitFamily.acceptProb`: the acceptance probability on an input word.
+* `Cslib.Quantum.UniformCircuitFamily.onesProb`,
+  `Cslib.Quantum.UniformCircuitFamily.postselectedAcceptProb`: the probability that measured qubits
+  read `1`, and the acceptance probability postselected on qubit `1`.
 * `Cslib.Quantum.UniformCircuitFamily.appendNot`: the family with a final NOT on qubit `0`.
 
 ## Main results
@@ -50,6 +58,8 @@ Appending a NOT gate on qubit `0` gives a family with complementary acceptance p
 ## References
 
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
+* [S. Aaronson, *Quantum computing, postselection, and probabilistic
+  polynomial-time*][Aaronson2005Postselection]
 -/
 
 @[expose] public section
@@ -90,6 +100,22 @@ theorem acceptProb_nonneg (F : UniformCircuitFamily) (x : List Bool) : 0 ≤ F.a
 theorem acceptProb_le_one (F : UniformCircuitFamily) (x : List Bool) : F.acceptProb x ≤ 1 :=
   Quantum.acceptProb_le_one _ _ _
 
+/-- The probability that the final measurement of the family's circuit on the input word `x` finds
+every qubit of `S` in state `1`. -/
+noncomputable def onesProb (F : UniformCircuitFamily) (S : List ℕ) (x : List Bool) : ℝ :=
+  Quantum.onesProb (F.width x.length) (F.gates x.length) S x
+
+theorem acceptProb_eq_onesProb (F : UniformCircuitFamily) (x : List Bool) :
+    F.acceptProb x = F.onesProb [0] x :=
+  rfl
+
+/-- The **postselected acceptance probability** of the family on the input word `x`: the
+probability that qubit `0` reads `1` conditioned on qubit `1` reading `1`, that is, the probability
+that both read `1` divided by the probability that qubit `1` does. It is `0` when qubit `1` never
+reads `1`. -/
+noncomputable def postselectedAcceptProb (F : UniformCircuitFamily) (x : List Bool) : ℝ :=
+  F.onesProb [0, 1] x / F.onesProb [1] x
+
 /-- The family with a final NOT gate on qubit `0`. -/
 def appendNot (F : UniformCircuitFamily) : UniformCircuitFamily where
   width := F.width
diff --git a/Complexity/Computability/Complexity/Classes/BQP/Counting.lean b/Complexity/Computability/Complexity/Classes/BQP/Counting.lean
index c931057a4..338ee4128 100644
--- a/Complexity/Computability/Complexity/Classes/BQP/Counting.lean
+++ b/Complexity/Computability/Complexity/Classes/BQP/Counting.lean
@@ -141,8 +141,8 @@ theorem acceptGap_mem_GapP (F : UniformCircuitFamily) :
   have hinner := GapP.sum_bits_mem hT (r := fun p : α × List Bool => h p.1) (by fun_prop)
   have houter := GapP.sum_bits_mem hinner hh
   convert houter using 2 with a
-  rw [ofFn_inputState (F.le_width _)]
-  rfl
+  rw [ofFn_inputState (F.le_width _), acceptGap, onesGap]
+  exact Finset.sum_congr rfl fun π _ => Finset.sum_congr rfl fun π' _ => onesTerm_zero _ _ _ _
 
 /-- **`BQP ⊆ AWPP`** [Fortnow, Rogers][FortnowRogers1999]: the acceptance probability of a uniform
 family is a `GapP` function divided by `2^h`, with `h` computed in polynomial time. -/
@@ -154,8 +154,7 @@ theorem BQP_subset_AWPP : BQP enc ⊆ AWPP enc := by
       have := F.computableInPolyTime_gates
       simp only [hadamardCount_eq_countP]
       fun_prop) (fun a => ?_)
-  have hp := acceptProb_eq_acceptGap (F.width_pos (enc a).length) _
-    (F.wellFormed (enc a).length) (enc a)
+  have hp := acceptProb_eq_acceptGap _ (F.wellFormed (enc a).length) (enc a)
   set g := acceptGap (F.gates (enc a).length)
     (List.ofFn (inputState (F.width (enc a).length) (enc a)))
   set r := hadamardCount (F.gates (enc a).length)
diff --git a/Complexity/Computability/Complexity/Classes/BQP/TensorContraction.lean b/Complexity/Computability/Complexity/Classes/BQP/TensorContraction.lean
index 8af90ccfd..021d3df69 100644
--- a/Complexity/Computability/Complexity/Classes/BQP/TensorContraction.lean
+++ b/Complexity/Computability/Complexity/Classes/BQP/TensorContraction.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Circuit.Quantum.PathNetworkPolyTime
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves
 public import Complexity.Computability.Complexity.Classes.Time
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
+import Complexity.Computability.GenericRAM.Native.ExpTimePolySpace
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
@@ -23,13 +24,14 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFr
 import Complexity.Foundations.Data.Nat.SqrtLog.Linear
 
 /-!
-# Quantum circuits by tensor contraction: `BQTIME[T] ⊆ DTIME[2 ^ O(T / √log T)]`
-
-The acceptance probability of a circuit of `L` gates over the Hadamard, NOT, CNOT and Toffoli gates
-is `acceptGap / 2 ^ h`, where `h` is the number of Hadamard gates
-(`Cslib.Quantum.acceptProb_eq_acceptGap`). The acceptance gap is the contraction of the network of
-the circuit and its mirror copy (`Cslib.Quantum.PathNetwork.contraction_network`), and over `ℕ`,
-with the Hadamard sign `2 ^ (h + 1) - 1`, its residue modulo `2 ^ (h + 1)`
+# Quantum circuits by tensor contraction: quantum time `T` in `DTIME[2 ^ O(T / √log T)]`
+
+The probability that the final measurement of a circuit of `L` gates over the Hadamard, NOT, CNOT
+and Toffoli gates finds every qubit of a list `S` in state `1` is `onesGap S / 2 ^ h`, where `h` is
+the number of Hadamard gates (`Cslib.Quantum.onesProb_eq_onesGap`); acceptance is the case
+`S = [0]`. The projected gap is the contraction of the network of the circuit and its mirror copy
+(`Cslib.Quantum.PathNetwork.contraction_network`), and over `ℕ`, with the Hadamard sign
+`2 ^ (h + 1) - 1`, its residue modulo `2 ^ (h + 1)`
 (`Cslib.Quantum.PathNetwork.contraction_network_mod`). The network has `s = 4 N` edges for
 `N ≤ 3 L` occurrences of qubits in gates, degree at most six and a bipartition, so it is admissible
 for the contraction algorithm of Theorem D.1 of [OpenAI2026ETH]
@@ -37,35 +39,52 @@ for the contraction algorithm of Theorem D.1 of [OpenAI2026ETH]
 `2 ^ O(s / √⌊log₂ s⌋)` times a polynomial and in polynomial space. The width of the circuit does
 not enter the exponent: qubits that no gate touches cost nothing.
 
-So the acceptance gap of polynomial-time computed circuits is computed by one machine in time
+So the projected gaps of polynomial-time computed circuits are computed by one machine in time
 `2 ^ (A (L + 1) / √⌊log₂ (L + 2)⌋)` times a polynomial in the input length, and in polynomial space
-(`QuantumContraction.exists_computableInO_gapValue`). For a uniform family with `O(T)` gates this
-decides the problem of the family: `BQTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]` for
-`max n 2 ≤ T n`, with a joint polynomial space bound `T ^ d`
-(`QuantumContraction.BQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`,
-`QuantumContraction.exists_decidableInTimeAndSpace_of_mem_BQTIME`). No time-constructibility of
-`T` is needed, since the machine never computes `T`. The novelty of this bound has not been
-checked against the literature.
+(`QuantumContraction.exists_computableInO_gapValue`), and so is any polynomial-time rule applied to
+two of them (`QuantumContraction.exists_computableInO_rule`). The gaps are exact, so a rule can
+test a probability for zero or compare two probabilities. For a uniform family with `O(T)` gates
+and `max n 2 ≤ T n`, a problem decided by such a rule lies in `⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`,
+with a joint polynomial space bound `T ^ d`
+(`QuantumContraction.exists_decidableInTimeAndSpace_of_onesProb`):
+
+* `BQTIME[T]`: the acceptance gap `g` against the gap `2 ^ h` of no condition, `2 ^ h < 2 g`;
+* `NQTIME[T]`: the acceptance gap is positive;
+* `EQTIME[T]`, which lies in `NQTIME[T]`;
+* `PostBQTIME[T]`: the gap `g` of qubits `0` and `1` against the gap `g'` of qubit `1`, `g' < 2 g`.
+
+No time-constructibility of `T` is needed, since the machine never computes `T`. The textbook
+characterizations `NQP = coC₌P` [FennerGreenHomerPruim1999] and `PostBQP = PP`
+[Aaronson2005Postselection] would lose a polynomial in `T`. The novelty of these bounds has not
+been established; a limited search found no direct simulation of these classes in this time.
 
 ## Main definitions
 
-* `Cslib.Complexity.QuantumContraction.gapValue`: the acceptance gap as the simulator computes
-  it.
+* `Cslib.Complexity.QuantumContraction.gapValue`: the projected gap as the simulator computes it.
 
 ## Main results
 
 * `Cslib.Quantum.PathNetwork.explicitAdmissible_network`: the network is admissible.
-* `Cslib.Complexity.QuantumContraction.gapValue_eq`: the simulator computes the acceptance gap.
-* `Cslib.Complexity.QuantumContraction.exists_computableInO_rule`,
-  `Cslib.Complexity.QuantumContraction.exists_computableInO_gapValue`: the simulator and its
+* `Cslib.Complexity.QuantumContraction.gapValue_eq`: the simulator computes the projected gap.
+* `Cslib.Complexity.QuantumContraction.exists_computableInO_gapValue`,
+  `Cslib.Complexity.QuantumContraction.exists_computableInO_rule`: the simulator and its
   resources.
-* `Cslib.Complexity.QuantumContraction.exists_decidableInTimeAndSpace_of_mem_BQTIME`,
-  `Cslib.Complexity.QuantumContraction.BQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`: the
-  class containments.
+* `Cslib.Complexity.QuantumContraction.exists_decidableInTimeAndSpace_of_onesProb`: deciding by two
+  projected gaps.
+* `Cslib.Complexity.QuantumContraction.BQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`,
+  `Cslib.Complexity.QuantumContraction.NQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`,
+  `Cslib.Complexity.QuantumContraction.EQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`,
+  `Cslib.Complexity.QuantumContraction.PostBQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`,
+  with the joint forms `exists_decidableInTimeAndSpace_of_mem_BQTIME`, `…_NQTIME` and
+  `…_PostBQTIME`: the class containments.
 
 ## References
 
 * [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53).
+* [S. Fenner, F. Green, S. Homer, R. Pruim, *Determining acceptance possibility for a quantum
+  computation is hard for the polynomial hierarchy*][FennerGreenHomerPruim1999]
+* [S. Aaronson, *Quantum computing, postselection, and probabilistic
+  polynomial-time*][Aaronson2005Postselection]
 -/
 
 public section
@@ -81,19 +100,19 @@ theorem nodup_qubits {m : ℕ} {g : GateCode} (h : g.WellFormed m) : (qubits g).
   · simp [qubits, h.2]
 
 /-- **The network is admissible** at size `4 N`, its number of edges, with constant `6`, for a
-nonempty list of well-formed gate codes. -/
-theorem explicitAdmissible_network (neg : ℕ) (X : List Bool) {gs : List GateCode}
+nonempty list of well-formed gate codes and any measured qubits. -/
+theorem explicitAdmissible_network (neg : ℕ) (S : List ℕ) (X : List Bool) {gs : List GateCode}
     (hgs : ∀ g ∈ gs, g.WellFormed X.length) (hne : gs ≠ []) :
-    ExplicitAdmissible 6 (4 * (occurrences gs).length) (network neg X gs) := by
+    ExplicitAdmissible 6 (4 * (occurrences gs).length) (network neg S X gs) := by
   have h3 : ∀ g ∈ gs, (qubits g).length ≤ 3 := fun g hg => length_qubits_le_three (hgs g hg)
   have hL : 1 ≤ gs.length := List.length_pos_iff.mpr hne
   have hLN := length_le_length_occurrences gs
   have hlog : 1 ≤ Nat.log 2 (4 * (occurrences gs).length) := Nat.log_pos (by norm_num) (by omega)
-  refine ⟨isRowsFirstBipartite_network neg X fun g hg => nodup_qubits (hgs g hg), ?_, ?_, ?_,
-    length_table_network neg X h3, ?_⟩
+  refine ⟨isRowsFirstBipartite_network neg S X fun g hg => nodup_qubits (hgs g hg), ?_, ?_, ?_,
+    length_table_network neg S X h3, ?_⟩
   · rw [numEdges_network]
     omega
-  · exact (maxDegree_network_le neg X h3).trans (by omega)
+  · exact (maxDegree_network_le neg S X h3).trans (by omega)
   · rw [length_vertices_network]
     omega
   · rw [numEdges_network]
@@ -112,35 +131,35 @@ open Quantum Quantum.PathNetwork Cslib.Circuits.Frontier Turing.MultiTapeTM Csli
 @[expose] def guard (gs : List GateCode) : Bool := !gs.isEmpty
 
 /-- The input of the contraction algorithm: the precision `h + 1`, for `h` Hadamard gates, and the
-network with Hadamard sign `2 ^ (h + 1) - 1` on the input register `X`. -/
-@[expose] def contractionInput (gs : List GateCode) (X : List Bool) :
+network with the measured qubits `S` and Hadamard sign `2 ^ (h + 1) - 1` on the input register
+`X`. -/
+@[expose] def contractionInput (S : List ℕ) (gs : List GateCode) (X : List Bool) :
     ℕ × ℕ × ExplicitTensorNetwork ℕ :=
-  (hadamardCount gs + 1, network (2 ^ (hadamardCount gs + 1) - 1 : ℕ) X gs)
+  (hadamardCount gs + 1, network (2 ^ (hadamardCount gs + 1) - 1 : ℕ) S X gs)
 
-/-- The answer for a circuit without gates: the bit of qubit `0`. -/
-@[expose] def fallback (X : List Bool) : ℕ := if X.getD 0 false then 1 else 0
+/-- The answer for a circuit without gates: whether every qubit of `S` reads one in `X`. -/
+@[expose] def fallback (S : List ℕ) (X : List Bool) : ℕ :=
+  if S.all fun j => X.getD j false then 1 else 0
 
-/-- **The acceptance gap as the simulator computes it**: the residue of the contraction of the
-network modulo `2 ^ (h + 1)`, or the bit of qubit `0` for a circuit without gates. -/
-@[expose] def gapValue (gs : List GateCode) (X : List Bool) : ℕ :=
+/-- **The projected gap as the simulator computes it**: the residue of the contraction of the
+network modulo `2 ^ (h + 1)`, or the bits of the qubits of `S` for a circuit without gates. -/
+@[expose] def gapValue (S : List ℕ) (gs : List GateCode) (X : List Bool) : ℕ :=
   if guard gs then
-    let (precision, _, network) := contractionInput gs X
+    let (precision, _, network) := contractionInput S gs X
     network.contraction % 2 ^ precision
-  else fallback X
+  else fallback S X
 
-/-- **The simulator computes the acceptance gap** of well-formed gate codes on a nonempty input
-register. -/
-theorem gapValue_eq {X : List Bool} (hX : 0 < X.length) {gs : List GateCode}
-    (hgs : ∀ g ∈ gs, g.WellFormed X.length) : gapValue gs X = (acceptGap gs X).toNat := by
+/-- **The simulator computes the projected gap** of well-formed gate codes on the register `X`. -/
+theorem gapValue_eq (S : List ℕ) {X : List Bool} {gs : List GateCode}
+    (hgs : ∀ g ∈ gs, g.WellFormed X.length) : gapValue S gs X = (onesGap S gs X).toNat := by
   unfold gapValue
   split
-  · exact contraction_network_mod X hX gs hgs (Nat.lt_succ_self _)
+  · exact contraction_network_mod S X gs hgs (Nat.lt_succ_self _)
   · next hg =>
     obtain rfl : gs = [] := by simpa [guard] using hg
-    rw [acceptGap_nil, fallback]
-    cases X with
-    | nil => rfl
-    | cons b X => cases b <;> rfl
+    simp only [fallback, onesGap, hadamardCount_nil, onesTerm, pathRun, List.ofFn_zero,
+      List.foldl_nil, true_and, Bool.xor_self, Bool.false_eq_true, ↓reduceIte]
+    split <;> rfl
 
 /-! ### Resources -/
 
@@ -162,20 +181,17 @@ section Machine
 
 variable {α : Type} {enc : α ↪ List Bool} {gs : α → List GateCode} {X : α → List Bool}
 
-/-- **The simulator with polynomial-time postprocessing.** For polynomial-time computed gate codes
-`gs a`, well formed on the polynomial-time computed register `X a`, one machine computes
-`rule (h, gapValue (gs a) (X a))`, for `h` the number of Hadamard gates and a polynomial-time
-`rule`, in time `2 ^ (A (L + 1) / √⌊log₂ (L + 2)⌋)` times a polynomial in the input length and in
-polynomial space, where `L` is the number of gates. -/
-theorem exists_computableInO_rule (hgs : ComputableInPolyTime gs enc (encList encGateCode))
-    (hX : ComputableInPolyTime X enc encBits) (hwf : ∀ a, ∀ g ∈ gs a, g.WellFormed (X a).length)
-    {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β}
-    (hrule : ComputableInPolyTime rule (encPair encUnary encNat) encβ) :
-    ∃ A e : ℕ, ComputableInO (fun a => rule (hadamardCount (gs a), gapValue (gs a) (X a))) enc
-      encβ
-      (fun a => 2 ^ (A * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) *
-        ((enc a).length + 1) ^ e)
-      (fun a => ((enc a).length + 1) ^ e) := by
+/-- **The simulator as a certificate**: for polynomial-time computed measured qubits `S a` and
+gate codes `gs a`, well formed on the polynomial-time computed register `X a`, the projected gap
+is computed in time `2 ^ (A (L + 1) / √⌊log₂ (L + 2)⌋)` times a polynomial and in polynomial
+space. -/
+private theorem exists_expTimePolySpace_gapValue {S : α → List ℕ}
+    (hS : ComputableInPolyTime S enc (encList encUnary))
+    (hgs : ComputableInPolyTime gs enc (encList encGateCode))
+    (hX : ComputableInPolyTime X enc encBits) (hwf : ∀ a, ∀ g ∈ gs a, g.WellFormed (X a).length) :
+    ∃ (A : ℕ) (c : NativeCertificate (fun a => gapValue (S a) (gs a) (X a)) enc encNat),
+      c.ExpTimePolySpace fun a =>
+        A * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2)) := by
   obtain ⟨K, hK⟩ := fastContractionAlgorithm.bound 6 1
   -- the polynomial-time parts
   have hh : ComputableInPolyTime (fun a => hadamardCount (gs a)) enc encUnary := by
@@ -184,46 +200,45 @@ theorem exists_computableInO_rule (hgs : ComputableInPolyTime gs enc (encList en
   have hguard : ComputableInPolyTime (fun a => guard (gs a)) enc encBool := by
     unfold guard
     fun_prop
-  have hinput : ComputableInPolyTime (fun a => contractionInput (gs a) (X a)) enc
+  have hinput : ComputableInPolyTime (fun a => contractionInput (S a) (gs a) (X a)) enc
       (encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork)) :=
     (unary_to_binary.comp (unary_add' hh (const 1))).prod (computableInPolyTime_network
-      (binary_sub' (binary_pow' (const 2) (unary_add' hh (const 1)))
-        (const 1)) hX hgs)
-  have hfb : ComputableInPolyTime (fun a => fallback (X a)) enc encNat :=
-    ite_decide (decide_eq' (bitsGetDWithInput hX (const 0) false) (const true)) (const 1) (const 0)
+      (binary_sub' (binary_pow' (const 2) (unary_add' hh (const 1))) (const 1)) hS hX hgs)
+  have hfb : ComputableInPolyTime (fun a => fallback (S a) (X a)) enc encNat :=
+    ite_decide (decide_eq' (allWithInput hS (bitsGetDWithInput (hX.comp (fst _ _)) (snd _ _)
+      false)) (const true)) (const 1) (const 0)
   -- the machine
-  let cv : NativeCertificate (fun a => gapValue (gs a) (X a)) enc encNat :=
+  let cv : NativeCertificate (fun a => gapValue (S a) (gs a) (X a)) enc encNat :=
     (NativeCertificate.branch (NativeCertificate.ofPolyTime hguard)
       (fastContractionAlgorithm.certificate.comp (NativeCertificate.ofPolyTime hinput))
       (NativeCertificate.ofPolyTime hfb)).congr fun _ => rfl
-  let cpair := (NativeCertificate.ofPolyTime hh).prod cv
-  let ctotal := (NativeCertificate.ofPolyTime hrule).comp cpair
+  refine ⟨12 * K, cv, ?_⟩
   -- polynomial bounds
   have hpg := NativeCertificate.ofPolyTime_isPolynomial hguard
   have hpi := NativeCertificate.ofPolyTime_isPolynomial hinput
   have hpf := NativeCertificate.ofPolyTime_isPolynomial hfb
-  have hph := NativeCertificate.ofPolyTime_isPolynomial hh
-  have hpr := NativeCertificate.ofPolyTime_isPolynomial hrule
   obtain ⟨cg, dg, htg⟩ := hpg.1.exists_le
   obtain ⟨cg', dg', hsg⟩ := hpg.2.exists_le
   obtain ⟨ci, di, hti⟩ := hpi.1.exists_le
   obtain ⟨ci', di', hsi⟩ := hpi.2.exists_le
   obtain ⟨cf, df, htf⟩ := hpf.1.exists_le
   obtain ⟨cf', df', hsf⟩ := hpf.2.exists_le
-  obtain ⟨ch, dh, hth⟩ := hph.1.exists_le
-  obtain ⟨ch', dh', hsh⟩ := hph.2.exists_le
-  obtain ⟨cr, dr, htr⟩ := hpr.1.exists_le
-  obtain ⟨cr', dr', hsr⟩ := hpr.2.exists_le
   obtain ⟨p, q, hlen⟩ := hinput.polyBounded_length.exists_le
   -- the contraction on guarded inputs
+  have hinlen (a : α) : (((encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork))
+      (contractionInput (S a) (gs a) (X a))).length + 1) ^ K ≤
+        (p + 1) ^ K * ((enc a).length + 1) ^ (q * K) := by
+    have h1 := hlen a
+    have h2 : 1 ≤ ((enc a).length + 1) ^ q := Nat.one_le_pow _ _ (Nat.le_add_left 1 _)
+    calc _ ≤ ((p + 1) * ((enc a).length + 1) ^ q) ^ K := Nat.pow_le_pow_left (by nlinarith) K
+      _ = _ := by rw [mul_pow, pow_mul]
   have hfast (a : α) (hga : guard (gs a) = true) :
-      fastContractionAlgorithm.certificate.time (contractionInput (gs a) (X a)) ≤
-          K * (((encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork))
-            (contractionInput (gs a) (X a))).length + 1) ^ K *
-            2 ^ (12 * K * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) ∧
-        fastContractionAlgorithm.certificate.space (contractionInput (gs a) (X a)) ≤
-          K * (((encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork))
-            (contractionInput (gs a) (X a))).length + 1) ^ K := by
+      fastContractionAlgorithm.certificate.time (contractionInput (S a) (gs a) (X a)) ≤
+          K * (p + 1) ^ K *
+            (2 ^ (12 * K * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) *
+              ((enc a).length + 1) ^ (q * K)) ∧
+        fastContractionAlgorithm.certificate.space (contractionInput (S a) (gs a) (X a)) ≤
+          K * (p + 1) ^ K * ((enc a).length + 1) ^ (q * K) := by
     have hne : gs a ≠ [] := by simpa [guard] using hga
     have hL : 1 ≤ (gs a).length := List.length_pos_iff.mpr hne
     have hLN := length_le_length_occurrences (gs a)
@@ -231,177 +246,148 @@ theorem exists_computableInO_rule (hgs : ComputableInPolyTime gs enc (encList en
       rw [hadamardCount_eq_countP]
       exact List.countP_le_length
     have hb := hK (4 * (occurrences (gs a)).length) (hadamardCount (gs a) + 1)
-      (network (2 ^ (hadamardCount (gs a) + 1) - 1 : ℕ) (X a) (gs a)) (by omega) (by omega)
-      (by omega) (explicitAdmissible_network _ (X a) (hwf a) hne)
-    exact ⟨hb.1.trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num)
-      (exponent_le K (hwf a) hne))), hb.2⟩
-  -- the space of the pair, and so the length of its output
-  set ds := dg' + di' + df' + dh' + q * K
-  set CS := cg' + ci' + cf' + ch' + K * (p + 1) ^ K
-  have hY {a : α} {d d' : ℕ} (h : d ≤ d') :
-      ((enc a).length + 1) ^ d ≤ ((enc a).length + 1) ^ d' :=
-    Nat.pow_le_pow_right (Nat.le_add_left 1 _) h
-  have hinlen (a : α) : (((encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork))
-      (contractionInput (gs a) (X a))).length + 1) ^ K ≤
-        (p + 1) ^ K * ((enc a).length + 1) ^ (q * K) := by
-    have h1 := hlen a
-    have h2 : 1 ≤ ((enc a).length + 1) ^ q := Nat.one_le_pow _ _ (Nat.le_add_left 1 _)
-    calc _ ≤ ((p + 1) * ((enc a).length + 1) ^ q) ^ K := Nat.pow_le_pow_left (by nlinarith) K
-      _ = _ := by rw [mul_pow, pow_mul]
-  have hspace_pair (a : α) : cpair.space a ≤ CS * ((enc a).length + 1) ^ ds := by
-    have e1 := (hsh a).trans (Nat.mul_le_mul_left ch' (hY (a := a) (show dh' ≤ ds by omega)))
-    have e2 := (hsg a).trans (Nat.mul_le_mul_left cg' (hY (a := a) (show dg' ≤ ds by omega)))
-    have e3 := (hsi a).trans (Nat.mul_le_mul_left ci' (hY (a := a) (show di' ≤ ds by omega)))
-    have e4 := (hsf a).trans (Nat.mul_le_mul_left cf' (hY (a := a) (show df' ≤ ds by omega)))
-    change (NativeCertificate.ofPolyTime hh).space a +
-        ((NativeCertificate.ofPolyTime hguard).space a + if guard (gs a) then
-          (NativeCertificate.ofPolyTime hinput).space a +
-            fastContractionAlgorithm.certificate.space (contractionInput (gs a) (X a))
-          else (NativeCertificate.ofPolyTime hfb).space a) ≤ _
-    split
-    · next hga =>
-      have e5 := ((hfast a hga).2.trans (Nat.mul_le_mul_left K (hinlen a))).trans
-        (show K * ((p + 1) ^ K * ((enc a).length + 1) ^ (q * K)) ≤
-          K * (p + 1) ^ K * ((enc a).length + 1) ^ ds by
-            rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_left _ (hY (by omega)))
-      calc _ ≤ ch' * ((enc a).length + 1) ^ ds + (cg' * ((enc a).length + 1) ^ ds +
-            (ci' * ((enc a).length + 1) ^ ds + K * (p + 1) ^ K * ((enc a).length + 1) ^ ds)) :=
-            Nat.add_le_add e1 (Nat.add_le_add e2 (Nat.add_le_add e3 e5))
-        _ = (ch' + cg' + ci' + K * (p + 1) ^ K) * ((enc a).length + 1) ^ ds := by ring
-        _ ≤ _ := Nat.mul_le_mul_right _ (by simp only [CS]; omega)
-    · calc _ ≤ ch' * ((enc a).length + 1) ^ ds + (cg' * ((enc a).length + 1) ^ ds +
-            cf' * ((enc a).length + 1) ^ ds) := Nat.add_le_add e1 (Nat.add_le_add e2 e4)
-        _ = (ch' + cg' + cf') * ((enc a).length + 1) ^ ds := by ring
-        _ ≤ _ := Nat.mul_le_mul_right _ (by simp only [CS]; omega)
-  obtain ⟨K₀, -, hK₀⟩ := cpair.computes
-  -- the postprocessing
-  set CR := K₀ * CS + K₀ + 1
-  have hpairlen (a : α) : (encPair encUnary encNat
-      (hadamardCount (gs a), gapValue (gs a) (X a))).length + 1 ≤
-        CR * ((enc a).length + 1) ^ ds := by
-    have h1 := hK₀ a
-    have h2 := hspace_pair a
-    have h3 : 1 ≤ ((enc a).length + 1) ^ ds := Nat.one_le_pow _ _ (Nat.le_add_left 1 _)
-    change _ ≤ K₀ * (cpair.space a + 1) at h1
-    simp only [CR]
-    nlinarith
-  have hrule_time (a : α) : (NativeCertificate.ofPolyTime hrule).time
-      (hadamardCount (gs a), gapValue (gs a) (X a)) ≤
-        cr * CR ^ dr * ((enc a).length + 1) ^ (ds * dr) := by
-    refine (htr _).trans ?_
-    calc _ ≤ cr * (CR * ((enc a).length + 1) ^ ds) ^ dr :=
-          Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (hpairlen a) dr)
-      _ = _ := by rw [mul_pow, ← pow_mul]; ring
-  have hrule_space (a : α) : (NativeCertificate.ofPolyTime hrule).space
-      (hadamardCount (gs a), gapValue (gs a) (X a)) ≤
-        cr' * CR ^ dr' * ((enc a).length + 1) ^ (ds * dr') := by
-    refine (hsr _).trans ?_
-    calc _ ≤ cr' * (CR * ((enc a).length + 1) ^ ds) ^ dr' :=
-          Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (hpairlen a) dr')
-      _ = _ := by rw [mul_pow, ← pow_mul]; ring
+      (network (2 ^ (hadamardCount (gs a) + 1) - 1 : ℕ) (S a) (X a) (gs a)) (by omega) (by omega)
+      (by omega) (explicitAdmissible_network _ (S a) (X a) (hwf a) hne)
+    constructor
+    · refine hb.1.trans ?_
+      calc _ ≤ K * ((p + 1) ^ K * ((enc a).length + 1) ^ (q * K)) *
+            2 ^ (12 * K * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) :=
+            Nat.mul_le_mul (Nat.mul_le_mul_left _ (hinlen a))
+              (Nat.pow_le_pow_right (by norm_num) (exponent_le K (hwf a) hne))
+        _ = _ := by ring
+    · exact hb.2.trans ((Nat.mul_le_mul_left K (hinlen a)).trans (Nat.mul_assoc _ _ _).ge)
   -- the totals
-  set e := dg + di + df + dh + q * K + ds * dr + ds * dr' + ds
-  set k := cg + ci + cf + ch + K * (p + 1) ^ K + cr * CR ^ dr + CS + cr' * CR ^ dr' + 1
-  refine ⟨12 * K, e, ctotal.computes.mono k (fun a => ?_) (fun a => ?_)⟩
-  · -- time
-    set E := 12 * K * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))
-    set Z := 2 ^ E * ((enc a).length + 1) ^ e
-    have hZ {d : ℕ} (h : d ≤ e) : ((enc a).length + 1) ^ d ≤ Z :=
-      (hY h).trans (Nat.le_mul_of_pos_left _ Nat.one_le_two_pow)
-    have e1 := (hth a).trans (Nat.mul_le_mul_left ch (hZ (show dh ≤ e by omega)))
-    have e2 := (htg a).trans (Nat.mul_le_mul_left cg (hZ (show dg ≤ e by omega)))
-    have e3 := (hti a).trans (Nat.mul_le_mul_left ci (hZ (show di ≤ e by omega)))
-    have e4 := (htf a).trans (Nat.mul_le_mul_left cf (hZ (show df ≤ e by omega)))
-    have e6 := (hrule_time a).trans (Nat.mul_le_mul_left _ (hZ (show ds * dr ≤ e by omega)))
-    change (NativeCertificate.ofPolyTime hh).time a +
-        ((NativeCertificate.ofPolyTime hguard).time a + if guard (gs a) then
-          (NativeCertificate.ofPolyTime hinput).time a +
-            fastContractionAlgorithm.certificate.time (contractionInput (gs a) (X a))
-          else (NativeCertificate.ofPolyTime hfb).time a) +
-        (NativeCertificate.ofPolyTime hrule).time
-          (hadamardCount (gs a), gapValue (gs a) (X a)) ≤ k * (Z + 1)
-    have hk : ∀ c, c ≤ k → c * Z ≤ k * (Z + 1) := fun c hc =>
-      (Nat.mul_le_mul_right _ hc).trans (Nat.mul_le_mul_left _ (Nat.le_succ _))
-    split
-    · next hga =>
-      have e5 : fastContractionAlgorithm.certificate.time (contractionInput (gs a) (X a)) ≤
-          K * (p + 1) ^ K * Z := by
-        refine (hfast a hga).1.trans ?_
-        calc _ ≤ K * ((p + 1) ^ K * ((enc a).length + 1) ^ (q * K)) * 2 ^ E :=
-              Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ (hinlen a))
-          _ = K * (p + 1) ^ K * (2 ^ E * ((enc a).length + 1) ^ (q * K)) := by ring
-          _ ≤ K * (p + 1) ^ K * Z :=
-              Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (hY (by omega)))
-      calc _ ≤ ch * Z + (cg * Z + (ci * Z + K * (p + 1) ^ K * Z)) + cr * CR ^ dr * Z :=
-            Nat.add_le_add (Nat.add_le_add e1 (Nat.add_le_add e2 (Nat.add_le_add e3 e5))) e6
-        _ = (ch + cg + ci + K * (p + 1) ^ K + cr * CR ^ dr) * Z := by ring
-        _ ≤ _ := hk _ (by simp only [k]; omega)
-    · calc _ ≤ ch * Z + (cg * Z + cf * Z) + cr * CR ^ dr * Z :=
-            Nat.add_le_add (Nat.add_le_add e1 (Nat.add_le_add e2 e4)) e6
-        _ = (ch + cg + cf + cr * CR ^ dr) * Z := by ring
-        _ ≤ _ := hk _ (by simp only [k]; omega)
-  · -- space
-    have e1 := (hspace_pair a).trans (Nat.mul_le_mul_left CS (hY (a := a) (show ds ≤ e by omega)))
-    have e2 := (hrule_space a).trans
-      (Nat.mul_le_mul_left _ (hY (a := a) (show ds * dr' ≤ e by omega)))
-    change cpair.space a + (NativeCertificate.ofPolyTime hrule).space
-      (hadamardCount (gs a), gapValue (gs a) (X a)) ≤ k * (((enc a).length + 1) ^ e + 1)
-    calc _ ≤ CS * ((enc a).length + 1) ^ e + cr' * CR ^ dr' * ((enc a).length + 1) ^ e :=
-          Nat.add_le_add e1 e2
-      _ = (CS + cr' * CR ^ dr') * ((enc a).length + 1) ^ e := by ring
-      _ ≤ k * ((enc a).length + 1) ^ e :=
-          Nat.mul_le_mul_right _ (by simp only [k]; omega)
-      _ ≤ _ := Nat.mul_le_mul_left _ (Nat.le_succ _)
-
-/-- **The simulator.** For polynomial-time computed gate codes `gs a`, well formed on the
-polynomial-time computed register `X a`, one machine computes `gapValue (gs a) (X a)`, the
-acceptance gap when `X a` is nonempty (`QuantumContraction.gapValue_eq`), in time
+  set d := dg + di + df + dg' + di' + df' + q * K
+  refine ⟨cg + ci + cf + cg' + ci' + cf' + K * (p + 1) ^ K, d, fun a => ?_⟩
+  set Y := ((enc a).length + 1) ^ d
+  set Z := 2 ^ (12 * K * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2)))
+  have hY {e : ℕ} (he : e ≤ d) : ((enc a).length + 1) ^ e ≤ Y :=
+    Nat.pow_le_pow_right (Nat.le_add_left 1 _) he
+  have hZ : Y ≤ Z * Y := Nat.le_mul_of_pos_left Y (Nat.two_pow_pos _)
+  change (NativeCertificate.ofPolyTime hguard).time a + (if guard (gs a) then
+        (NativeCertificate.ofPolyTime hinput).time a +
+          fastContractionAlgorithm.certificate.time (contractionInput (S a) (gs a) (X a))
+        else (NativeCertificate.ofPolyTime hfb).time a) ≤ _ ∧
+      (NativeCertificate.ofPolyTime hguard).space a + (if guard (gs a) then
+        (NativeCertificate.ofPolyTime hinput).space a +
+          fastContractionAlgorithm.certificate.space (contractionInput (S a) (gs a) (X a))
+        else (NativeCertificate.ofPolyTime hfb).space a) ≤ _
+  have e1 := (htg a).trans (Nat.mul_le_mul_left cg ((hY (e := dg) (by omega)).trans hZ))
+  have e2 := (hti a).trans (Nat.mul_le_mul_left ci ((hY (e := di) (by omega)).trans hZ))
+  have e3 := (htf a).trans (Nat.mul_le_mul_left cf ((hY (e := df) (by omega)).trans hZ))
+  have e1' := (hsg a).trans (Nat.mul_le_mul_left cg' (hY (e := dg') (by omega)))
+  have e2' := (hsi a).trans (Nat.mul_le_mul_left ci' (hY (e := di') (by omega)))
+  have e3' := (hsf a).trans (Nat.mul_le_mul_left cf' (hY (e := df') (by omega)))
+  have hqK : ((enc a).length + 1) ^ (q * K) ≤ Y := hY (by omega)
+  split
+  · next hga =>
+    have e4 := (hfast a hga).1.trans (Nat.mul_le_mul_left _ (Nat.mul_le_mul_left Z hqK))
+    have e4' := (hfast a hga).2.trans (Nat.mul_le_mul_left _ hqK)
+    constructor
+    · calc _ ≤ cg * (Z * Y) + (ci * (Z * Y) + K * (p + 1) ^ K * (Z * Y)) :=
+            Nat.add_le_add e1 (Nat.add_le_add e2 e4)
+        _ ≤ _ := by
+          rw [show cg * (Z * Y) + (ci * (Z * Y) + K * (p + 1) ^ K * (Z * Y)) =
+            (cg + ci + K * (p + 1) ^ K) * Z * Y by ring]
+          exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (by omega))
+    · calc _ ≤ cg' * Y + (ci' * Y + K * (p + 1) ^ K * Y) :=
+            Nat.add_le_add e1' (Nat.add_le_add e2' e4')
+        _ ≤ _ := by
+          rw [show cg' * Y + (ci' * Y + K * (p + 1) ^ K * Y) =
+            (cg' + ci' + K * (p + 1) ^ K) * Y by ring]
+          exact Nat.mul_le_mul_right _ (by omega)
+  · constructor
+    · calc _ ≤ cg * (Z * Y) + cf * (Z * Y) := Nat.add_le_add e1 e3
+        _ ≤ _ := by
+          rw [show cg * (Z * Y) + cf * (Z * Y) = (cg + cf) * Z * Y by ring]
+          exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (by omega))
+    · calc _ ≤ cg' * Y + cf' * Y := Nat.add_le_add e1' e3'
+        _ ≤ _ := by
+          rw [show cg' * Y + cf' * Y = (cg' + cf') * Y by ring]
+          exact Nat.mul_le_mul_right _ (by omega)
+
+/-- **The simulator.** For polynomial-time computed measured qubits `S a` and gate codes `gs a`,
+well formed on the polynomial-time computed register `X a`, one machine computes
+`gapValue (S a) (gs a) (X a)`, the projected gap (`QuantumContraction.gapValue_eq`), in time
 `2 ^ (A (L + 1) / √⌊log₂ (L + 2)⌋)` times a polynomial in the input length and in polynomial
 space, where `L` is the number of gates. -/
-theorem exists_computableInO_gapValue (hgs : ComputableInPolyTime gs enc (encList encGateCode))
+theorem exists_computableInO_gapValue {S : α → List ℕ}
+    (hS : ComputableInPolyTime S enc (encList encUnary))
+    (hgs : ComputableInPolyTime gs enc (encList encGateCode))
     (hX : ComputableInPolyTime X enc encBits)
     (hwf : ∀ a, ∀ g ∈ gs a, g.WellFormed (X a).length) :
-    ∃ A e : ℕ, ComputableInO (fun a => gapValue (gs a) (X a)) enc encNat
+    ∃ A e : ℕ, ComputableInO (fun a => gapValue (S a) (gs a) (X a)) enc encNat
       (fun a => 2 ^ (A * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) *
         ((enc a).length + 1) ^ e)
-      (fun a => ((enc a).length + 1) ^ e) :=
-  exists_computableInO_rule hgs hX hwf (rule := Prod.snd) (snd _ _)
+      (fun a => ((enc a).length + 1) ^ e) := by
+  obtain ⟨A, c, hc⟩ := exists_expTimePolySpace_gapValue hS hgs hX hwf
+  obtain ⟨e, he⟩ := hc.computableInO
+  exact ⟨A, e, he⟩
+
+/-- **Two projected gaps with polynomial-time postprocessing.** For polynomial-time computed lists
+`S a` and `P a` of measured qubits and gate codes `gs a`, well formed on the polynomial-time
+computed register `X a`, one machine computes `rule (gapValue (S a) …, gapValue (P a) …)`, for a
+polynomial-time `rule`, in time `2 ^ (A (L + 1) / √⌊log₂ (L + 2)⌋)` times a polynomial in the
+input length and in polynomial space, where `L` is the number of gates. With `P a = []`, whose
+projected gap is `2 ^ h` (`Cslib.Quantum.onesGap_nil_eq_two_pow`), the rule sees a probability
+and its denominator; with `P a` a postselected event, a conditional probability. -/
+theorem exists_computableInO_rule {S P : α → List ℕ}
+    (hS : ComputableInPolyTime S enc (encList encUnary))
+    (hP : ComputableInPolyTime P enc (encList encUnary))
+    (hgs : ComputableInPolyTime gs enc (encList encGateCode))
+    (hX : ComputableInPolyTime X enc encBits) (hwf : ∀ a, ∀ g ∈ gs a, g.WellFormed (X a).length)
+    {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β}
+    (hrule : ComputableInPolyTime rule (encPair encNat encNat) encβ) :
+    ∃ A e : ℕ, ComputableInO
+      (fun a => rule (gapValue (S a) (gs a) (X a), gapValue (P a) (gs a) (X a))) enc encβ
+      (fun a => 2 ^ (A * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) *
+        ((enc a).length + 1) ^ e)
+      (fun a => ((enc a).length + 1) ^ e) := by
+  obtain ⟨A, c, hc⟩ := exists_expTimePolySpace_gapValue hS hgs hX hwf
+  obtain ⟨A', c', hc'⟩ := exists_expTimePolySpace_gapValue hP hgs hX hwf
+  have hcc := ((hc.prod hc').mono (E' := fun a =>
+    (A + A') * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) fun a =>
+      Nat.div_add_div_le_add_div.trans (Nat.div_le_div_right (by rw [Nat.add_mul]))).comp_ofPolyTime
+    hrule
+  obtain ⟨e, he⟩ := hcc.computableInO
+  exact ⟨A + A', e, he⟩
 
 end Machine
 
-/-- **The acceptance probability from the simulator**: for well-formed codes on `m > 0` qubits and
-an input `x` of length at most `m`, the acceptance probability is `gapValue / 2 ^ h` on the padded
-register. -/
-theorem acceptProb_eq_gapValue {m : ℕ} (hm : 0 < m) {gs : List GateCode}
-    (hgs : ∀ g ∈ gs, g.WellFormed m) {x : List Bool} (hx : x.length ≤ m) :
-    acceptProb m gs x =
-      (gapValue gs (x ++ List.replicate (m - x.length) false) : ℝ) / 2 ^ hadamardCount gs := by
+/-- **Probabilities from the simulator**: for well-formed codes on `m` qubits and an input `x` of
+length at most `m`, the probability that every qubit of `S` reads `1` is `gapValue S / 2 ^ h` on the
+padded register. -/
+theorem onesProb_eq_gapValue {m : ℕ} {gs : List GateCode} (hgs : ∀ g ∈ gs, g.WellFormed m)
+    (S : List ℕ) {x : List Bool} (hx : x.length ≤ m) :
+    onesProb m gs S x =
+      (gapValue S gs (x ++ List.replicate (m - x.length) false) : ℝ) / 2 ^ hadamardCount gs := by
   have hlen : (x ++ List.replicate (m - x.length) false).length = m := by simp; omega
   have hgs' : ∀ g ∈ gs, g.WellFormed (x ++ List.replicate (m - x.length) false).length := by
     rw [hlen]
     exact hgs
-  have hm' : 0 < (x ++ List.replicate (m - x.length) false).length := by
-    rw [hlen]
-    exact hm
-  rw [acceptProb_eq_acceptGap hm gs hgs x, ofFn_inputState hx, gapValue_eq hm' hgs']
+  rw [onesProb_eq_onesGap gs hgs, ofFn_inputState hx, gapValue_eq S hgs']
   congr 1
-  have := Int.toNat_of_nonneg (acceptGap_nonneg_and_le hm' gs hgs').1
+  have := Int.toNat_of_nonneg (onesGap_nonneg_and_le S gs hgs').1
   exact_mod_cast this.symm
 
 /-! ### The class containments -/
 
 variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ}
 
-/-- **Bounded-error quantum time `T` in time `2 ^ O(T / √log T)` and space `T ^ O(1)`.** For `T`
-with `max n 2 ≤ T n`, every problem in `BQTIME[T]` is decided by one deterministic machine within
-time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`: the machine computes the acceptance gap
-of the circuit by tensor contraction and compares it with half of `2 ^ h`. -/
-theorem exists_decidableInTimeAndSpace_of_mem_BQTIME (hTn : ∀ n, max n 2 ≤ T n) {L : Set α}
-    (hL : L ∈ BQTIME enc T) :
+/-- **Deciding by two projected gaps in time `2 ^ O(T / √log T)` and space `T ^ O(1)`.** For `T`
+with `max n 2 ≤ T n`, a uniform family with `O(T)` gates and lists `S` and `P` of measured qubits,
+a problem is decided by one deterministic machine within time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and
+workspace `T n ^ d` when a polynomial-time `rule` decides it from any two numerators `g` and `g'`
+over a common power of two of the probabilities that the qubits of `S` and of `P` read `1`. -/
+theorem exists_decidableInTimeAndSpace_of_onesProb (hTn : ∀ n, max n 2 ≤ T n)
+    {F : UniformCircuitFamily} {c₁ c₂ : ℕ} (hgates : ∀ n, (F.gates n).length ≤ c₁ * T n + c₂)
+    (S P : List ℕ) {rule : ℕ × ℕ → Bool}
+    (hrule : ComputableInPolyTime rule (encPair encNat encNat) encBool) {L : Set α}
+    (hL : ∀ a (g g' r : ℕ), F.onesProb S (enc a) = g / 2 ^ r →
+      F.onesProb P (enc a) = g' / 2 ^ r → (a ∈ L ↔ rule (g, g') = true)) :
     ∃ C d : ℕ, DecidableInTimeAndSpace L enc
       (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
       (fun a => T (enc a).length ^ d) := by
-  obtain ⟨F, c₁, c₂, hgates, hF⟩ := hL
   have hgates' := F.computableInPolyTime_gates
   have hwidth := F.computableInPolyTime_width
   let gs : α → List GateCode := fun a => F.gates (enc a).length
@@ -417,33 +403,13 @@ theorem exists_decidableInTimeAndSpace_of_mem_BQTIME (hTn : ∀ n, max n 2 ≤ T
       omega
     rw [this]
     exact F.wellFormed _
-  have hrule : ComputableInPolyTime (fun p : ℕ × ℕ => decide (2 ^ p.1 < 2 * p.2))
-      (encPair encUnary encNat) encBool := by fun_prop
-  obtain ⟨A, e, hc⟩ := exists_computableInO_rule hgs hX hwf hrule
+  obtain ⟨A, e, hc⟩ := exists_computableInO_rule (const S) (const P) hgs hX hwf hrule
   obtain ⟨K, hK, -⟩ := hc
   -- correctness
-  have hcorrect (a : α) : a ∈ L ↔
-      decide (2 ^ hadamardCount (gs a) < 2 * gapValue (gs a) (X a)) = true := by
-    have hp := acceptProb_eq_gapValue (F.width_pos (enc a).length)
-      (F.wellFormed (enc a).length) (F.le_width (enc a).length)
-    change F.acceptProb (enc a) = _ at hp
-    set g := gapValue (gs a) (X a)
-    set r := hadamardCount (gs a)
-    have hpos : (0 : ℝ) < 2 ^ r := by positivity
-    rw [decide_eq_true_iff]
-    by_cases ha : a ∈ L
-    · have := (hF a).1 ha
-      rw [hp, le_div_iff₀ hpos] at this
-      have h1 : (2 : ℝ) * 2 ^ r ≤ 3 * g := by linarith
-      have h2 : 2 * 2 ^ r ≤ 3 * g := by exact_mod_cast h1
-      have h3 : 1 ≤ 2 ^ r := Nat.one_le_two_pow
-      exact ⟨fun _ => by omega, fun _ => ha⟩
-    · have := (hF a).2 ha
-      rw [hp, div_le_iff₀ hpos] at this
-      have h1 : (3 : ℝ) * g ≤ 2 ^ r := by linarith
-      have h2 : 3 * g ≤ 2 ^ r := by exact_mod_cast h1
-      have h3 : 1 ≤ 2 ^ r := Nat.one_le_two_pow
-      exact ⟨fun h => absurd h ha, fun h => by omega⟩
+  have hcorrect (a : α) :
+      a ∈ L ↔ rule (gapValue S (gs a) (X a), gapValue P (gs a) (X a)) = true :=
+    hL a _ _ _ (onesProb_eq_gapValue (F.wellFormed _) S (F.le_width _))
+      (onesProb_eq_gapValue (F.wellFormed _) P (F.le_width _))
   -- the bounds
   set C₀ := 2 * A * (c₁ + c₂ + 2) + 2 * e
   set D₀ := 2 * A * (c₁ + c₂ + 2) + 3 * A
@@ -453,19 +419,19 @@ theorem exists_decidableInTimeAndSpace_of_mem_BQTIME (hTn : ∀ n, max n 2 ≤ T
     have hT2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _)
     have hnT : (enc a).length ≤ T (enc a).length := (le_max_left _ _).trans (hTn _)
   · -- time
-    set S := T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))
+    set Q := T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))
     have hE := Nat.mul_succ_div_sqrt_log_two_le_of_le A c₁ c₂ hT2 (hgates (enc a).length)
     have hY := Nat.add_one_pow_le_two_pow_div_sqrt_log_two e hT2 hnT
     have hZ : 2 ^ (A * ((gs a).length + 1) / Nat.sqrt (Nat.log 2 ((gs a).length + 2))) *
-        ((enc a).length + 1) ^ e ≤ 2 ^ D₀ * 2 ^ (C₀ * S) := by
-      calc _ ≤ 2 ^ (2 * A * (c₁ + c₂ + 2) * S + D₀) * 2 ^ (2 * e * S) :=
+        ((enc a).length + 1) ^ e ≤ 2 ^ D₀ * 2 ^ (C₀ * Q) := by
+      calc _ ≤ 2 ^ (2 * A * (c₁ + c₂ + 2) * Q + D₀) * 2 ^ (2 * e * Q) :=
             Nat.mul_le_mul (Nat.pow_le_pow_right (by norm_num) hE) hY
-        _ = 2 ^ D₀ * 2 ^ (C₀ * S) := by
+        _ = 2 ^ D₀ * 2 ^ (C₀ * Q) := by
             rw [← pow_add, ← pow_add]
             congr 1
             simp only [C₀]
             ring
-    have hCS : C₀ * S ≤ C₀ * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)) :=
+    have hCQ : C₀ * Q ≤ C₀ * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)) :=
       Nat.mul_div_le_mul_div_assoc _ _ _
     have hfinal := Nat.mul_two_pow_div_sqrt_log_two_add_le (a := K * 2 ^ D₀) (b := K) (C := C₀)
       hT2
@@ -474,7 +440,7 @@ theorem exists_decidableInTimeAndSpace_of_mem_BQTIME (hTn : ∀ n, max n 2 ≤ T
         ≤ K * (2 ^ D₀ * 2 ^ (C₀ * T (enc a).length /
             Nat.sqrt (Nat.log 2 (T (enc a).length))) + 1) :=
           Nat.mul_le_mul_left _ (Nat.add_le_add_right (hZ.trans (Nat.mul_le_mul_left _
-            (Nat.pow_le_pow_right (by norm_num) hCS))) _)
+            (Nat.pow_le_pow_right (by norm_num) hCQ))) _)
       _ = K * 2 ^ D₀ * 2 ^ (C₀ * T (enc a).length /
             Nat.sqrt (Nat.log 2 (T (enc a).length))) + K := by ring
       _ ≤ _ := hfinal
@@ -487,12 +453,115 @@ theorem exists_decidableInTimeAndSpace_of_mem_BQTIME (hTn : ∀ n, max n 2 ≤ T
           exact Nat.add_le_add_right (Nat.mul_le_mul_left _ hpow) _
       _ ≤ _ := this
 
-/-- **`BQTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for `T` with `max n 2 ≤ T n`. -/
-theorem BQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hTn : ∀ n, max n 2 ≤ T n) :
-    BQTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := by
-  intro L hL
-  obtain ⟨C, d, h⟩ := exists_decidableInTimeAndSpace_of_mem_BQTIME hTn hL
+/-- A problem decided within time `2 ^ (C T / √⌊log₂ T⌋)` lies in the union of these classes. -/
+private theorem mem_iUnion_DTIME {L : Set α}
+    (h : ∃ C d : ℕ, DecidableInTimeAndSpace L enc
+      (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
+      (fun a => T (enc a).length ^ d)) :
+    L ∈ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := by
+  obtain ⟨C, d, h⟩ := h
   exact Set.mem_iUnion.mpr ⟨C, 1, 0, fun n => T n ^ d,
     ComputableInTimeAndSpace.mono h (fun a => by rw [Nat.one_mul, Nat.add_zero]) fun _ => le_rfl⟩
 
+/-- **The bounded-error rule**: when `g / g'` is at least `2 / 3` on members and at most `1 / 3`
+otherwise, for `g' > 0`, membership is `g' < 2 g`. -/
+private theorem iff_lt_two_mul {L : Set α} {a : α} {g g' : ℕ} (hg' : 0 < g')
+    (h₁ : a ∈ L → (2 : ℝ) / 3 ≤ g / g') (h₂ : a ∉ L → (g : ℝ) / g' ≤ 1 / 3) :
+    a ∈ L ↔ decide (g' < 2 * g) = true := by
+  have hpos : (0 : ℝ) < g' := by exact_mod_cast hg'
+  rw [decide_eq_true_iff]
+  by_cases ha : a ∈ L
+  · have := h₁ ha
+    rw [le_div_iff₀ hpos] at this
+    have : 2 * g' ≤ 3 * g := by exact_mod_cast (by linarith : (2 : ℝ) * g' ≤ 3 * g)
+    exact ⟨fun _ => by omega, fun _ => ha⟩
+  · have := h₂ ha
+    rw [div_le_iff₀ hpos] at this
+    have : 3 * g ≤ g' := by exact_mod_cast (by linarith : (3 : ℝ) * g ≤ g')
+    exact ⟨fun h => absurd h ha, fun h => by omega⟩
+
+/-- **Bounded-error quantum time `T` in time `2 ^ O(T / √log T)` and space `T ^ O(1)`.** For `T`
+with `max n 2 ≤ T n`, every problem in `BQTIME[T]` is decided by one deterministic machine within
+time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`: the machine computes the acceptance gap
+`g` of the circuit and the projected gap `2 ^ h` of no condition by tensor contraction and accepts
+when `2 ^ h < 2 g`. -/
+theorem exists_decidableInTimeAndSpace_of_mem_BQTIME (hTn : ∀ n, max n 2 ≤ T n) {L : Set α}
+    (hL : L ∈ BQTIME enc T) :
+    ∃ C d : ℕ, DecidableInTimeAndSpace L enc
+      (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
+      (fun a => T (enc a).length ^ d) := by
+  obtain ⟨F, c₁, c₂, hgates, hF⟩ := hL
+  refine exists_decidableInTimeAndSpace_of_onesProb hTn hgates [0] []
+    (rule := fun p => decide (p.2 < 2 * p.1)) (by fun_prop) fun a g g' r h h' => ?_
+  rw [UniformCircuitFamily.onesProb, onesProb_nil] at h'
+  have hg' : (g' : ℝ) = 2 ^ r := by
+    rw [eq_div_iff (by positivity), one_mul] at h'
+    exact h'.symm
+  have hp : F.acceptProb (enc a) = g / g' := by rw [hg']; exact h
+  exact iff_lt_two_mul (by exact_mod_cast hg' ▸ (by positivity : (0 : ℝ) < 2 ^ r))
+    (fun ha => hp ▸ (hF a).1 ha) fun ha => hp ▸ (hF a).2 ha
+
+/-- **`BQTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for `T` with `max n 2 ≤ T n`. -/
+theorem BQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hTn : ∀ n, max n 2 ≤ T n) :
+    BQTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) :=
+  fun _ hL => mem_iUnion_DTIME (exists_decidableInTimeAndSpace_of_mem_BQTIME hTn hL)
+
+/-- **Nondeterministic quantum time `T` in time `2 ^ O(T / √log T)` and space `T ^ O(1)`.** For
+`T` with `max n 2 ≤ T n`, every problem in `NQTIME[T]` is decided by one deterministic machine
+within time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`: the machine computes the
+acceptance gap of the circuit by tensor contraction and accepts when it is positive. -/
+theorem exists_decidableInTimeAndSpace_of_mem_NQTIME (hTn : ∀ n, max n 2 ≤ T n) {L : Set α}
+    (hL : L ∈ NQTIME enc T) :
+    ∃ C d : ℕ, DecidableInTimeAndSpace L enc
+      (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
+      (fun a => T (enc a).length ^ d) := by
+  obtain ⟨F, c₁, c₂, hgates, hF⟩ := hL
+  refine exists_decidableInTimeAndSpace_of_onesProb hTn hgates [0] []
+    (rule := fun p => decide (0 < p.1)) (by fun_prop) fun a g g' r h _ => ?_
+  rw [hF a, decide_eq_true_iff, UniformCircuitFamily.acceptProb_eq_onesProb, h]
+  constructor
+  · intro hpos
+    exact_mod_cast (div_pos_iff_of_pos_right (by positivity : (0 : ℝ) < 2 ^ r)).mp hpos
+  · intro hg
+    exact div_pos (by exact_mod_cast hg) (by positivity)
+
+/-- **`NQTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for `T` with `max n 2 ≤ T n`. -/
+theorem NQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hTn : ∀ n, max n 2 ≤ T n) :
+    NQTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) :=
+  fun _ hL => mem_iUnion_DTIME (exists_decidableInTimeAndSpace_of_mem_NQTIME hTn hL)
+
+/-- **Exact quantum time `T` in time `2 ^ O(T / √log T)`**: exact quantum time lies in
+nondeterministic quantum time (`Cslib.Complexity.EQTIME_subset_NQTIME`). -/
+theorem EQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hTn : ∀ n, max n 2 ≤ T n) :
+    EQTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) :=
+  (EQTIME_subset_NQTIME T).trans (NQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hTn)
+
+/-- **Postselected bounded-error quantum time `T` in time `2 ^ O(T / √log T)` and space
+`T ^ O(1)`.** For `T` with `max n 2 ≤ T n`, every problem in `PostBQTIME[T]` is decided by one
+deterministic machine within time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`: the
+machine computes the projected gaps `g` of qubits `0` and `1` and `g'` of qubit `1` by tensor
+contraction and accepts when `g' < 2 g`, that is, when the postselected acceptance probability
+exceeds `1 / 2`. -/
+theorem exists_decidableInTimeAndSpace_of_mem_PostBQTIME (hTn : ∀ n, max n 2 ≤ T n) {L : Set α}
+    (hL : L ∈ PostBQTIME enc T) :
+    ∃ C d : ℕ, DecidableInTimeAndSpace L enc
+      (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
+      (fun a => T (enc a).length ^ d) := by
+  obtain ⟨F, c₁, c₂, hgates, hF⟩ := hL
+  refine exists_decidableInTimeAndSpace_of_onesProb hTn hgates [0, 1] [1]
+    (rule := fun p => decide (p.2 < 2 * p.1)) (by fun_prop) fun a g g' r h h' => ?_
+  obtain ⟨hpost, h₁, h₂⟩ := hF a
+  have hr : (0 : ℝ) < 2 ^ r := by positivity
+  have hg' : 0 < g' := by
+    rw [h'] at hpost
+    exact_mod_cast (div_pos_iff_of_pos_right hr).mp hpost
+  have hp : F.postselectedAcceptProb (enc a) = g / g' := by
+    rw [UniformCircuitFamily.postselectedAcceptProb, h, h', div_div_div_cancel_right₀ hr.ne']
+  exact iff_lt_two_mul hg' (fun ha => hp ▸ h₁ ha) fun ha => hp ▸ h₂ ha
+
+/-- **`PostBQTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for `T` with `max n 2 ≤ T n`. -/
+theorem PostBQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hTn : ∀ n, max n 2 ≤ T n) :
+    PostBQTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) :=
+  fun _ hL => mem_iUnion_DTIME (exists_decidableInTimeAndSpace_of_mem_PostBQTIME hTn hL)
+
 end Cslib.Complexity.QuantumContraction
diff --git a/Complexity/Computability/Complexity/Classes/BQP/Time.lean b/Complexity/Computability/Complexity/Classes/BQP/Time.lean
index 17a790f1d..803ed496b 100644
--- a/Complexity/Computability/Complexity/Classes/BQP/Time.lean
+++ b/Complexity/Computability/Complexity/Classes/BQP/Time.lean
@@ -12,7 +12,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives
 
 /-!
-# Bounded-error quantum time
+# Quantum time classes
 
 `BQTIME enc t` (`Cslib.Complexity.BQTIME`) is the class of problems decided with bounded error by
 the polynomial-time uniform families of quantum circuits of `Cslib.Complexity.BQP` whose circuits
@@ -25,16 +25,48 @@ The families are polynomial-time uniform, so every circuit has polynomially many
 dominates every polynomial. `BQP` is the union of the classes `BQTIME[n ^ k]`
 (`Cslib.Complexity.BQP_eq_iUnion_BQTIME`).
 
+The same families with the same gate bounds define three more classes, by other acceptance
+conditions:
+
+* **Nondeterministic quantum time** `NQTIME enc t` (`Cslib.Complexity.NQTIME`): members are the
+  instances accepted with nonzero probability. It is the time-`t` circuit analogue of the class
+  `NQP` of Adleman, DeMarrais and Huang, defined for quantum Turing machines in [Fenner, Green,
+  Homer, Pruim][FennerGreenHomerPruim1999], Definition 2.1, who show `NQP = coC₌P` (Theorem 1.1),
+  and in Section 4 that `coC₌P` is already in `NQP` with amplitudes in `{0, ±1/√2, ±1}`.
+* **Exact quantum time** `EQTIME enc t` (`Cslib.Complexity.EQTIME`): members are accepted with
+  probability `1` and other instances with probability `0`, as `EQTime(T(n))` in
+  [Bernstein, Vazirani][BernsteinVazirani1997], Definition 8.1, for quantum Turing machines.
+  Exactness depends on the gate set: approximating one gate set by another preserves bounded error
+  but not zero error, so this is exact quantum time over the Hadamard, NOT, CNOT and Toffoli gates,
+  and it is not claimed to equal exact quantum time over other gate sets or quantum Turing
+  machines. It lies in `NQTIME` and in `BQTIME` (`Cslib.Complexity.EQTIME_subset_NQTIME`,
+  `Cslib.Complexity.EQTIME_subset_BQTIME`).
+* **Postselected bounded-error quantum time** `PostBQTIME enc t` (`Cslib.Complexity.PostBQTIME`):
+  qubit `1` reads `1` with nonzero probability, and conditioned on that, qubit `0` reads `1` with
+  probability at least `2 / 3` on members and at most `1 / 3` otherwise. It is the time-`t`
+  analogue of `PostBQP`, [Aaronson][Aaronson2005Postselection], Definition 1, with his first
+  (postselected) and second (output) qubits exchanged; he shows `PostBQP = PP` (Theorem 4).
+
 ## Main definitions
 
-* `Cslib.Complexity.BQTIME`.
+* `Cslib.Complexity.BQTIME`, `Cslib.Complexity.NQTIME`, `Cslib.Complexity.EQTIME`,
+  `Cslib.Complexity.PostBQTIME`.
 
 ## Main results
 
 * `Cslib.Complexity.BQTIME_subset_BQP`: every `BQTIME` class lies in `BQP`.
 * `Cslib.Complexity.BQP_eq_iUnion_BQTIME`: `BQP = ⋃ k, BQTIME[n ^ k]`.
--/
+* `Cslib.Complexity.EQTIME_subset_NQTIME`, `Cslib.Complexity.EQTIME_subset_BQTIME`: exact quantum
+  time is nondeterministic and bounded-error quantum time.
+
+## References
 
+* [E. Bernstein, U. Vazirani, *Quantum complexity theory*][BernsteinVazirani1997]
+* [S. Fenner, F. Green, S. Homer, R. Pruim, *Determining acceptance possibility for a quantum
+  computation is hard for the polynomial hierarchy*][FennerGreenHomerPruim1999]
+* [S. Aaronson, *Quantum computing, postselection, and probabilistic
+  polynomial-time*][Aaronson2005Postselection]
+-/
 @[expose] public section
 
 namespace Cslib.Complexity
@@ -55,8 +87,57 @@ def BQTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
   {A | ∃ (F : UniformCircuitFamily) (c₁ c₂ : ℕ), (∀ n, (F.gates n).length ≤ c₁ * t n + c₂) ∧
     ∀ a, (a ∈ A → 2 / 3 ≤ F.acceptProb (enc a)) ∧ (a ∉ A → F.acceptProb (enc a) ≤ 1 / 3)}
 
+/-- **Nondeterministic quantum time** `t`: the problems whose members, with respect to the encoding
+`enc` of instances, are exactly the instances accepted with nonzero probability by a
+polynomial-time uniform family of quantum circuits over the Hadamard, NOT, CNOT and Toffoli gates
+(`Cslib.Quantum.UniformCircuitFamily`) whose circuit for inputs of length `n` has at most
+`c₁ t n + c₂` gates. -/
+def NQTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
+  {A | ∃ (F : UniformCircuitFamily) (c₁ c₂ : ℕ), (∀ n, (F.gates n).length ≤ c₁ * t n + c₂) ∧
+    ∀ a, a ∈ A ↔ 0 < F.acceptProb (enc a)}
+
+/-- **Exact quantum time** `t` over the Hadamard, NOT, CNOT and Toffoli gates: the problems decided
+without error, with respect to the encoding `enc` of instances, by a polynomial-time uniform family
+of quantum circuits whose circuit for inputs of length `n` has at most `c₁ t n + c₂` gates.
+Members are accepted with probability `1` and other instances with probability `0`. -/
+def EQTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
+  {A | ∃ (F : UniformCircuitFamily) (c₁ c₂ : ℕ), (∀ n, (F.gates n).length ≤ c₁ * t n + c₂) ∧
+    ∀ a, (a ∈ A → F.acceptProb (enc a) = 1) ∧ (a ∉ A → F.acceptProb (enc a) = 0)}
+
+/-- **Postselected bounded-error quantum time** `t`: the problems decided with bounded error after
+postselection, with respect to the encoding `enc` of instances, by a polynomial-time uniform family
+of quantum circuits over the Hadamard, NOT, CNOT and Toffoli gates whose circuit for inputs of
+length `n` has at most `c₁ t n + c₂` gates. On every instance qubit `1` reads `1` with nonzero
+probability, and conditioned on that (`Cslib.Quantum.UniformCircuitFamily.postselectedAcceptProb`)
+members are accepted with probability at least `2 / 3` and other instances with probability at
+most `1 / 3`. -/
+def PostBQTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
+  {A | ∃ (F : UniformCircuitFamily) (c₁ c₂ : ℕ), (∀ n, (F.gates n).length ≤ c₁ * t n + c₂) ∧
+    ∀ a, 0 < F.onesProb [1] (enc a) ∧ (a ∈ A → 2 / 3 ≤ F.postselectedAcceptProb (enc a)) ∧
+      (a ∉ A → F.postselectedAcceptProb (enc a) ≤ 1 / 3)}
+
 variable {enc : α ↪ List Bool}
 
+/-- **Exact quantum time is nondeterministic quantum time**: a probability that is `0` or `1` is
+positive exactly when it is `1`. -/
+theorem EQTIME_subset_NQTIME (t : ℕ → ℕ) : EQTIME enc t ⊆ NQTIME enc t := by
+  rintro A ⟨F, c₁, c₂, hgates, hF⟩
+  refine ⟨F, c₁, c₂, hgates, fun a => ⟨fun ha => ?_, fun hp => ?_⟩⟩
+  · rw [(hF a).1 ha]
+    exact one_pos
+  · by_contra ha
+    rw [(hF a).2 ha] at hp
+    exact lt_irrefl 0 hp
+
+/-- **Exact quantum time is bounded-error quantum time.** -/
+theorem EQTIME_subset_BQTIME (t : ℕ → ℕ) : EQTIME enc t ⊆ BQTIME enc t := by
+  rintro A ⟨F, c₁, c₂, hgates, hF⟩
+  refine ⟨F, c₁, c₂, hgates, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩
+  · rw [(hF a).1 ha]
+    norm_num
+  · rw [(hF a).2 ha]
+    norm_num
+
 /-- Every `BQTIME` class lies in `BQP`. -/
 theorem BQTIME_subset_BQP (t : ℕ → ℕ) : BQTIME enc t ⊆ BQP enc :=
   fun _ ⟨F, _, _, _, hF⟩ => ⟨F, hF⟩
diff --git a/Complexity/Computability/GenericRAM/Native/ExpTimePolySpace.lean b/Complexity/Computability/GenericRAM/Native/ExpTimePolySpace.lean
new file mode 100644
index 000000000..0cbc7efe9
--- /dev/null
+++ b/Complexity/Computability/GenericRAM/Native/ExpTimePolySpace.lean
@@ -0,0 +1,162 @@
+/-
+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.GenericRAM.Native.Combinators
+
+/-!
+# Certificates in time `2 ^ E` times a polynomial and polynomial space
+
+A native certificate runs *in time `2 ^ E` times a polynomial and in polynomial space*
+(`Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace`) when, for constants `C` and `d`, its time is
+at most `C 2 ^ E a (n + 1) ^ d` and its space at most `C (n + 1) ^ d` on inputs `a` of encoded
+length `n`. This shape survives pairing, which adds the exponents
+(`Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace.prod`), and polynomial-time postprocessing,
+since a polynomial space bound also bounds the encoded intermediate value
+(`Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace.comp_ofPolyTime`). Simulations that run a few
+exponential-time subroutines and combine their answers in polynomial time are assembled this way.
+
+## Main definitions
+
+* `Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace`.
+
+## Main results
+
+* `Cslib.GenericRAM.NativeCertificate.expTimePolySpace_ofPolyTime`: polynomial-time certificates.
+* `Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace.prod`,
+  `Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace.comp_ofPolyTime`: pairs and
+  polynomial-time postprocessing.
+* `Cslib.GenericRAM.NativeCertificate.ExpTimePolySpace.computableInO`: the resulting machine bounds.
+-/
+
+public section
+
+namespace Cslib.GenericRAM.NativeCertificate
+
+open Turing.MultiTapeTM
+
+variable {α β γ : Type} {enc : α ↪ List Bool} {eβ : β ↪ List Bool} {eγ : γ ↪ List Bool}
+  {f : α → β} {g : α → γ}
+
+/-- A certificate **runs in time `2 ^ E` times a polynomial and in polynomial space**: for constants
+`C` and `d`, its time is at most `C 2 ^ E a (n + 1) ^ d` and its space at most `C (n + 1) ^ d` on
+inputs `a` of encoded length `n`. -/
+@[expose] def ExpTimePolySpace (c : NativeCertificate f enc eβ) (E : α → ℕ) : Prop :=
+  ∃ C d : ℕ, ∀ a, c.time a ≤ C * 2 ^ E a * ((enc a).length + 1) ^ d ∧
+    c.space a ≤ C * ((enc a).length + 1) ^ d
+
+namespace ExpTimePolySpace
+
+variable {c : NativeCertificate f enc eβ} {E E' : α → ℕ}
+
+theorem mono (h : c.ExpTimePolySpace E) (hE : ∀ a, E a ≤ E' a) : c.ExpTimePolySpace E' := by
+  obtain ⟨C, d, h⟩ := h
+  exact ⟨C, d, fun a => ⟨(h a).1.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _
+    (Nat.pow_le_pow_right (by norm_num) (hE a)))), (h a).2⟩⟩
+
+/-- **Pairs add the exponents.** -/
+theorem prod {c' : NativeCertificate g enc eγ} (h : c.ExpTimePolySpace E)
+    (h' : c'.ExpTimePolySpace E') : (c.prod c').ExpTimePolySpace fun a => E a + E' a := by
+  obtain ⟨C, d, h⟩ := h
+  obtain ⟨C', d', h'⟩ := h'
+  refine ⟨C + C', d + d', fun a => ?_⟩
+  have hd := Nat.pow_le_pow_right (Nat.succ_pos (enc a).length) (Nat.le_add_right d d')
+  have hd' := Nat.pow_le_pow_right (Nat.succ_pos (enc a).length) (Nat.le_add_left d' d)
+  have hE := Nat.le_mul_of_pos_right (2 ^ E a) (Nat.two_pow_pos (E' a))
+  have hE' := Nat.le_mul_of_pos_left (2 ^ E' a) (Nat.two_pow_pos (E a))
+  rw [prod_time, prod_space, pow_add 2 (E a) (E' a)]
+  constructor
+  · calc c.time a + c'.time a
+        ≤ C * 2 ^ E a * ((enc a).length + 1) ^ d + C' * 2 ^ E' a * ((enc a).length + 1) ^ d' :=
+          Nat.add_le_add (h a).1 (h' a).1
+      _ ≤ C * (2 ^ E a * 2 ^ E' a) * ((enc a).length + 1) ^ (d + d') +
+          C' * (2 ^ E a * 2 ^ E' a) * ((enc a).length + 1) ^ (d + d') := by
+          gcongr
+      _ = _ := by ring
+  · calc c.space a + c'.space a
+        ≤ C * ((enc a).length + 1) ^ d + C' * ((enc a).length + 1) ^ d' :=
+          Nat.add_le_add (h a).2 (h' a).2
+      _ ≤ C * ((enc a).length + 1) ^ (d + d') + C' * ((enc a).length + 1) ^ (d + d') := by
+          gcongr
+      _ = _ := by ring
+
+/-- **Polynomial-time postprocessing keeps the shape**: the polynomial space bound also bounds the
+encoded intermediate value, on which the postprocessing runs. -/
+theorem comp_ofPolyTime (h : c.ExpTimePolySpace E) {r : β → γ}
+    (hr : ComputableInPolyTime r eβ eγ) : ((ofPolyTime hr).comp c).ExpTimePolySpace E := by
+  obtain ⟨C, d, h⟩ := h
+  obtain ⟨K₀, -, hK₀⟩ := c.computes
+  have hp := ofPolyTime_isPolynomial hr
+  obtain ⟨ct, dt, ht⟩ := hp.1.exists_le
+  obtain ⟨cs, ds, hs⟩ := hp.2.exists_le
+  set D := K₀ * C + K₀ + 1
+  -- the encoded intermediate value
+  have hlen (a : α) : (eβ (f a)).length + 1 ≤ D * ((enc a).length + 1) ^ d := by
+    have h1 := hK₀ a
+    have h2 := (h a).2
+    have h3 : 1 ≤ ((enc a).length + 1) ^ d := Nat.one_le_pow _ _ (Nat.succ_pos _)
+    simp only [D]
+    nlinarith
+  have hpoly {c₀ d₀ : ℕ} {u : β → ℕ} (hu : ∀ b, u b ≤ c₀ * ((eβ b).length + 1) ^ d₀) (a : α) :
+      u (f a) ≤ c₀ * D ^ d₀ * ((enc a).length + 1) ^ (d * d₀) := by
+    refine (hu (f a)).trans ?_
+    calc c₀ * ((eβ (f a)).length + 1) ^ d₀ ≤ c₀ * (D * ((enc a).length + 1) ^ d) ^ d₀ :=
+          Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (hlen a) d₀)
+      _ = _ := by rw [mul_pow, ← pow_mul]; ring
+  refine ⟨C + ct * D ^ dt + cs * D ^ ds, d + d * dt + d * ds, fun a => ?_⟩
+  set Y := ((enc a).length + 1) ^ (d + d * dt + d * ds)
+  have hY {e : ℕ} (he : e ≤ d + d * dt + d * ds) : ((enc a).length + 1) ^ e ≤ Y :=
+    Nat.pow_le_pow_right (Nat.succ_pos _) he
+  have hZ : Y ≤ 2 ^ E a * Y := Nat.le_mul_of_pos_left Y (Nat.two_pow_pos (E a))
+  rw [comp_time, comp_space]
+  constructor
+  · calc c.time a + (ofPolyTime hr).time (f a)
+        ≤ C * 2 ^ E a * ((enc a).length + 1) ^ d +
+            ct * D ^ dt * ((enc a).length + 1) ^ (d * dt) :=
+          Nat.add_le_add (h a).1 (hpoly ht a)
+      _ ≤ C * 2 ^ E a * Y + ct * D ^ dt * (2 ^ E a * Y) :=
+          Nat.add_le_add (Nat.mul_le_mul_left _ (hY (e := d) (by omega)))
+            (Nat.mul_le_mul_left _ ((hY (e := d * dt) (by omega)).trans hZ))
+      _ = (C + ct * D ^ dt) * 2 ^ E a * Y := by ring
+      _ ≤ _ := Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (by omega))
+  · calc c.space a + (ofPolyTime hr).space (f a)
+        ≤ C * ((enc a).length + 1) ^ d + cs * D ^ ds * ((enc a).length + 1) ^ (d * ds) :=
+          Nat.add_le_add (h a).2 (hpoly hs a)
+      _ ≤ C * Y + cs * D ^ ds * Y :=
+          Nat.add_le_add (Nat.mul_le_mul_left _ (hY (e := d) (by omega)))
+            (Nat.mul_le_mul_left _ (hY (e := d * ds) (by omega)))
+      _ = (C + cs * D ^ ds) * Y := by ring
+      _ ≤ _ := Nat.mul_le_mul_right _ (by omega)
+
+/-- **The machine bounds** of a certificate in time `2 ^ E` times a polynomial and polynomial
+space. -/
+theorem computableInO (h : c.ExpTimePolySpace E) : ∃ e : ℕ,
+    ComputableInO f enc eβ (fun a => 2 ^ E a * ((enc a).length + 1) ^ e)
+      (fun a => ((enc a).length + 1) ^ e) := by
+  obtain ⟨C, d, h⟩ := h
+  refine ⟨d, c.computes.mono C (fun a => (h a).1.trans ?_) (fun a => (h a).2.trans ?_)⟩
+  · rw [Nat.mul_assoc]
+    exact Nat.mul_le_mul_left _ (Nat.le_succ _)
+  · exact Nat.mul_le_mul_left _ (Nat.le_succ _)
+
+end ExpTimePolySpace
+
+/-- **Polynomial-time certificates** run in time `2 ^ E` times a polynomial for every `E`. -/
+theorem expTimePolySpace_ofPolyTime (hf : ComputableInPolyTime f enc eβ) (E : α → ℕ) :
+    (ofPolyTime hf).ExpTimePolySpace E := by
+  have hp := ofPolyTime_isPolynomial hf
+  obtain ⟨ct, dt, ht⟩ := hp.1.exists_le
+  obtain ⟨cs, ds, hs⟩ := hp.2.exists_le
+  refine ⟨ct + cs, dt + ds, fun a => ⟨(ht a).trans ?_, (hs a).trans ?_⟩⟩
+  · rw [Nat.mul_assoc]
+    exact Nat.mul_le_mul (by omega)
+      ((Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_add_right _ _)).trans
+        (Nat.le_mul_of_pos_left _ (Nat.two_pow_pos _)))
+  · exact Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_add_left _ _))
+
+end Cslib.GenericRAM.NativeCertificate
diff --git a/ComplexityTests/BQPCounting.lean b/ComplexityTests/BQPCounting.lean
index 38706a002..d3a65076d 100644
--- a/ComplexityTests/BQPCounting.lean
+++ b/ComplexityTests/BQPCounting.lean
@@ -42,7 +42,7 @@ example : acceptGap [(true, 0, []), (true, 0, [])] [true] = 4 := by decide
 
 -- The count agrees with the quantum acceptance probability of `hadamardOnce`.
 example : acceptProb 1 [(true, 0, [])] [] = 1 / 2 := by
-  rw [acceptProb_eq_acceptGap (by norm_num) _ (by decide)]
+  rw [acceptProb_eq_acceptGap _ (by decide)]
   have : List.ofFn (inputState 1 []) = [false] := by decide
   rw [this, show acceptGap [(true, 0, [])] [false] = 1 by decide]
   norm_num
diff --git a/ComplexityTests/BQPTensorContraction.lean b/ComplexityTests/BQPTensorContraction.lean
index dd90bb0c7..6b9912d81 100644
--- a/ComplexityTests/BQPTensorContraction.lean
+++ b/ComplexityTests/BQPTensorContraction.lean
@@ -18,41 +18,50 @@ open Cslib Cslib.Quantum Cslib.Quantum.PathNetwork Cslib.Complexity
 /-! ### The bipartition -/
 
 -- A Hadamard gate copied by a CNOT: every edge joins a row to a column.
-example : (network (-1 : ℤ) [false, false] [(true, 1, []), (false, 0, [1])]).2.IsRowsFirstBipartite
-    (network (-1 : ℤ) [false, false] [(true, 1, []), (false, 0, [1])]).1 := by decide
+example :
+    (network (-1 : ℤ) [0] [false, false] [(true, 1, []), (false, 0, [1])]).2.IsRowsFirstBipartite
+      (network (-1 : ℤ) [0] [false, false] [(true, 1, []), (false, 0, [1])]).1 := by decide
 
-example : (network (-1 : ℤ) [false, false] [(true, 1, []), (false, 0, [1])]).2.IsRowsFirstBipartite
-    (network (-1 : ℤ) [false, false] [(true, 1, []), (false, 0, [1])]).1 :=
-  isRowsFirstBipartite_network _ _ (by decide)
+example :
+    (network (-1 : ℤ) [0] [false, false] [(true, 1, []), (false, 0, [1])]).2.IsRowsFirstBipartite
+      (network (-1 : ℤ) [0] [false, false] [(true, 1, []), (false, 0, [1])]).1 :=
+  isRowsFirstBipartite_network _ _ _ (by decide)
 
 -- The hypothesis that the qubits of a gate are distinct is needed: a CNOT whose control is its
 -- target reads the same link edge twice.
-example : ¬(network (-1 : ℤ) [false, false] [(true, 0, []), (false, 0, [0])]).2.IsRowsFirstBipartite
-    (network (-1 : ℤ) [false, false] [(true, 0, []), (false, 0, [0])]).1 := by decide
+example :
+    ¬(network (-1 : ℤ) [0] [false, false] [(true, 0, []), (false, 0, [0])]).2.IsRowsFirstBipartite
+      (network (-1 : ℤ) [0] [false, false] [(true, 0, []), (false, 0, [0])]).1 := by decide
 
 -- A Toffoli gate: three occurrences, so twelve edges, admissible at size twelve.
 example : CountingSimulation.ExplicitAdmissible 6 12
-    (network 7 [false, false, false] [(false, 2, [0, 1])]) :=
-  explicitAdmissible_network 7 [false, false, false] (by decide) (by decide)
+    (network 7 [0] [false, false, false] [(false, 2, [0, 1])]) :=
+  explicitAdmissible_network 7 [0] [false, false, false] (by decide) (by decide)
 
 /-! ### The simulator -/
 
 -- One Hadamard gate on `|0⟩`: the gap is `1`, so the acceptance probability is `1 / 2`.
-example : gapValue [(true, 0, [])] [false] = 1 := by decide
+example : gapValue [0] [(true, 0, [])] [false] = 1 := by decide
 
 example : acceptProb 1 [(true, 0, [])] [false] = 1 / 2 := by
-  rw [acceptProb_eq_gapValue (by decide) (by decide) (by decide)]
-  rw [show gapValue [(true, 0, [])] ([false] ++ List.replicate (1 - [false].length) false) = 1 by
-    decide]
+  rw [acceptProb_eq_onesProb, onesProb_eq_gapValue (by decide) [0] (by decide)]
+  rw [show gapValue [0] [(true, 0, [])] ([false] ++ List.replicate (1 - [false].length) false) = 1
+    by decide]
   norm_num [hadamardCount]
 
--- Without gates, the simulator reads qubit `0`.
-example : gapValue [] [true, false] = 1 := by decide
-example : gapValue [] [false, true] = 0 := by decide
+-- Without gates, the simulator reads the measured qubits.
+example : gapValue [0] [] [true, false] = 1 := by decide
+example : gapValue [0] [] [false, true] = 0 := by decide
+example : gapValue [0, 1] [] [true, true] = 1 := by decide
 
 -- Two Hadamard gates on `|1⟩` interfere: the gap is `2 ^ 2`.
-example : gapValue [(true, 0, []), (true, 0, [])] [true] = 4 := by
-  rw [gapValue_eq (by decide) (by decide)]
+example : gapValue [0] [(true, 0, []), (true, 0, [])] [true] = 4 := by
+  rw [gapValue_eq _ (by decide)]
+  decide
+
+-- Measuring no qubit gives `2 ^ h`, the denominator of the bounded-error rule.
+example : gapValue [] [(true, 0, []), (true, 0, [])] [true] = 4 := by
+  rw [gapValue_eq _ (by decide)]
   decide
 
 /-! ### A member of `BQTIME` -/
diff --git a/ComplexityTests/QuantumPathNetwork.lean b/ComplexityTests/QuantumPathNetwork.lean
index ebddc4fc6..285c07914 100644
--- a/ComplexityTests/QuantumPathNetwork.lean
+++ b/ComplexityTests/QuantumPathNetwork.lean
@@ -7,7 +7,8 @@ Authors: Samuel Schlesinger
 import Complexity.Computability.Circuit.Quantum.PathNetwork
 
 /-! The tensor network of a circuit and its mirror copy: concrete contractions that equal the
-acceptance gaps of small circuits, computed directly and through `contraction_network`. -/
+acceptance gaps and other projected gaps of small circuits, computed directly and through
+`contraction_network`. -/
 
 namespace ComplexityTests.QuantumPathNetwork
 
@@ -17,50 +18,73 @@ open Cslib Cslib.Quantum Cslib.Quantum.PathNetwork Cslib.Circuits.Frontier
 
 -- One Hadamard gate on `|0⟩`: one of the four pairs of paths accepts, so the gap is `1`. The
 -- network has one occurrence, so four edges: sixteen assignments.
-example : (network (-1 : ℤ) [false] [(true, 0, [])]).2.contraction = 1 := by decide
+example : (network (-1 : ℤ) [0] [false] [(true, 0, [])]).2.contraction = 1 := by decide
 example : acceptGap [(true, 0, [])] [false] = 1 := by decide
 
 -- A NOT gate on `|0⟩` accepts with certainty and has no Hadamard gate.
-example : (network (-1 : ℤ) [false] [(false, 0, [])]).2.contraction = 1 := by decide
+example : (network (-1 : ℤ) [0] [false] [(false, 0, [])]).2.contraction = 1 := by decide
 
 -- A NOT gate on `|1⟩` rejects with certainty.
-example : (network (-1 : ℤ) [true] [(false, 0, [])]).2.contraction = 0 := by decide
+example : (network (-1 : ℤ) [0] [true] [(false, 0, [])]).2.contraction = 0 := by decide
 
 -- Without gates the network is the scalar vertex alone: it reads the input bit of qubit `0`.
-example : (network (-1 : ℤ) [true] []).2.contraction = 1 := by decide
-example : (network (-1 : ℤ) [false] []).2.contraction = 0 := by decide
+example : (network (-1 : ℤ) [0] [true] []).2.contraction = 1 := by decide
+example : (network (-1 : ℤ) [0] [false] []).2.contraction = 0 := by decide
 
 -- An untouched qubit `0` set to one: the gate on qubit `1` does not matter, the gap is `2 ^ 1`.
-example : (network (-1 : ℤ) [true, false] [(true, 1, [])]).2.contraction = 2 := by decide
+example : (network (-1 : ℤ) [0] [true, false] [(true, 1, [])]).2.contraction = 2 := by decide
 
 /-! ### Through the identity -/
 
 -- Two Hadamard gates interfere; the signed entries `-1` cancel the four accepting pairs from
 -- `|0⟩` and add them up from `|1⟩`.
-example : (network (-1 : ℤ) [false] [(true, 0, []), (true, 0, [])]).2.contraction = 0 := by
-  rw [contraction_network _ _ (by decide)]
+example : (network (-1 : ℤ) [0] [false] [(true, 0, []), (true, 0, [])]).2.contraction = 0 := by
+  rw [contraction_network _ _ _ (by decide)]
   decide
-example : (network (-1 : ℤ) [true] [(true, 0, []), (true, 0, [])]).2.contraction = 4 := by
-  rw [contraction_network _ _ (by decide)]
+example : (network (-1 : ℤ) [0] [true] [(true, 0, []), (true, 0, [])]).2.contraction = 4 := by
+  rw [contraction_network _ _ _ (by decide)]
   decide
 
 -- A Hadamard gate copied by a CNOT into qubit `0`: probability `1 / 2`, gap `1`.
-example : (network (-1 : ℤ) [false, false] [(true, 1, []), (false, 0, [1])]).2.contraction = 1 := by
-  rw [contraction_network _ _ (by decide)]
+example :
+    (network (-1 : ℤ) [0] [false, false] [(true, 1, []), (false, 0, [1])]).2.contraction = 1 := by
+  rw [contraction_network _ _ _ (by decide)]
+  decide
+
+/-! ### Other measured qubits -/
+
+-- Measuring no qubit gives the squared norm `2 ^ h`.
+example : (network (-1 : ℤ) [] [false] [(true, 0, [])]).2.contraction = 2 := by decide
+
+-- An untouched measured qubit is read from the input register by the scalar vertex.
+example : (network (-1 : ℤ) [1] [false, true] [(true, 0, [])]).2.contraction = 2 := by decide
+example : (network (-1 : ℤ) [1] [false, false] [(true, 0, [])]).2.contraction = 0 := by decide
+
+-- The Hadamard gate copied into qubit `0` leaves qubits `0` and `1` equal: both read `1` with
+-- probability `1 / 2`, the same as qubit `1` alone.
+example :
+    (network (-1 : ℤ) [0, 1] [false, false] [(true, 1, []), (false, 0, [1])]).2.contraction =
+      1 := by
+  rw [contraction_network _ _ _ (by decide)]
+  decide
+example :
+    (network (-1 : ℤ) [1] [false, false] [(true, 1, []), (false, 0, [1])]).2.contraction = 1 := by
+  rw [contraction_network _ _ _ (by decide)]
   decide
 
 /-! ### Residues over `ℕ` -/
 
 -- Over `ℕ` the Hadamard sign is `2 ^ P - 1`; modulo `2 ^ P` the contraction is the gap.
-example : (network (2 ^ 3 - 1 : ℕ) [true] [(true, 0, []), (true, 0, [])]).2.contraction % 2 ^ 3 =
-    4 := by
-  rw [contraction_network_mod _ (by decide) _ (by decide) (by decide)]
+example :
+    (network (2 ^ 3 - 1 : ℕ) [0] [true] [(true, 0, []), (true, 0, [])]).2.contraction % 2 ^ 3 =
+      4 := by
+  rw [contraction_network_mod _ _ _ (by decide) (by decide)]
   decide
 
 /-! ### Sizes -/
 
 -- Four edges per occurrence: the Toffoli gate has three occurrences.
-example : (network (-1 : ℤ) [false, false, false] [(false, 2, [0, 1])]).2.numEdges = 12 := by
+example : (network (-1 : ℤ) [0] [false, false, false] [(false, 2, [0, 1])]).2.numEdges = 12 := by
   decide
 
 end ComplexityTests.QuantumPathNetwork
diff --git a/ComplexityTests/QuantumTimeClasses.lean b/ComplexityTests/QuantumTimeClasses.lean
new file mode 100644
index 000000000..f43fe7ac2
--- /dev/null
+++ b/ComplexityTests/QuantumTimeClasses.lean
@@ -0,0 +1,183 @@
+/-
+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.TensorContraction
+import ComplexityTests.BQPTensorContraction
+
+/-! Nondeterministic, exact and postselected quantum time: circuits accepting with probability
+strictly between `0` and `1`, exact circuits whose paths interfere, a postselected circuit that
+accepts only after postselection, the classes they witness, and the containments applied to them.
+-/
+
+namespace ComplexityTests.QuantumTimeClasses
+
+open Cslib Cslib.Quantum Cslib.Complexity Cslib.Complexity.QuantumContraction Turing.MultiTapeTM
+  ComplexityTests.BQPTensorContraction
+
+/-- The encoding of the single instance of `Unit` as the empty word. -/
+def encUnit : Unit ↪ List Bool := ⟨fun _ => [], fun _ _ _ => rfl⟩
+
+/-- The family running the fixed gate codes `gs` on `n + k` qubits for inputs of length `n`. -/
+def constFamily (k : ℕ) (hk : 0 < k) (gs : List GateCode)
+    (hgs : ∀ g ∈ gs, ∀ n, g.WellFormed (n + k)) : UniformCircuitFamily where
+  width n := n + k
+  gates _ := gs
+  computableInPolyTime_width := by fun_prop
+  computableInPolyTime_gates := ComputableInPolyTime.const _
+  le_width n := Nat.le_add_right n k
+  width_pos n := by omega
+  wellFormed n g hg := hgs g hg n
+
+/-! ### Nonzero but not exact -/
+
+/-- One Hadamard gate on qubit `0`. -/
+def coin : UniformCircuitFamily :=
+  constFamily 1 (by norm_num) [(true, 0, [])] fun g hg n => by
+    obtain rfl := List.mem_singleton.mp hg
+    simp [GateCode.WellFormed]
+
+-- The coin accepts with probability `1 / 2`: positive, but neither `0` nor `1`.
+theorem acceptProb_coin : coin.acceptProb [] = 1 / 2 := by
+  change acceptProb 1 [(true, 0, [])] [] = 1 / 2
+  rw [acceptProb_eq_acceptGap _ (by decide), show List.ofFn (inputState 1 []) = [false] by decide,
+    show acceptGap [(true, 0, [])] [false] = 1 by decide]
+  norm_num [hadamardCount]
+
+example : 0 < coin.acceptProb [] ∧ coin.acceptProb [] ≠ 1 := by
+  rw [acceptProb_coin]
+  norm_num
+
+/-- The coin puts the instance into `NQTIME`. -/
+theorem univ_mem_NQTIME : (Set.univ : Set Unit) ∈ NQTIME encUnit fun _ => 1 :=
+  ⟨coin, 0, 1, fun _ => le_rfl, fun _ => by
+    change _ ↔ 0 < coin.acceptProb []
+    rw [acceptProb_coin]
+    norm_num⟩
+
+example : (Set.univ : Set Unit) ∈ ⋃ C, DTIME encUnit fun n =>
+    2 ^ (C * (n + 2) / Nat.sqrt (Nat.log 2 (n + 2))) :=
+  NQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (T := fun n => n + 2)
+    (fun n => max_le (by omega) (by omega))
+    (show (Set.univ : Set Unit) ∈ NQTIME encUnit fun n => n + 2 from
+      ⟨coin, 0, 1, fun _ => by simp [coin, constFamily], fun _ => by
+        change _ ↔ 0 < coin.acceptProb []
+        rw [acceptProb_coin]
+        norm_num⟩)
+
+/-! ### Exact -/
+
+/-- Two Hadamard gates on qubit `0`, after a NOT gate when `flip` holds. Their paths interfere, so
+the circuit accepts exactly when `flip` holds. -/
+def twice (flip : Bool) : UniformCircuitFamily :=
+  constFamily 1 (by norm_num)
+    ((if flip then [(false, 0, [])] else []) ++ [(true, 0, []), (true, 0, [])]) fun g hg n => by
+    cases flip <;> simp only [Bool.false_eq_true, ite_false, ite_true, List.nil_append,
+      List.cons_append, List.mem_cons, List.not_mem_nil, or_false] at hg <;>
+      rcases hg with rfl | rfl | rfl <;> simp [GateCode.WellFormed]
+
+-- From `|0⟩` the four accepting pairs of paths cancel; after the NOT gate they add up to `2 ^ 2`.
+theorem acceptProb_twice_false : (twice false).acceptProb [] = 0 := by
+  change acceptProb 1 [(true, 0, []), (true, 0, [])] [] = 0
+  rw [acceptProb_eq_acceptGap _ (by decide), show List.ofFn (inputState 1 []) = [false] by decide,
+    show acceptGap [(true, 0, []), (true, 0, [])] [false] = 0 by decide]
+  norm_num
+
+theorem acceptProb_twice_true : (twice true).acceptProb [] = 1 := by
+  change acceptProb 1 [(false, 0, []), (true, 0, []), (true, 0, [])] [] = 1
+  rw [acceptProb_eq_acceptGap _ (by decide), show List.ofFn (inputState 1 []) = [false] by decide,
+    show acceptGap [(false, 0, []), (true, 0, []), (true, 0, [])] [false] = 4 by decide]
+  norm_num [hadamardCount]
+
+example : (∅ : Set Unit) ∈ EQTIME encUnit fun _ => 1 :=
+  ⟨twice false, 0, 2, fun _ => le_rfl, fun _ =>
+    ⟨fun h => absurd h (Set.notMem_empty _), fun _ => acceptProb_twice_false⟩⟩
+
+example : (Set.univ : Set Unit) ∈ EQTIME encUnit fun _ => 1 :=
+  ⟨twice true, 0, 3, fun _ => le_rfl, fun _ =>
+    ⟨fun _ => acceptProb_twice_true, fun h => absurd (Set.mem_univ _) h⟩⟩
+
+/-- Deciding the first bit takes no gates, exactly. -/
+theorem firstBit_mem_EQTIME (t : ℕ → ℕ) : FirstBit ∈ EQTIME encBits t := by
+  refine ⟨readFirst, 0, 0, fun n => by simp [readFirst], fun x => ⟨fun hx => ?_, fun hx => ?_⟩⟩
+  · rw [encBits_apply, acceptProb_readFirst]
+    simp only [show x.headD false = true from hx, ite_true]
+  · rw [encBits_apply, acceptProb_readFirst]
+    simp only [show x.headD false = false from Bool.eq_false_iff.mpr hx, Bool.false_eq_true,
+      ite_false]
+
+example : FirstBit ∈ NQTIME encBits fun _ => 0 :=
+  EQTIME_subset_NQTIME _ (firstBit_mem_EQTIME _)
+
+example : FirstBit ∈ ⋃ C, DTIME encBits fun n =>
+    2 ^ (C * (n + 2) / Nat.sqrt (Nat.log 2 (n + 2))) :=
+  EQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (T := fun n => n + 2)
+    (fun n => max_le (by omega) (by omega)) (firstBit_mem_EQTIME _)
+
+/-! ### Postselection -/
+
+/-- The gate codes of `postselect`: two fair coins on qubits `2` and `3`, and their conjunction
+written into qubits `0` and `1`. -/
+def postselectCodes : List GateCode :=
+  [(true, 2, []), (true, 3, []), (false, 0, [2, 3]), (false, 1, [2, 3])]
+
+/-- Two fair coins whose conjunction is written into qubits `0` and `1`: qubit `0` reads `1` with
+probability `1 / 4`, but always once qubit `1` reads `1`. -/
+def postselect : UniformCircuitFamily :=
+  constFamily 4 (by norm_num) postselectCodes fun g hg n => by
+    simp only [postselectCodes, List.mem_cons, List.not_mem_nil, or_false] at hg
+    rcases hg with rfl | rfl | rfl | rfl <;> simp [GateCode.WellFormed]
+
+theorem onesProb_postselect (S : List ℕ) :
+    postselect.onesProb S [] =
+      (onesGap S postselectCodes [false, false, false, false] : ℝ) / 4 := by
+  change onesProb 4 postselectCodes S [] = _
+  rw [onesProb_eq_onesGap _ (by decide),
+    show List.ofFn (inputState 4 []) = [false, false, false, false] by decide,
+    show hadamardCount postselectCodes = 2 by decide]
+  norm_num
+
+-- Without postselection the circuit rejects: it accepts with probability `1 / 4`.
+example : postselect.acceptProb [] = 1 / 4 := by
+  rw [UniformCircuitFamily.acceptProb_eq_onesProb, onesProb_postselect,
+    show onesGap [0] postselectCodes [false, false, false, false] = 1 by decide]
+  norm_num
+
+-- Qubit `1` reads `1` with probability `1 / 4`, and then so does qubit `0`.
+theorem onesProb_postselect_one : postselect.onesProb [1] [] = 1 / 4 := by
+  rw [onesProb_postselect, show onesGap [1] postselectCodes [false, false, false, false] = 1 by
+    decide]
+  norm_num
+
+theorem postselectedAcceptProb_postselect : postselect.postselectedAcceptProb [] = 1 := by
+  rw [UniformCircuitFamily.postselectedAcceptProb, onesProb_postselect_one, onesProb_postselect,
+    show onesGap [0, 1] postselectCodes [false, false, false, false] = 1 by decide]
+  norm_num
+
+-- The simulator computes both projected gaps.
+example : gapValue [0, 1] postselectCodes [false, false, false, false] = 1 := by
+  rw [gapValue_eq _ (by decide)]
+  decide
+example : gapValue [1] postselectCodes [false, false, false, false] = 1 := by
+  rw [gapValue_eq _ (by decide)]
+  decide
+
+/-- Postselection puts the instance into `PostBQTIME`. -/
+theorem univ_mem_PostBQTIME (t : ℕ → ℕ) : (Set.univ : Set Unit) ∈ PostBQTIME encUnit t := by
+  refine ⟨postselect, 0, 4, fun _ => by simp [postselect, constFamily, postselectCodes],
+    fun _ => ⟨?_, fun _ => ?_, fun h => absurd (Set.mem_univ _) h⟩⟩
+  · change 0 < postselect.onesProb [1] []
+    rw [onesProb_postselect_one]
+    norm_num
+  · change 2 / 3 ≤ postselect.postselectedAcceptProb []
+    rw [postselectedAcceptProb_postselect]
+    norm_num
+
+example : (Set.univ : Set Unit) ∈ ⋃ C, DTIME encUnit fun n =>
+    2 ^ (C * (n + 2) / Nat.sqrt (Nat.log 2 (n + 2))) :=
+  PostBQTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (T := fun n => n + 2)
+    (fun n => max_le (by omega) (by omega)) (univ_mem_PostBQTIME _)
+
+end ComplexityTests.QuantumTimeClasses
diff --git a/references.bib b/references.bib
index 925a848de..33404174c 100644
--- a/references.bib
+++ b/references.bib
@@ -1,3 +1,18 @@
+@article{Aaronson2005Postselection,
+  author    = {Aaronson, Scott},
+  title     = {Quantum Computing, Postselection, and Probabilistic Polynomial-Time},
+  journal   = {Proceedings of the Royal Society A: Mathematical, Physical and Engineering
+               Sciences},
+  volume    = {461},
+  number    = {2063},
+  pages     = {3473--3482},
+  year      = {2005},
+  doi       = {10.1098/rspa.2005.1546},
+  eprint    = {quant-ph/0412187},
+  archivePrefix = {arXiv},
+  note      = {Locators follow arXiv:quant-ph/0412187v1}
+}
+
 @inproceedings{AaronsonBenDavidKothariRaoTal2021,
   author    = {Aaronson, Scott and Ben-David, Shalev and Kothari, Robin and Rao, Shravas and
                Tal, Avishay},
@@ -1692,6 +1707,22 @@ @article{FennerFortnowKurtz1994
   doi       = {10.1016/S0022-0000(05)80024-8}
 }
 
+@article{FennerGreenHomerPruim1999,
+  author    = {Fenner, Stephen and Green, Frederic and Homer, Steven and Pruim, Randall},
+  title     = {Determining Acceptance Possibility for a Quantum Computation is Hard for the
+               Polynomial Hierarchy},
+  journal   = {Proceedings of the Royal Society of London. Series A: Mathematical, Physical and
+               Engineering Sciences},
+  volume    = {455},
+  number    = {1991},
+  pages     = {3953--3966},
+  year      = {1999},
+  doi       = {10.1098/rspa.1999.0485},
+  eprint    = {quant-ph/9812056},
+  archivePrefix = {arXiv},
+  note      = {Locators follow arXiv:quant-ph/9812056v1}
+}
+
 @article{Fenwick1994,
   author    = {Fenwick, Peter M.},
   title     = {A New Data Structure for Cumulative Frequency Tables},