diff --git a/Complexity.lean b/Complexity.lean
index 6d49d14900..daad6ceafd 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1873,6 +1873,8 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.D
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.Graph
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.GraphPolyTime
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.Table
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.TablePolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/Table.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/Table.lean
new file mode 100644
index 0000000000..78b02e38b8
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/Table.lean
@@ -0,0 +1,802 @@
+/-
+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.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.Graph
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount
+
+/-!
+# The tables of an explicit block-counting network, on numbers
+
+The tables of the explicit block-counting network of a schedule
+(`Turing.MultiTapePTM.explicitBlockNetwork`) are values of the tensors of the block-counting
+network (`Turing.MultiTapePTM.blockNetwork`) at letters read from the bits of a table index. This
+module computes them from numbers, the form in which a polynomial-time construction produces
+them.
+
+* **Letters from numbers.** A letter is read as its number (`Turing.MultiTapePTM.letterEquiv`),
+  and every natural number is decoded to a letter (`Turing.MultiTapePTM.decodeLetter`), inverting
+  the numbering (`Turing.MultiTapePTM.decodeLetter_letterEquiv`). The control record of a number
+  is computed on plain data by division and remainder (`Turing.MultiTapePTM.decodeControlData`),
+  and so are the cells of block contents (`Turing.MultiTapePTM.contentsCellNum`) and the accepting
+  weight (`Turing.MultiTapePTM.acceptNum`).
+* **The window entering an interval.** The previous appearance of a block in windows is a search
+  over the earlier intervals (`Turing.MultiTapePTM.lastBeforeNum_eq`), and its window entry is a
+  digit-count difference (`Turing.MultiTapePTM.portOfNum`).
+* **The tensors on numbers.** Given the numbers of the letters on all edges, the tensor of an
+  interval is an interval count on plain data (`Turing.MultiTapePTM.localIntervalCount`) when the
+  letters leaving it have the right kinds, and zero otherwise; the sinks are the accepting weight
+  or `1` (`Turing.MultiTapePTM.blockNetwork_tensor_decodeLetter`).
+
+## Main definitions
+
+* `Turing.MultiTapePTM.decodeControlData`, `Turing.MultiTapePTM.decodeLetter`,
+  `Turing.MultiTapePTM.contentsCellNum`, `Turing.MultiTapePTM.acceptNum`: decoding letters.
+* `Turing.MultiTapePTM.lastBeforeNum`, `Turing.MultiTapePTM.portOfNum`: previous appearances and
+  window entries on numbers.
+* `Turing.MultiTapePTM.intervalEntryNum`, `Turing.MultiTapePTM.oldEntryNum`: the tensors of the
+  block-counting network on numbers.
+
+## Main results
+
+* `Turing.MultiTapePTM.decodeControlData_controlEquiv`,
+  `Turing.MultiTapePTM.decodeLetter_letterEquiv`: decoding inverts the numberings.
+* `Turing.MultiTapePTM.card_intervalHolds`: the tensor of an interval is an interval count.
+* `Turing.MultiTapePTM.blockNetwork_tensor_decodeLetter`: the tensors on numbers.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM
+
+open Cslib.Circuits.Frontier MultiTapeNTM.ChoiceTable
+
+variable {k q s : ℕ} {State : Type}
+
+/-! ### Products of numberings -/
+
+private theorem val_finProdFinEquiv_div {m n : ℕ} (x : Fin m × Fin n) :
+    (finProdFinEquiv x : ℕ) / n = x.1 := by
+  have := x.2.isLt
+  rw [finProdFinEquiv_apply_val, Nat.add_mul_div_left _ _ (by omega), Nat.div_eq_of_lt x.2.isLt,
+    zero_add]
+
+private theorem val_finProdFinEquiv_mod {m n : ℕ} (x : Fin m × Fin n) :
+    (finProdFinEquiv x : ℕ) % n = x.2 := by
+  rw [finProdFinEquiv_apply_val, Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt x.2.isLt]
+
+/-- Digit `r < b` in base `3` of a number is that of its remainder modulo `3 ^ b`. -/
+private theorem mod_pow_div_pow_mod (x : ℕ) {r b : ℕ} (hr : r < b) :
+    x % 3 ^ b / 3 ^ r % 3 = x / 3 ^ r % 3 := by
+  obtain ⟨d, rfl⟩ : ∃ d, b = r + (d + 1) := ⟨b - r - 1, by omega⟩
+  rw [pow_add, Nat.mod_mul_right_div_self, Nat.mod_mod_of_dvd _ (dvd_pow_self 3 (by omega))]
+
+private theorem equivFin_symm_eq_accept_iff {t : ℕ} (ht : t < 3) :
+    OutputTrack.equivFin.symm ⟨t, ht⟩ = .accept ↔ t = 1 := by
+  interval_cases t <;> simp [OutputTrack.equivFin]
+
+/-! ### Decoding letters -/
+
+/-- The number of control records, which come first among the letters. -/
+@[expose] def controlCount (k s b : ℕ) : ℕ := (s + 1) * (b ^ (k + 1) * 3)
+
+/-- The number of letters. -/
+@[expose] def letterCount (k s b : ℕ) : ℕ := controlCount k s b + 3 ^ b
+
+section Decode
+
+variable (e : State ≃ Fin s) (b : ℕ)
+
+/-- The state numbered `i ≤ s`: none for `0`, and the state numbered `i - 1` by `e` otherwise. -/
+@[expose] def stateOfFin (i : Fin (s + 1)) : Option State :=
+  ((Equiv.optionCongr e).trans (finSuccEquiv s).symm).symm i
+
+/-- **The control record of a number**, on plain data: the state from the quotient by
+`b ^ (k + 1) * 3` (capped at `s`), the offsets as digits in base `b` and the output track from the
+remainder. -/
+@[expose] def decodeControlData (n : ℕ) : ControlData k State :=
+  (stateOfFin e ⟨min s (n / (b ^ (k + 1) * 3)) % (s + 1), Nat.mod_lt _ (by omega)⟩,
+    fun head => n % (b ^ (k + 1) * 3) / 3 / b ^ ((finSuccEquiv k).symm head : ℕ) % b,
+    OutputTrack.equivFin.symm ⟨n % (b ^ (k + 1) * 3) % 3, Nat.mod_lt _ (by omega)⟩)
+
+/-- **Decoding control records inverts their numbering.** -/
+theorem decodeControlData_controlEquiv [NeZero b] (c : BlockControl k State b) :
+    decodeControlData e b (controlEquiv e c) = controlData c := by
+  obtain ⟨st, off, tr⟩ := c
+  set x := controlEquiv e (st, off, tr)
+  have hx : (x : ℕ) = (finProdFinEquiv (((Equiv.optionCongr e).trans (finSuccEquiv s).symm) st,
+      finProdFinEquiv (finFunctionFinEquiv fun c => zmodEquiv b (off (finSuccEquiv k c)),
+        OutputTrack.equivFin tr)) : ℕ) := rfl
+  have hdiv : (x : ℕ) / (b ^ (k + 1) * 3) =
+      ((Equiv.optionCongr e).trans (finSuccEquiv s).symm) st := by
+    rw [hx, val_finProdFinEquiv_div]
+  have hmod : (x : ℕ) % (b ^ (k + 1) * 3) = (finProdFinEquiv (finFunctionFinEquiv fun c =>
+      zmodEquiv b (off (finSuccEquiv k c)), OutputTrack.equivFin tr) : ℕ) := by
+    rw [hx, val_finProdFinEquiv_mod]
+  have hst : stateOfFin e ⟨min s ((x : ℕ) / (b ^ (k + 1) * 3)) % (s + 1),
+      Nat.mod_lt _ (by omega)⟩ = st := by
+    have hlt := (((Equiv.optionCongr e).trans (finSuccEquiv s).symm) st).isLt
+    have hfin : (⟨min s ((x : ℕ) / (b ^ (k + 1) * 3)) % (s + 1), Nat.mod_lt _ (by omega)⟩ :
+        Fin (s + 1)) = ((Equiv.optionCongr e).trans (finSuccEquiv s).symm) st := by
+      ext
+      simp only
+      rw [hdiv, Nat.min_eq_right (by omega), Nat.mod_eq_of_lt hlt]
+    rw [hfin, stateOfFin, Equiv.symm_apply_apply]
+  have htr : OutputTrack.equivFin.symm ⟨(x : ℕ) % (b ^ (k + 1) * 3) % 3,
+      Nat.mod_lt _ (by omega)⟩ = tr := by
+    have hfin : (⟨(x : ℕ) % (b ^ (k + 1) * 3) % 3, Nat.mod_lt _ (by omega)⟩ : Fin 3) =
+        OutputTrack.equivFin tr := by
+      ext
+      simp only
+      rw [hmod, val_finProdFinEquiv_mod]
+    rw [hfin, Equiv.symm_apply_apply]
+  have hoff : ∀ head,
+      (x : ℕ) % (b ^ (k + 1) * 3) / 3 / b ^ ((finSuccEquiv k).symm head : ℕ) % b =
+        (off head).val := by
+    intro head
+    rw [hmod, val_finProdFinEquiv_div, ← finFunctionFinEquiv_symm_apply_val,
+      Equiv.symm_apply_apply, val_zmodEquiv, Equiv.apply_symm_apply]
+  simp only [decodeControlData, controlData, hst, htr, hoff]
+
+/-- The control record entering an interval from a letter number: the decoded record of a control
+letter, and the default record of block contents. -/
+@[expose] def controlDataOfNum (n : ℕ) : ControlData k State :=
+  if n < controlCount k s b then decodeControlData e b n else (none, fun _ => 0, .empty)
+
+/-- The cell `r` of the block contents numbered `n`, blank for a control record. -/
+@[expose] def contentsCellNum (k s b n r : ℕ) : Option Bool :=
+  if n < controlCount k s b then none
+  else cellEquiv.symm ⟨(n - controlCount k s b) / 3 ^ r % 3, Nat.mod_lt _ (by omega)⟩
+
+/-- The accepting weight of the letter numbered `n`: one for a control record with output track
+`accept`. -/
+@[expose] def acceptNum (k s b n : ℕ) : ℕ :=
+  if n < controlCount k s b ∧ n % (b ^ (k + 1) * 3) % 3 = 1 then 1 else 0
+
+variable [NeZero b]
+
+/-- **The letter of a number**: the control record of that number for a number below
+`controlCount`, and otherwise the block contents of the remainder of `n - controlCount` modulo
+`3 ^ b`. Below `letterCount` this inverts `Turing.MultiTapePTM.letterEquiv`. -/
+@[expose] def decodeLetter (n : ℕ) : BlockLetter k State b :=
+  if h : n < controlCount k s b then .inl ((controlEquiv e).symm ⟨n, h⟩)
+  else .inr ((contentsEquiv b).symm
+    ⟨(n - controlCount k s b) % 3 ^ b, Nat.mod_lt _ (by positivity)⟩)
+
+/-- **Decoding letters inverts their numbering.** -/
+theorem decodeLetter_letterEquiv (l : BlockLetter k State b) :
+    decodeLetter e b (letterEquiv e l) = l := by
+  rcases l with c | w
+  · have hval : (letterEquiv e (.inl c) : ℕ) = controlEquiv e c := by
+      simp [letterEquiv]
+    have hlt : (letterEquiv e (.inl c) : ℕ) < controlCount k s b := by
+      rw [hval]
+      exact (controlEquiv e c).isLt
+    rw [decodeLetter, dite_eq_left hlt]
+    congr 1
+    rw [Equiv.symm_apply_eq]
+    exact Fin.ext hval.symm
+  · have hval : (letterEquiv e (.inr w : BlockLetter k State b) : ℕ) =
+        controlCount k s b + contentsEquiv b w := by
+      simp [letterEquiv, controlCount]
+    rw [decodeLetter, dite_eq_right (by omega)]
+    congr 1
+    rw [Equiv.symm_apply_eq]
+    ext
+    simp only [hval, Nat.add_sub_cancel_left]
+    exact Nat.mod_eq_of_lt (contentsEquiv b w).isLt
+
+/-- Below `letterCount`, the letter of a number is the numbered letter. -/
+theorem decodeLetter_of_lt {n : ℕ} (hn : n < letterCount k s b) :
+    decodeLetter e b n = (letterEquiv e).symm ⟨n, hn⟩ := by
+  conv_lhs => rw [show n = (letterEquiv e ((letterEquiv e).symm ⟨n, hn⟩) : ℕ) by simp]
+  exact decodeLetter_letterEquiv e b _
+
+/-- The control record of a decoded letter. -/
+theorem controlData_control_decodeLetter (n : ℕ) :
+    controlData (decodeLetter (k := k) e b n).control = controlDataOfNum e b n := by
+  unfold decodeLetter controlDataOfNum
+  split_ifs with h
+  · simp only [BlockLetter.control]
+    rw [← decodeControlData_controlEquiv e b, Equiv.apply_symm_apply]
+  · simp only [BlockLetter.control, controlData, Pi.zero_apply, ZMod.val_zero]
+
+/-- The cells of a decoded letter. -/
+theorem contents_decodeLetter (n : ℕ) (r : ZMod b) :
+    (decodeLetter (k := k) e b n).contents r = contentsCellNum k s b n r.val := by
+  unfold decodeLetter contentsCellNum
+  split_ifs with h
+  · rfl
+  · simp only [BlockLetter.contents, contentsEquiv, Equiv.symm_trans_apply, Equiv.arrowCongr_symm,
+      Equiv.arrowCongr_apply, Function.comp_apply, Equiv.symm_symm]
+    congr 1
+    ext
+    rw [finFunctionFinEquiv_symm_apply_val]
+    simp only [val_zmodEquiv]
+    exact mod_pow_div_pow_mod _ (ZMod.val_lt r)
+
+/-- The accepting weight of a decoded letter. -/
+theorem acceptWeight_decodeLetter (n : ℕ) :
+    acceptWeight (decodeLetter (k := k) e b n) = acceptNum k s b n := by
+  unfold decodeLetter acceptNum
+  by_cases h : n < controlCount k s b
+  · have hc := decodeControlData_controlEquiv e b ((controlEquiv e).symm ⟨n, h⟩)
+    rw [Equiv.apply_symm_apply] at hc
+    have htr := congrArg (fun c => c.2.2) hc
+    simp only [decodeControlData, controlData] at htr
+    simp only [h, ↓reduceDIte, acceptWeight, ← htr, equivFin_symm_eq_accept_iff, true_and]
+  · simp only [h, ↓reduceDIte, acceptWeight, false_and, ↓reduceIte]
+
+end Decode
+
+/-! ### The window entering an interval, on numbers -/
+
+/-- The last interval before `i` whose window contains the block `δ` of interval `i`'s window,
+for the head with digit offset `c`, found by searching the earlier intervals from the latest. -/
+@[expose] def lastBeforeNum (k σ c i δ : ℕ) : Option ℕ :=
+  ((List.range i).find? fun j => inWindowNum k σ c i δ (i - 1 - j)).map fun j => i - 1 - j
+
+/-- **Previous appearances on numbers.** -/
+theorem lastBeforeNum_eq (σ : ℕ) (i : Fin q) (h : Fin k) (δ : Fin 3) :
+    lastBeforeNum k σ (h + 1) i δ =
+      (lastBefore (InWindow (scheduleOfNat k q σ) h
+        (portBlock (scheduleOfNat k q σ) i h δ)) i).map Fin.val := by
+  cases hl : lastBefore (InWindow (scheduleOfNat k q σ) h
+      (portBlock (scheduleOfNat k q σ) i h δ)) i with
+  | none =>
+    rw [lastBefore_eq_none_iff] at hl
+    simp only [Option.map_none, lastBeforeNum, Option.map_eq_none_iff, List.find?_eq_none,
+      List.mem_range]
+    intro j hj hw
+    exact hl ⟨i - 1 - j, by omega⟩ (Fin.lt_def.mpr (by simp only; omega))
+      ((inWindowNum_iff σ i ⟨i - 1 - j, by omega⟩ h δ).mp hw)
+  | some i' =>
+    obtain ⟨hlt, hw, hmax⟩ := lastBefore_eq_some_iff.mp hl
+    have hlt' : (i' : ℕ) < i := hlt
+    have hfind : (List.range i).find? (fun j => inWindowNum k σ (h + 1) i δ (i - 1 - j)) =
+        some ((i : ℕ) - 1 - i') := by
+      rw [List.find?_range_eq_some]
+      refine ⟨?_, List.mem_range.mpr (by omega), fun j hj => ?_⟩
+      · rw [show (i : ℕ) - 1 - (i - 1 - i') = i' by omega]
+        exact (inWindowNum_iff σ i i' h δ).mpr hw
+      · rw [Bool.not_eq_true', Bool.eq_false_iff, ne_eq,
+          inWindowNum_iff σ i ⟨i - 1 - j, by omega⟩ h δ]
+        exact hmax ⟨i - 1 - j, by omega⟩ (Fin.lt_def.mpr (by simp only; omega))
+          (Fin.lt_def.mpr (by simp only; omega))
+    simp only [lastBeforeNum, hfind, Option.map_some, Option.some.injEq]
+    omega
+
+/-- The window entry, in the window of interval `i'`, of the block `δ` of interval `i`'s window,
+for the head with digit offset `c`: `b(i) + δ - b(i') mod 3` from the digit counts. -/
+@[expose] def portOfNum (k σ c i i' δ : ℕ) : ℕ :=
+  (digitCount k σ c 2 i + digitCount k σ c 0 i' + δ -
+    (digitCount k σ c 0 i + digitCount k σ c 2 i')) % 3
+
+/-- **Window entries on numbers.** -/
+theorem val_portOf (σ : ℕ) (i i' : Fin q) (h : Fin k) (δ : Fin 3) :
+    (portOf (scheduleOfNat k q σ) i' h (portBlock (scheduleOfNat k q σ) i h δ) : ℕ) =
+      portOfNum k σ (h + 1) i i' δ := by
+  have hc : (((finSuccEquiv k).symm (some h) : Fin (k + 1)) : ℕ) = h + 1 := by simp
+  have hb := scheduleBlock_scheduleOfNat (k := k) σ i.isLt.le (some h)
+  have hb' := scheduleBlock_scheduleOfNat (k := k) σ i'.isLt.le (some h)
+  rw [hc] at hb hb'
+  simp only [portOf, portBlock, hb, hb', portOfNum]
+  congr 1
+  omega
+
+/-! ### The tensor of an interval -/
+
+section Interval
+
+variable (machine : MultiTapePTM k Bool State) (input : List Bool) (b : ℕ) (σ : Schedule k q)
+
+open scoped Classical in
+/-- **The tensor of an interval is an interval count** when the letters leaving it are a control
+record and block contents. -/
+theorem card_intervalHolds (i : Fin q) {x : BlockEdge k q → BlockLetter k State b}
+    {cOut : BlockControl k State b} {wOut : Fin k → Fin 3 → ZMod b → Option Bool}
+    (hc : x (.inl i) = .inl cOut) (hw : ∀ h d, x (.inr (i, h, d)) = .inr (wOut h d)) :
+    (Finset.univ.filter fun u => machine.IntervalHolds input b σ i x u).card =
+      machine.intervalCount b input (scheduleBlock σ i) (σ i) (machine.inControl b i x)
+        (inWindow σ i x) cOut wOut := by
+  unfold intervalCount
+  congr 1
+  ext u
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and, IntervalHolds, hc, hw, Sum.inl.injEq,
+    Sum.inr.injEq]
+  constructor
+  · rintro ⟨c', w', hstep, rfl, hw'⟩
+    obtain rfl : w' = wOut := funext fun h => funext fun d => (hw' h d).symm
+    exact hstep
+  · exact fun hstep => ⟨cOut, wOut, hstep, rfl, fun _ _ => rfl⟩
+
+open scoped Classical in
+/-- The tensor of an interval vanishes when a letter leaving it has the wrong kind. -/
+theorem card_intervalHolds_eq_zero (i : Fin q) {x : BlockEdge k q → BlockLetter k State b}
+    (hx : ¬ ((∃ cOut, x (.inl i) = .inl cOut) ∧ ∀ h d, ∃ w, x (.inr (i, h, d)) = .inr w)) :
+    (Finset.univ.filter fun u => machine.IntervalHolds input b σ i x u).card = 0 := by
+  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
+  rintro u - ⟨cOut, wOut, -, hc, hw⟩
+  exact hx ⟨⟨cOut, hc⟩, fun h d => ⟨_, hw h d⟩⟩
+
+end Interval
+
+/-! ### The tensors on numbers -/
+
+section Tensors
+
+variable (e : State ≃ Fin s) (b : ℕ)
+
+/-- The block indices at the start of interval `i` of the schedule of `σ`, as digit counts. -/
+@[expose] def blockIndexNum (k σ i : ℕ) : Option (Fin k) → ℤ := fun head =>
+  (digitCount k σ ((finSuccEquiv k).symm head) 2 i : ℤ) -
+    digitCount k σ ((finSuccEquiv k).symm head) 0 i
+
+/-- The movements of the blocks in interval `i` of the schedule of `σ`. -/
+@[expose] def blockMoveNum (k σ i : ℕ) : Option (Fin k) → SignType := fun head =>
+  signEquiv.symm ⟨σ / 3 ^ (((finSuccEquiv k).symm head : ℕ) + (k + 1) * i) % 3,
+    Nat.mod_lt _ (by norm_num)⟩
+
+/-- The control record entering interval `i`, from the letter numbers `L` of the edges. -/
+@[expose] def inControlNum (initial : State) (L : ℕ → ℕ) (i : ℕ) : ControlData k State :=
+  if i = 0 then (some initial, fun _ => 0, .empty) else controlDataOfNum e b (L (i - 1))
+
+/-- The cells of the window of work tape `h` entering interval `i`, from the letter numbers `L`
+of the edges of a schedule number `σ` with `q` intervals. -/
+@[expose] def inCellsNum (k q s b σ : ℕ) (L : ℕ → ℕ) (i h : ℕ) : List (Option Bool) :=
+  (List.range (3 * b)).map fun c =>
+    (lastBeforeNum k σ (h + 1) i (c / b)).elim none fun i' =>
+      contentsCellNum k s b (L (q + (portOfNum k σ (h + 1) i i' (c / b) + 3 * h + k * 3 * i')))
+        (c % b)
+
+/-- The cells of the window of work tape `h` leaving interval `i`, from the letter numbers `L`
+of the edges. -/
+@[expose] def outCellsNum (k q s b : ℕ) (L : ℕ → ℕ) (i h : ℕ) : List (Option Bool) :=
+  (List.range (3 * b)).map fun c =>
+    contentsCellNum k s b (L (q + (c / b + 3 * h + k * 3 * i))) (c % b)
+
+variable [DecidableEq State] (machine : MultiTapePTM k Bool State) (input : List Bool)
+
+/-- **The tensor of interval `i` on numbers**, from the letter numbers `L` of the edges: the
+interval count on plain data when the control edge leaving `i` carries a control record and its
+block edges carry block contents, and zero otherwise. -/
+@[expose] def intervalEntryNum (q σ : ℕ) (L : ℕ → ℕ) (i : ℕ) : ℕ :=
+  if L i < controlCount k s b ∧
+      ∀ h : Fin k, ∀ δ : Fin 3, ¬ L (q + (δ + 3 * h + k * 3 * i)) < controlCount k s b then
+    machine.localIntervalCount b input (blockIndexNum k σ i) (blockMoveNum k σ i)
+      (inControlNum e b machine.initial L i) (fun h => inCellsNum k q s b σ L i h)
+      (decodeControlData e b (L i)) (fun h => outCellsNum k q s b L i h)
+  else 0
+
+/-- **The tensor of an old vertex on numbers**: an interval (`v < q`), or the sink of the edge
+numbered `v - q`, which accepts the last control record and is `1` otherwise. -/
+@[expose] def oldEntryNum (q σ : ℕ) (L : ℕ → ℕ) (v : ℕ) : ℕ :=
+  if v < q then intervalEntryNum e b machine input q σ L v
+  else if v - q + 1 = q then acceptNum k s b (L (v - q)) else 1
+
+end Tensors
+
+/-! ### The tensors of the block-counting network on numbers -/
+
+section TensorEq
+
+variable (e : State ≃ Fin s) (b : ℕ) [NeZero b]
+
+/-- A decoded letter is a control record exactly below `controlCount`. -/
+theorem exists_decodeLetter_eq_inl_iff (n : ℕ) :
+    (∃ c, decodeLetter (k := k) e b n = .inl c) ↔ n < controlCount k s b := by
+  unfold decodeLetter
+  split_ifs with h
+  · exact iff_of_true ⟨_, rfl⟩ h
+  · exact iff_of_false (by rintro ⟨c, hc⟩; cases hc) h
+
+/-- A decoded letter is block contents exactly from `controlCount` on. -/
+theorem exists_decodeLetter_eq_inr_iff (n : ℕ) :
+    (∃ w, decodeLetter (k := k) e b n = .inr w) ↔ ¬ n < controlCount k s b := by
+  unfold decodeLetter
+  split_ifs with h
+  · exact iff_of_false (by rintro ⟨c, hc⟩; cases hc) (not_not.mpr h)
+  · exact iff_of_true ⟨_, rfl⟩ h
+
+variable [DecidableEq State] (machine : MultiTapePTM k Bool State) (input : List Bool)
+
+/-- **The tensors of the block-counting network on numbers.** At the letters decoded from numbers
+`L` of the edges (`Turing.MultiTapePTM.decodeLetter`), the tensor of an old vertex of the explicit
+network is `Turing.MultiTapePTM.oldEntryNum` at its number. -/
+theorem blockNetwork_tensor_decodeLetter (σ : ℕ) (u : Fin q ⊕ BlockEdge k q) (L : ℕ → ℕ) :
+    (machine.blockNetwork input b (scheduleOfNat k q σ)).tensor u
+        (fun e' => decodeLetter e b (L (blockEdgeEquiv k q e'))) =
+      oldEntryNum e b machine input q σ L
+        (explicitVertexEquiv k q (letterBits k s b) (.inl u)) := by
+  set x : BlockEdge k q → BlockLetter k State b :=
+    fun e' => decodeLetter e b (L (blockEdgeEquiv k q e'))
+  rcases u with i | i | ⟨i, h₀, d₀⟩
+  · rw [val_explicitVertexEquiv_interval, oldEntryNum, ite_eq_left i.isLt, intervalEntryNum,
+      blockNetwork_tensor_interval]
+    have hxl : x (.inl i) = decodeLetter e b (L i) := by
+      simp only [x, val_blockEdgeEquiv_inl]
+    have hxr : ∀ (i' : Fin q) h d, x (.inr (i', h, d)) =
+        decodeLetter e b (L (q + (d + 3 * h + k * 3 * i'))) := by
+      intro i' h d
+      simp only [x, val_blockEdgeEquiv_inr]
+    split_ifs with hcond
+    · obtain ⟨hctl, hblk⟩ := hcond
+      have hc : x (.inl i) = .inl (x (.inl i)).control := by
+        obtain ⟨c, hc⟩ := (exists_decodeLetter_eq_inl_iff e b _).mpr hctl
+        rw [hxl, hc]
+        rfl
+      have hw : ∀ h d, x (.inr (i, h, d)) = .inr (x (.inr (i, h, d))).contents := by
+        intro h d
+        obtain ⟨w, hw⟩ := (exists_decodeLetter_eq_inr_iff e b _).mpr (hblk h d)
+        rw [hxr, hw]
+        rfl
+      rw [card_intervalHolds machine input b _ i hc hw, ← localIntervalCount_eq_intervalCount]
+      congr 1
+      · funext head
+        exact scheduleBlock_scheduleOfNat σ i.isLt.le head
+      · unfold inControl inControlNum
+        split_ifs with h0
+        · simp only [controlData, Pi.zero_apply, ZMod.val_zero]
+        · have : x (.inl ⟨i - 1, by omega⟩) = decodeLetter e b (L (i - 1)) := by
+            simp only [x, val_blockEdgeEquiv_inl]
+          rw [this, controlData_control_decodeLetter]
+      · funext h
+        unfold windowCells inCellsNum
+        refine List.map_congr_left fun c hc => ?_
+        have hc3 : c / b < 3 := by
+          rw [Nat.div_lt_iff_lt_mul (Nat.pos_of_neZero b)]
+          simpa [Nat.mul_comm] using List.mem_range.mp hc
+        rw [dite_eq_left hc3, inWindow, lastBeforeNum_eq σ i h ⟨c / b, hc3⟩]
+        cases lastBefore (InWindow (scheduleOfNat k q σ) h
+            (portBlock (scheduleOfNat k q σ) i h ⟨c / b, hc3⟩)) i with
+        | none => rfl
+        | some i' =>
+          simp only [Option.elim_some, Option.map_some]
+          rw [hxr, contents_decodeLetter, ZMod.val_natCast, val_portOf σ i i' h ⟨c / b, hc3⟩]
+      · rw [hxl, controlData_control_decodeLetter, controlDataOfNum, ite_eq_left hctl]
+      · funext h
+        unfold windowCells outCellsNum
+        refine List.map_congr_left fun c hc => ?_
+        have hc3 : c / b < 3 := by
+          rw [Nat.div_lt_iff_lt_mul (Nat.pos_of_neZero b)]
+          simpa [Nat.mul_comm] using List.mem_range.mp hc
+        rw [dite_eq_left hc3]
+        simp only
+        rw [hxr, contents_decodeLetter, ZMod.val_natCast]
+    · refine card_intervalHolds_eq_zero machine input b _ i fun ⟨⟨c, hc⟩, hw⟩ => hcond ⟨?_, ?_⟩
+      · rw [hxl] at hc
+        exact (exists_decodeLetter_eq_inl_iff e b _).mp ⟨c, hc⟩
+      · intro h d
+        obtain ⟨w, hw⟩ := hw h d
+        rw [hxr] at hw
+        exact (exists_decodeLetter_eq_inr_iff e b _).mp ⟨w, hw⟩
+  · rw [val_explicitVertexEquiv_sink, val_blockEdgeEquiv_inl, oldEntryNum,
+      ite_eq_right (by omega), blockNetwork_tensor_controlSink, Nat.add_sub_cancel_left]
+    have hxl : x (.inl i) = decodeLetter e b (L i) := by
+      simp only [x, val_blockEdgeEquiv_inl]
+    rw [hxl, acceptWeight_decodeLetter]
+  · rw [val_explicitVertexEquiv_sink, val_blockEdgeEquiv_inr, oldEntryNum,
+      ite_eq_right (by omega), ite_eq_right (by omega), blockNetwork_tensor_blockSink]
+
+end TensorEq
+
+/-! ### Reading letters from table indices -/
+
+section Read
+
+variable (e : State ≃ Fin s) (b : ℕ) [NeZero b]
+
+/-- Bits are the code of a letter exactly when they write its number. -/
+theorem letterCode_eq_iff (l : BlockLetter k State b) (bits : Fin (letterBits k s b) → Bool) :
+    letterCode e l = bits ↔ (letterEquiv e l : ℕ) = Cslib.BitString.lsbValue (List.ofFn bits) := by
+  have hlt : (letterEquiv e l : ℕ) < 2 ^ letterBits k s b :=
+    (letterEquiv e l).isLt.trans_le card_letter_le_two_pow
+  constructor
+  · rintro rfl
+    refine Nat.eq_of_testBit_eq fun i => ?_
+    rw [Cslib.BitString.testBit_lsbValue]
+    by_cases hi : i < letterBits k s b
+    · rw [List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_ofFn]
+      rfl
+    · rw [List.getD_eq_default _ _ (by simpa using hi),
+        Nat.testBit_lt_two_pow (hlt.trans_le (Nat.pow_le_pow_right two_pos (not_lt.mp hi)))]
+  · intro h
+    funext r
+    simp only [letterCode, h, Cslib.BitString.testBit_lsbValue]
+    rw [List.getD_eq_getElem _ _ (by rw [List.length_ofFn]; exact r.isLt), List.getElem_ofFn]
+
+/-- **Reading a letter code**: bits are the code of a letter exactly when the number they write is
+below `letterCount`. -/
+theorem mem_range_letterCode_iff (bits : Fin (letterBits k s b) → Bool) :
+    bits ∈ Set.range (letterCode (k := k) e) ↔
+      Cslib.BitString.lsbValue (List.ofFn bits) < letterCount k s b := by
+  constructor
+  · rintro ⟨l, hl⟩
+    rw [← (letterCode_eq_iff e b l bits).mp hl]
+    exact (letterEquiv e l).isLt
+  · intro h
+    exact ⟨(letterEquiv e).symm ⟨_, h⟩, (letterCode_eq_iff e b _ bits).mpr (by simp)⟩
+
+/-- The letter read from the code `bits` is the decoded letter of their number. -/
+theorem invFun_letterCode {bits : Fin (letterBits k s b) → Bool}
+    (h : Cslib.BitString.lsbValue (List.ofFn bits) < letterCount k s b) :
+    Function.invFun (letterCode (k := k) e) bits =
+      decodeLetter e b (Cslib.BitString.lsbValue (List.ofFn bits)) := by
+  have hmem := (mem_range_letterCode_iff e b bits).mpr h
+  have hinv := Function.invFun_eq hmem
+  rw [letterCode_eq_iff] at hinv
+  rw [← hinv, decodeLetter_letterEquiv]
+
+end Read
+
+/-! ### The tables on numbers -/
+
+section Tables
+
+/-- The letter number read from the table index `j` at the `m` port numbers `base, …,
+base + m - 1` of the port list `P`: its bit `r` is the bit of `j` at the position of port
+`base + r` in `P`. -/
+@[expose] def readNum (m : ℕ) (P : List ℕ) (j base : ℕ) : ℕ :=
+  Cslib.BitString.lsbValue ((List.range m).map fun r => j.testBit (P.idxOf (base + r)))
+
+/-- The first number of the explicit edges of the block edge numbered `n` at the old vertex
+numbered `v`: its source halves when `v` is the interval it leaves, and its target halves
+otherwise. -/
+@[expose] def halfBase (k q m v n : ℕ) : ℕ :=
+  if blockSrcNum k q n = v then m * n else q * (3 * k + 1) * m + m * n
+
+/-- The letter numbers of the block edges read at the old vertex numbered `v` from the table
+index `j` and the ports `P`. -/
+@[expose] def lettersAt (k q m : ℕ) (P : List ℕ) (j v : ℕ) (n : ℕ) : ℕ :=
+  readNum m P j (halfBase k q m v n)
+
+/-- Whether every block edge at the old vertex numbered `v` carries a letter number, read from
+the table index `j` and the ports `P`, below `letterCount`. -/
+@[expose] def validNum (k q s b σ : ℕ) (P : List ℕ) (j v : ℕ) : Bool :=
+  (List.range (q * (3 * k + 1))).all fun n =>
+    !decide (blockSrcNum k q n = v ∨ edgeTargetNum k q σ n = v) ||
+      decide (lettersAt k q (letterBits k s b) P j v n < letterCount k s b)
+
+variable (e : State ≃ Fin s) (b : ℕ) [DecidableEq State] (machine : MultiTapePTM k Bool State)
+  (input : List Bool)
+
+/-- **The table entry on numbers** of the vertex numbered `v` with ports `P` at the table index
+`j`: for an old vertex, its tensor at the letters read from `j` when they are all valid, and zero
+otherwise; for the subdivision vertex of a copy, equality of the bits on its two halves. -/
+@[expose] def tableEntryNum (q σ v : ℕ) (P : List ℕ) (j : ℕ) : ℕ :=
+  if v < q * (3 * k + 2) then
+    if validNum k q s b σ P j v then
+      oldEntryNum e b machine input q σ (lettersAt k q (letterBits k s b) P j v) v
+    else 0
+  else if j.testBit (P.idxOf (v - q * (3 * k + 2))) =
+      j.testBit (P.idxOf (q * (3 * k + 1) * letterBits k s b + (v - q * (3 * k + 2)))) then 1
+    else 0
+
+/-- **The table on numbers** of the vertex numbered `v`: its entries at all indices below
+`2 ^ (number of ports)`. -/
+@[expose] def explicitTableNum (q σ v : ℕ) : List ℕ :=
+  (List.range (2 ^ (explicitPortsNum k q (letterBits k s b) σ v).length)).map
+    (tableEntryNum e b machine input q σ v (explicitPortsNum k q (letterBits k s b) σ v))
+
+/-- **The vertices of the explicit network on numbers**: the ports and the table of every vertex
+number. -/
+@[expose] def explicitVerticesNum (q σ : ℕ) : List (List ℕ × List ℕ) :=
+  (List.range (q * (3 * k + 2) + q * (3 * k + 1) * letterBits k s b)).map fun v =>
+    (explicitPortsNum k q (letterBits k s b) σ v, explicitTableNum e b machine input q σ v)
+
+private theorem idxOf_map_val {n : ℕ} (l : List (Fin n)) (a : Fin n) :
+    (l.map Fin.val).idxOf a.val = l.idxOf a := by
+  induction l with
+  | nil => rfl
+  | cons x l ih =>
+    simp only [List.map_cons, List.idxOf_cons, ih, beq_iff_eq, Fin.val_inj]
+
+private theorem ofFn_eq_map_range {m : ℕ} (f : ℕ → Bool) :
+    List.ofFn (fun r : Fin m => f r) = (List.range m).map f := by
+  rw [List.ofFn_eq_map, ← List.map_coe_finRange_eq_range, List.map_map]
+  rfl
+
+variable [NeZero b]
+
+/-- **The tables of the explicit network on numbers**: the table of every vertex of the
+binarized, subdivided network, with the edges numbered by `explicitEdgeEquiv`, is
+`explicitTableNum` at the number of the vertex. -/
+theorem explicitTable_eq_explicitTableNum (σ : ℕ)
+    (w : (Fin q ⊕ BlockEdge k q) ⊕ BlockEdge k q × Fin (letterBits k s b)) :
+    ((machine.blockNetwork input b (scheduleOfNat k q σ)).binarize
+        (letterCode e)).subdivide.explicitTable (explicitEdgeEquiv k q (letterBits k s b)) w =
+      explicitTableNum e b machine input q σ (explicitVertexEquiv k q (letterBits k s b) w) := by
+  set BN := machine.blockNetwork input b (scheduleOfNat k q σ)
+  set ee := explicitEdgeEquiv k q (letterBits k s b)
+  set ev := explicitVertexEquiv k q (letterBits k s b)
+  set P := explicitPortsNum k q (letterBits k s b) σ (ev w)
+  have hP : ((BN.binarize (letterCode e)).subdivide.explicitPorts ee w).map Fin.val = P :=
+    map_val_explicitPorts machine input b (letterCode e) σ w
+  have hidx : ∀ p, ((BN.binarize (letterCode e)).subdivide.explicitPorts ee w).idxOf (ee p) =
+      P.idxOf (ee p : ℕ) := fun p => by rw [← hP, idxOf_map_val]
+  unfold TensorNetwork.explicitTable explicitTableNum
+  rw [show ((BN.binarize (letterCode e)).subdivide.explicitPorts ee w).length = P.length by
+    rw [← hP, List.length_map]]
+  refine List.map_congr_left fun j _ => ?_
+  simp only [hidx]
+  rcases w with u | ⟨e₀, r⟩
+  · -- An old vertex.
+    have hv : (ev (.inl u) : ℕ) < q * (3 * k + 2) := explicitVertexEquiv_inl k q _ u
+    rw [tableEntryNum, ite_eq_left hv, TensorNetwork.subdivide_tensor_inl]
+    simp only [TensorNetwork.binarize]
+    -- The bits on the copies of an edge, and their number.
+    have hsrc : ∀ e' : BlockEdge k q,
+        BN.src e' = u ↔ blockSrcNum k q (blockEdgeEquiv k q e') = ev (.inl u) := by
+      intro e'
+      rw [blockSrcNum_blockEdgeEquiv (letterBits k s b) e', blockNetwork_src, Fin.val_inj,
+        Equiv.apply_eq_iff_eq]
+      simp only [Sum.inl.injEq]
+    have htgt : ∀ e' : BlockEdge k q,
+        BN.tgt e' = u ↔ edgeTargetNum k q σ (blockEdgeEquiv k q e') = ev (.inl u) := by
+      intro e'
+      rw [edgeTargetNum_blockEdgeEquiv σ (letterBits k s b) e', blockNetwork_tgt, Fin.val_inj,
+        Equiv.apply_eq_iff_eq]
+      simp only [Sum.inl.injEq]
+    have hbits : ∀ e' : BlockEdge k q,
+        Cslib.BitString.lsbValue (List.ofFn (TensorNetwork.bitsOn (fun p =>
+          if BN.src p.1 = u then j.testBit (P.idxOf (ee (.inl p) : ℕ))
+          else j.testBit (P.idxOf (ee (.inr p) : ℕ))) e')) =
+          lettersAt k q (letterBits k s b) P j (ev (.inl u)) (blockEdgeEquiv k q e') := by
+      intro e'
+      simp only [lettersAt, readNum, halfBase, ← hsrc e']
+      rw [← ofFn_eq_map_range]
+      refine congrArg (fun l => Cslib.BitString.lsbValue (List.ofFn l)) (funext fun r => ?_)
+      rw [TensorNetwork.bitsOn_apply]
+      split_ifs
+      · rw [val_explicitEdgeEquiv_inl, Nat.add_comm]
+      · rw [val_explicitEdgeEquiv_inr, Nat.add_left_comm, Nat.add_comm (r : ℕ)]
+    have hinc : ∀ e' : BlockEdge k q, (BN.src e' = u ∨ BN.tgt e' = u) ↔
+        (blockSrcNum k q (blockEdgeEquiv k q e') = ev (.inl u) ∨
+          edgeTargetNum k q σ (blockEdgeEquiv k q e') = ev (.inl u)) := fun e' => by
+      rw [hsrc, htgt]
+    have hall : validNum k q s b σ P j (ev (.inl u)) = true ↔ ∀ e' : BlockEdge k q,
+        (BN.src e' = u ∨ BN.tgt e' = u) →
+          lettersAt k q (letterBits k s b) P j (ev (.inl u)) (blockEdgeEquiv k q e') <
+            letterCount k s b := by
+      rw [validNum, List.all_eq_true]
+      simp only [List.mem_range, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
+        decide_eq_true_eq]
+      constructor
+      · intro h e' he'
+        exact (h _ (blockEdgeEquiv k q e').isLt).resolve_left (not_not.mpr ((hinc e').mp he'))
+      · intro h n hn
+        obtain ⟨e', rfl⟩ : ∃ e', (blockEdgeEquiv k q e' : ℕ) = n :=
+          ⟨(blockEdgeEquiv k q).symm ⟨n, hn⟩, by simp⟩
+        by_cases he' : BN.src e' = u ∨ BN.tgt e' = u
+        · exact Or.inr (h e' he')
+        · exact Or.inl (fun h' => he' ((hinc e').mpr h'))
+    split_ifs with h1 h2 h2
+    · rw [← blockNetwork_tensor_decodeLetter]
+      refine BN.tensor_congr _ _ _ fun e' he' => ?_
+      have hlt := (mem_range_letterCode_iff e b _).mp (h1 e' he')
+      rw [invFun_letterCode e b hlt]
+      exact congrArg (decodeLetter e b) (hbits e')
+    · exact absurd (hall.mpr fun e' he' =>
+        (hbits e').symm.trans_lt ((mem_range_letterCode_iff e b _).mp (h1 e' he'))) h2
+    · exact absurd (fun e' he' => (mem_range_letterCode_iff e b _).mpr
+        ((hbits e').trans_lt (hall.mp h2 e' he'))) h1
+    · rfl
+  · -- A subdivision vertex.
+    have hv : q * (3 * k + 2) ≤ (ev (.inr (e₀, r)) : ℕ) := le_explicitVertexEquiv_inr k q _ _
+    have hc : (ev (.inr (e₀, r)) : ℕ) - q * (3 * k + 2) =
+        r + letterBits k s b * blockEdgeEquiv k q e₀ := by
+      rw [val_explicitVertexEquiv_inr]
+      omega
+    rw [tableEntryNum, ite_eq_right (by omega), TensorNetwork.subdivide_tensor_inr, hc,
+      val_explicitEdgeEquiv_inl, val_explicitEdgeEquiv_inr]
+
+/-- **The explicit block-counting network on numbers**: `2 q (3 k + 1) m` edges and the vertices
+`explicitVerticesNum`. -/
+@[expose] def explicitNetworkNum (q σ : ℕ) : ExplicitTensorNetwork ℕ where
+  numEdges := 2 * (q * (3 * k + 1) * letterBits k s b)
+  vertices := explicitVerticesNum e b machine input q σ
+
+/-- **The explicit block-counting network is computed on numbers**: for the schedule of `σ`,
+`explicitBlockNetwork` is `explicitNetworkNum`. -/
+theorem explicitBlockNetwork_eq_explicitNetworkNum (σ : ℕ) :
+    machine.explicitBlockNetwork input b (scheduleOfNat k q σ) e =
+      explicitNetworkNum e b machine input q σ := by
+  have hv : (machine.explicitBlockNetwork input b (scheduleOfNat k q σ) e).vertices =
+      explicitVerticesNum e b machine input q σ := by
+    rw [explicitBlockNetwork, TensorNetwork.toExplicit, explicitVerticesNum,
+      ← List.map_coe_finRange_eq_range, List.map_map, List.ofFn_eq_map]
+    refine List.map_congr_left fun v _ => ?_
+    simp only [Function.comp_apply]
+    rw [map_val_explicitPorts, explicitTable_eq_explicitTableNum, Equiv.apply_symm_apply]
+  cases h : machine.explicitBlockNetwork input b (scheduleOfNat k q σ) e with
+  | mk n vs =>
+    rw [h] at hv
+    have hn := numEdges_explicitBlockNetwork machine input b (scheduleOfNat k q σ) e
+    rw [h] at hn
+    simp only at hv hn
+    rw [explicitNetworkNum, hv, hn]
+
+end Tables
+
+/-! ### Port counts -/
+
+section PortCounts
+
+/-- Every explicit edge starts at an old vertex. -/
+theorem explicitSrcNum_lt {m σ j : ℕ} (hj : j < 2 * (q * (3 * k + 1) * m)) :
+    explicitSrcNum k q m σ j < q * (3 * k + 2) := by
+  have hm : 0 < m := by
+    rcases Nat.eq_zero_or_pos m with rfl | hm
+    · simp at hj
+    · exact hm
+  unfold explicitSrcNum
+  split_ifs with hlt
+  · have hn : j / m < q * (3 * k + 1) := (Nat.div_lt_iff_lt_mul hm).mpr hlt
+    unfold blockSrcNum
+    split_ifs with hq
+    · nlinarith
+    · rcases Nat.eq_zero_or_pos k with rfl | hk
+      · omega
+      · have : (j / m - q) / (k * 3) < q := by
+          rw [Nat.div_lt_iff_lt_mul (by omega)]
+          have : q * (3 * k + 1) = q + q * (k * 3) := by ring
+          omega
+        nlinarith
+  · have hn : (j - q * (3 * k + 1) * m) / m < q * (3 * k + 1) :=
+      (Nat.div_lt_iff_lt_mul hm).mpr (by omega)
+    set n := (j - q * (3 * k + 1) * m) / m
+    unfold edgeTargetNum
+    split_ifs with h1 h2
+    · nlinarith
+    · nlinarith
+    · cases hf : firstAfterNum k q σ ((n - q) % (k * 3) / 3 + 1) ((n - q) / (k * 3)) ((n - q) % 3)
+        with
+      | none => simp only [Option.getD_none]; nlinarith
+      | some i' =>
+        have hmem := List.mem_of_find?_eq_some hf
+        rw [List.mem_range] at hmem
+        simp only [Option.getD_some]
+        nlinarith
+
+/-- Every explicit edge ends at a vertex. -/
+theorem explicitTgtNum_lt {m j : ℕ} (hj : j < 2 * (q * (3 * k + 1) * m)) :
+    explicitTgtNum k q m j < q * (3 * k + 2) + q * (3 * k + 1) * m := by
+  unfold explicitTgtNum
+  split_ifs <;> omega
+
+/-- A number past the vertices has no ports. -/
+theorem explicitPortsNum_eq_nil {m σ v : ℕ}
+    (hv : q * (3 * k + 2) + q * (3 * k + 1) * m ≤ v) : explicitPortsNum k q m σ v = [] := by
+  rw [explicitPortsNum, List.filter_eq_nil_iff]
+  intro j hj
+  rw [List.mem_range] at hj
+  have h1 := explicitSrcNum_lt (σ := σ) hj
+  have h2 := explicitTgtNum_lt hj
+  simp only [decide_eq_true_eq, not_or]
+  omega
+
+/-- **The degree bound on numbers**: every vertex number has at most
+`2 (3 k + 1) (letterBits k s b)` ports. -/
+theorem length_explicitPortsNum_le {State : Type} (machine : MultiTapePTM k Bool State)
+    (b : ℕ) [NeZero b] (e : State ≃ Fin s) (σ v : ℕ) :
+    (explicitPortsNum k q (letterBits k s b) σ v).length ≤ 2 * (3 * k + 1) * letterBits k s b := by
+  by_cases hv : v < q * (3 * k + 2) + q * (3 * k + 1) * letterBits k s b
+  · have hmem : explicitPortsNum k q (letterBits k s b) σ v ∈
+        (machine.explicitBlockNetwork [] b (scheduleOfNat k q σ) e).vertices.map Prod.fst := by
+      rw [map_fst_vertices_explicitBlockNetwork]
+      exact List.mem_map_of_mem (List.mem_range.mpr hv)
+    obtain ⟨p, hp, hpv⟩ := List.mem_map.mp hmem
+    rw [← hpv]
+    exact ((machine.explicitBlockNetwork [] b (scheduleOfNat k q σ) e).length_le_maxDegree hp).trans
+      (maxDegree_explicitBlockNetwork_le ..)
+  · rw [explicitPortsNum_eq_nil (not_lt.mp hv)]
+    exact Nat.zero_le _
+
+end PortCounts
+
+end Turing.MultiTapePTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean
new file mode 100644
index 0000000000..cb04f090b9
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean
@@ -0,0 +1,474 @@
+/-
+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.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.Table
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.GraphPolyTime
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+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.Nat.Div
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Fin
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPower
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePiPrimitives
+
+/-!
+# The tables of an explicit block-counting network in polynomial time
+
+The explicit block-counting network on numbers (`Turing.MultiTapePTM.explicitNetworkNum`) is
+computable in polynomial time from the input, the block length and the number of intervals in
+unary, and the schedule number in binary, provided that `2 ^ b` is bounded by a computed unary
+number. Its tables have `2 ^ (number of ports)` entries, at most `(2 ^ b) ^ (2 (3 k + 1) (s + k +
+4))`, and each entry decodes letters by arithmetic and evaluates an interval count
+(`Turing.MultiTapePTM.computableInPolyTime_localIntervalCount`).
+
+## Main results
+
+* `Turing.MultiTapePTM.computableInPolyTime_decodeControlData`,
+  `Turing.MultiTapePTM.computableInPolyTime_contentsCellNum`: decoding letters.
+* `Turing.MultiTapePTM.computableInPolyTime_intervalEntryNum`: the tensor of an interval on
+  numbers.
+* `Turing.MultiTapePTM.computableInPolyTime_explicitNetworkNum`: the explicit network on numbers,
+  as its number of edges in unary and its vertices, with ports and table entries in binary.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM
+
+open MultiTapeTM ComputableInPolyTime MultiTapeNTM.ChoiceTable
+
+variable {k s : ℕ} {State : Type} {α : Type} {inp : α ↪ List Bool}
+
+/-! ### Small numbers and digits -/
+
+/-- A binary number reduced modulo `3`, as an element of `Fin 3`. -/
+private theorem fin3 {v : α → ℕ} (hv : ComputableInPolyTime v inp encNat) :
+    ComputableInPolyTime (fun a => (⟨v a % 3, Nat.mod_lt _ (by norm_num)⟩ : Fin 3)) inp
+      (encFinite (Fin 3)) := by
+  have hu : ComputableInPolyTime (fun a => v a % 3) inp encUnary :=
+    binary_to_unary_bounded (binary_mod.comp (hv.prod (const 3))) (const 2) fun a => by omega
+  have h := (unary_finMod (by norm_num : 0 < 3) (encFinite (Fin 3))).comp hu
+  simpa only [Function.comp_def, Nat.mod_mod] using h
+
+/-- The number of control records, in binary. -/
+private theorem controlCount' {b : α → ℕ} (hb : ComputableInPolyTime b inp encUnary) :
+    ComputableInPolyTime (fun a => controlCount k s (b a)) inp encNat := by
+  unfold controlCount
+  exact binary_mul' (const _) (binary_mul' (binary_pow' (unary_to_binary.comp hb) (const _))
+    (const 3))
+
+/-- The number of letters, in binary. -/
+private theorem letterCount' {b : α → ℕ} (hb : ComputableInPolyTime b inp encUnary) :
+    ComputableInPolyTime (fun a => letterCount k s (b a)) inp encNat := by
+  unfold letterCount
+  exact binary_add.comp ((controlCount' hb).prod (binary_pow' (const 3) hb))
+
+/-! ### Decoding letters -/
+
+/-- **Cells of block contents are polynomial-time.** -/
+theorem computableInPolyTime_contentsCellNum {b n r : α → ℕ}
+    (hb : ComputableInPolyTime b inp encUnary) (hn : ComputableInPolyTime n inp encNat)
+    (hr : ComputableInPolyTime r inp encUnary) :
+    ComputableInPolyTime (fun a => contentsCellNum k s (b a) (n a) (r a)) inp
+      (encOption encBool) := by
+  have hC := controlCount' (k := k) (s := s) hb
+  unfold contentsCellNum
+  refine ite_decide (binary_lt' hn hC) (const none) ?_
+  exact (of_finite (encIn := encFinite (Fin 3)) (encOut := encOption encBool)
+    cellEquiv.symm).comp (fin3 (binary_div.comp ((binary_sub' hn hC).prod
+      (binary_pow' (const 3) hr))))
+
+variable [Finite State]
+
+/-- **Control records of numbers are polynomial-time**, on plain data. -/
+theorem computableInPolyTime_decodeControlData (e : State ≃ Fin s) {b n : α → ℕ}
+    (hb : ComputableInPolyTime b inp encUnary) (hb0 : ∀ a, 0 < b a)
+    (hn : ComputableInPolyTime n inp encNat) :
+    ComputableInPolyTime (fun a => decodeControlData (k := k) e (b a) (n a)) inp
+      encControlData := by
+  have hbB : ComputableInPolyTime b inp encNat := unary_to_binary.comp hb
+  have hD : ComputableInPolyTime (fun a => b a ^ (k + 1) * 3) inp encNat :=
+    binary_mul' (binary_pow' hbB (const _)) (const 3)
+  have hrem : ComputableInPolyTime (fun a => n a % (b a ^ (k + 1) * 3)) inp encNat :=
+    binary_mod.comp (hn.prod hD)
+  have hstate : ComputableInPolyTime (fun a => stateOfFin e
+      ⟨min s (n a / (b a ^ (k + 1) * 3)) % (s + 1), Nat.mod_lt _ (by omega)⟩) inp
+      (encFinite (Option State)) :=
+    (of_finite (encIn := encFinite (Fin (s + 1))) (encOut := encFinite (Option State))
+      (stateOfFin e)).comp ((unary_finMod (Nat.succ_pos s) (encFinite (Fin (s + 1)))).comp
+        (binary_min_unary' (const s) (binary_div.comp (hn.prod hD))))
+  have hoff : ComputableInPolyTime (fun a (head : Option (Fin k)) =>
+      n a % (b a ^ (k + 1) * 3) / 3 / b a ^ ((finSuccEquiv k).symm head : ℕ) % b a) inp
+      (encPi encUnary) := by
+    refine pi fun head => binary_to_unary_bounded ?_ hb fun a => (Nat.mod_lt _ (hb0 a)).le
+    exact binary_mod.comp ((binary_div.comp ((binary_div.comp (hrem.prod (const 3))).prod
+      (binary_pow' hbB (const _)))).prod hbB)
+  have htrack : ComputableInPolyTime (fun a => OutputTrack.equivFin.symm
+      ⟨n a % (b a ^ (k + 1) * 3) % 3, Nat.mod_lt _ (by norm_num)⟩) inp
+      (encFinite OutputTrack) :=
+    (of_finite (encIn := encFinite (Fin 3)) (encOut := encFinite OutputTrack)
+      OutputTrack.equivFin.symm).comp (fin3 hrem)
+  exact ControlData.computableInPolyTime_mk hstate hoff htrack
+
+/-- Entering control records from letter numbers are polynomial-time. -/
+theorem computableInPolyTime_controlDataOfNum (e : State ≃ Fin s) {b n : α → ℕ}
+    (hb : ComputableInPolyTime b inp encUnary) (hb0 : ∀ a, 0 < b a)
+    (hn : ComputableInPolyTime n inp encNat) :
+    ComputableInPolyTime (fun a => controlDataOfNum (k := k) e (b a) (n a)) inp
+      encControlData := by
+  unfold controlDataOfNum
+  exact ite_decide (binary_lt' hn (controlCount' hb))
+    (computableInPolyTime_decodeControlData e hb hb0 hn) (const _)
+
+/-! ### Block indices, movements and the entering window -/
+
+/-- Block indices as digit counts are polynomial-time. -/
+theorem computableInPolyTime_blockIndexNum {σ i : α → ℕ}
+    (hσ : ComputableInPolyTime σ inp encNat) (hi : ComputableInPolyTime i inp encUnary) :
+    ComputableInPolyTime (fun a => blockIndexNum k (σ a) (i a)) inp (encPi encIntBin) := by
+  refine pi fun head => ?_
+  have hcount := fun δ => computableInPolyTime_digitCount (k := k) hσ
+    (const ((finSuccEquiv k).symm head : ℕ)) (const δ) hi
+  exact intBin_sub.comp ((intBin_natCast.comp (unary_to_binary.comp (hcount 2))).prod
+    (intBin_natCast.comp (unary_to_binary.comp (hcount 0))))
+
+/-- Block movements of a schedule number are polynomial-time. -/
+theorem computableInPolyTime_blockMoveNum {σ i : α → ℕ}
+    (hσ : ComputableInPolyTime σ inp encNat) (hi : ComputableInPolyTime i inp encUnary) :
+    ComputableInPolyTime (fun a => blockMoveNum k (σ a) (i a)) inp
+      (encFinite (Option (Fin k) → SignType)) := by
+  have hpi : ComputableInPolyTime (fun a => blockMoveNum k (σ a) (i a)) inp
+      (encPi (encFinite SignType)) := by
+    refine pi fun head => ?_
+    have hpos : ComputableInPolyTime (fun a => ((finSuccEquiv k).symm head : ℕ) + (k + 1) * i a)
+        inp encUnary := unary_add' (const _) (unary_mul' (const _) hi)
+    exact (of_finite (encIn := encFinite (Fin 3)) (encOut := encFinite SignType)
+      signEquiv.symm).comp (fin3 (binary_div.comp (hσ.prod (binary_pow' (const 3) hpos))))
+  exact (of_finite (encIn := encPi (encFinite SignType))
+    (encOut := encFinite (Option (Fin k) → SignType)) id).comp hpi
+
+/-- Previous appearances on numbers are polynomial-time. -/
+theorem computableInPolyTime_lastBeforeNum {σ c i δ : α → ℕ}
+    (hσ : ComputableInPolyTime σ inp encNat) (hc : ComputableInPolyTime c inp encUnary)
+    (hi : ComputableInPolyTime i inp encUnary) (hδ : ComputableInPolyTime δ inp encUnary) :
+    ComputableInPolyTime (fun a => lastBeforeNum k (σ a) (c a) (i a) (δ a)) inp
+      (encOption encUnary) := by
+  have heq : ∀ a, lastBeforeNum k (σ a) (c a) (i a) (δ a) =
+      ((List.range (i a)).find? fun j => inWindowNum k (σ a) (c a) (i a) (δ a) (i a - 1 - j)).elim
+        none fun j => some (i a - 1 - j) := fun a => by
+    unfold lastBeforeNum
+    cases (List.range (i a)).find? _ <;> rfl
+  simp only [heq]
+  have hi1 : ComputableInPolyTime (fun p : α × ℕ => i p.1 - 1 - p.2) (encPair inp encUnary)
+      encUnary := unary_sub' (unary_sub' (hi.comp (fst _ _)) (const 1)) (snd _ _)
+  refine optionElimWithInput (findWithInput (range.comp hi) ?_) (const none)
+    ((optionSome encUnary).comp hi1)
+  exact computableInPolyTime_inWindowNum (hσ.comp (fst _ _)) (hc.comp (fst _ _))
+    (hi.comp (fst _ _)) (hδ.comp (fst _ _)) hi1
+
+/-- Window entries on numbers are polynomial-time. -/
+theorem computableInPolyTime_portOfNum {σ c i i' δ : α → ℕ}
+    (hσ : ComputableInPolyTime σ inp encNat) (hc : ComputableInPolyTime c inp encUnary)
+    (hi : ComputableInPolyTime i inp encUnary) (hi' : ComputableInPolyTime i' inp encUnary)
+    (hδ : ComputableInPolyTime δ inp encUnary) :
+    ComputableInPolyTime (fun a => portOfNum k (σ a) (c a) (i a) (i' a) (δ a)) inp encUnary := by
+  have hcount := fun {j : α → ℕ} (hj : ComputableInPolyTime j inp encUnary) (d : ℕ) =>
+    computableInPolyTime_digitCount (k := k) hσ hc (const d) hj
+  unfold portOfNum
+  exact unary_mod.comp ((unary_sub' (unary_add' (unary_add' (hcount hi 2) (hcount hi' 0)) hδ)
+    (unary_add' (hcount hi 0) (hcount hi' 2))).prod (const 3))
+
+/-! ### The tensor of an interval -/
+
+/-- A computed unary bound on `2 ^ b` gives the budget of the interval counts. -/
+private theorem budget_of_cap {b cap : α → ℕ} (hcap : ComputableInPolyTime cap inp encUnary)
+    (h2b : ∀ a, 2 ^ b a ≤ cap a) :
+    ∃ size : ℕ → ℕ, Cslib.PolynomiallyBounded size ∧
+      ∀ a, 2 ^ b a * (2 * b a + 1) ≤ size (inp a).length := by
+  obtain ⟨bound, hbound, hle⟩ := polyBounded hcap
+  refine ⟨fun n => bound n * (2 * bound n + 1), by fun_prop, fun a => ?_⟩
+  have h1 : 2 ^ b a ≤ bound (inp a).length := (h2b a).trans (hle a)
+  have h2 : b a < 2 ^ b a := Nat.lt_two_pow_self
+  exact Nat.mul_le_mul h1 (by omega)
+
+/-- A letter number at a computed edge number. -/
+private theorem letter_comp {β : Type} {encβ : β ↪ List Bool} {L : α → ℕ → ℕ}
+    (hL : ComputableInPolyTime (fun p : α × ℕ => L p.1 p.2) (encPair inp encUnary) encNat)
+    {g : β → α} {n : β → ℕ} (hg : ComputableInPolyTime g encβ inp)
+    (hn : ComputableInPolyTime n encβ encUnary) :
+    ComputableInPolyTime (fun c => L (g c) (n c)) encβ encNat :=
+  hL.comp (hg.prod hn)
+
+section Interval
+
+variable [DecidableEq State] (e : State ≃ Fin s) (machine : MultiTapePTM k Bool State)
+  {x : α → List Bool} {b q σ cap : α → ℕ} {L : α → ℕ → ℕ}
+
+/-- The cells of a window entering an interval are polynomial-time. -/
+theorem computableInPolyTime_inCellsNum (h : ℕ) {i : α → ℕ}
+    (hb : ComputableInPolyTime b inp encUnary) (hq : ComputableInPolyTime q inp encUnary)
+    (hσ : ComputableInPolyTime σ inp encNat)
+    (hL : ComputableInPolyTime (fun p : α × ℕ => L p.1 p.2) (encPair inp encUnary) encNat)
+    (hi : ComputableInPolyTime i inp encUnary) :
+    ComputableInPolyTime (fun a => inCellsNum k (q a) s (b a) (σ a) (L a) (i a) h) inp
+      (encList (encOption encBool)) := by
+  unfold inCellsNum
+  have hcb : ComputableInPolyTime (fun p : α × ℕ => p.2 / b p.1) (encPair inp encUnary)
+      encUnary := unary_div.comp ((snd _ _).prod (hb.comp (fst _ _)))
+  refine mapWithInput (range.comp (unary_mul' (const 3) hb))
+    (optionElimWithInput (computableInPolyTime_lastBeforeNum (hσ.comp (fst _ _)) (const _)
+      (hi.comp (fst _ _)) hcb) (const none) ?_)
+  have ha : ComputableInPolyTime (fun r : (α × ℕ) × ℕ => r.1.1)
+      (encPair (encPair inp encUnary) encUnary) inp := (fst _ _).comp (fst _ _)
+  have hc : ComputableInPolyTime (fun r : (α × ℕ) × ℕ => r.1.2)
+      (encPair (encPair inp encUnary) encUnary) encUnary := (snd _ _).comp (fst _ _)
+  have hi' : ComputableInPolyTime (fun r : (α × ℕ) × ℕ => r.2)
+      (encPair (encPair inp encUnary) encUnary) encUnary := snd _ _
+  refine computableInPolyTime_contentsCellNum (hb.comp ha) (letter_comp hL ha ?_)
+    (unary_mod.comp (hc.prod (hb.comp ha)))
+  exact unary_add' (hq.comp ha) (unary_add' (unary_add' (computableInPolyTime_portOfNum
+    (hσ.comp ha) (const _) (hi.comp ha) hi' (unary_div.comp (hc.prod (hb.comp ha)))) (const _))
+    (unary_mul' (const _) hi'))
+
+/-- The cells of a window leaving an interval are polynomial-time. -/
+theorem computableInPolyTime_outCellsNum (h : ℕ) {i : α → ℕ}
+    (hb : ComputableInPolyTime b inp encUnary) (hq : ComputableInPolyTime q inp encUnary)
+    (hL : ComputableInPolyTime (fun p : α × ℕ => L p.1 p.2) (encPair inp encUnary) encNat)
+    (hi : ComputableInPolyTime i inp encUnary) :
+    ComputableInPolyTime (fun a => outCellsNum k (q a) s (b a) (L a) (i a) h) inp
+      (encList (encOption encBool)) := by
+  unfold outCellsNum
+  have ha : ComputableInPolyTime (fun p : α × ℕ => p.1) (encPair inp encUnary) inp := fst _ _
+  have hc : ComputableInPolyTime (fun p : α × ℕ => p.2) (encPair inp encUnary) encUnary :=
+    snd _ _
+  refine mapWithInput (range.comp (unary_mul' (const 3) hb))
+    (computableInPolyTime_contentsCellNum (hb.comp ha) (letter_comp hL ha ?_)
+      (unary_mod.comp (hc.prod (hb.comp ha))))
+  exact unary_add' (hq.comp ha) (unary_add' (unary_add' (unary_div.comp (hc.prod (hb.comp ha)))
+    (const _)) (unary_mul' (const _) (hi.comp ha)))
+
+/-- **The tensor of an interval on numbers is polynomial-time**, from the letter numbers of the
+edges, when `2 ^ b` is bounded by a computed unary number. -/
+theorem computableInPolyTime_intervalEntryNum {i : α → ℕ}
+    (hx : ComputableInPolyTime x inp encBits) (hb : ComputableInPolyTime b inp encUnary)
+    (hb0 : ∀ a, 0 < b a) (hq : ComputableInPolyTime q inp encUnary)
+    (hσ : ComputableInPolyTime σ inp encNat) (hcap : ComputableInPolyTime cap inp encUnary)
+    (h2b : ∀ a, 2 ^ b a ≤ cap a)
+    (hL : ComputableInPolyTime (fun p : α × ℕ => L p.1 p.2) (encPair inp encUnary) encNat)
+    (hi : ComputableInPolyTime i inp encUnary) :
+    ComputableInPolyTime (fun a => intervalEntryNum e (b a) machine (x a) (q a) (σ a) (L a) (i a))
+      inp encUnary := by
+  obtain ⟨size, hsize, hbudget⟩ := budget_of_cap hcap h2b
+  have hC := controlCount' (k := k) (s := s) hb
+  have hLat : ∀ {n : α → ℕ}, ComputableInPolyTime n inp encUnary →
+      ComputableInPolyTime (fun a => L a (n a)) inp encNat := fun hn => letter_comp hL id' hn
+  have hcond : ∀ a, decide (L a (i a) < controlCount k s (b a) ∧ ∀ h : Fin k, ∀ δ : Fin 3,
+      ¬ L a (q a + (δ + 3 * h + k * 3 * i a)) < controlCount k s (b a)) =
+      (decide (L a (i a) < controlCount k s (b a)) && (List.finRange k).all fun h =>
+        (List.finRange 3).all fun δ =>
+          !decide (L a (q a + (δ + 3 * h + k * 3 * i a)) < controlCount k s (b a))) := by
+    intro a
+    rw [Bool.eq_iff_iff]
+    simp [List.all_eq_true]
+  have hcIn : ComputableInPolyTime
+      (fun a => (inControlNum e (b a) machine.initial (L a) (i a) : ControlData k State)) inp
+      encControlData := by
+    unfold inControlNum
+    exact ite_decide (decide_eq' hi (const 0)) (const _)
+      (computableInPolyTime_controlDataOfNum e hb hb0 (hLat (unary_sub' hi (const 1))))
+  unfold intervalEntryNum
+  refine ite_decide ?_ ?_ (const 0)
+  · simp only [hcond]
+    refine bool_and' (binary_lt' (hLat hi) hC) (allConst _ fun h _ => allConst _ fun δ _ => ?_)
+    exact bool_not.comp (binary_lt' (hLat (unary_add' hq (unary_add' (const _)
+      (unary_mul' (const _) hi)))) hC)
+  · have hd := IntervalData.computableInPolyTime_mk hx hb
+      (computableInPolyTime_blockIndexNum hσ hi) (computableInPolyTime_blockMoveNum hσ hi) hcIn
+      (pi fun h : Fin k => computableInPolyTime_inCellsNum (k := k) (s := s) h.val hb hq hσ hL hi)
+      (computableInPolyTime_decodeControlData e hb hb0 (hLat hi))
+      (pi fun h : Fin k => computableInPolyTime_outCellsNum (k := k) (s := s) h.val hb hq hL hi)
+    have hcount := computableInPolyTime_localIntervalCount machine hd hsize hbudget
+    simpa only [IntervalData.count] using hcount
+
+end Interval
+
+/-! ### Reading letters and the tables -/
+
+private theorem lsbValue_eq_ofBits : ∀ w : List Bool, Cslib.BitString.lsbValue w = ofBits w
+  | [] => rfl
+  | c :: w => by
+    rw [Cslib.BitString.lsbValue, lsbValue_eq_ofBits w]
+    simp only [ofBits, List.foldr_cons, Nat.bit_val]
+    ring
+
+/-- **Letter numbers read from table indices are polynomial-time.** -/
+theorem computableInPolyTime_readNum {m j base : α → ℕ} {P : α → List ℕ}
+    (hm : ComputableInPolyTime m inp encUnary) (hP : ComputableInPolyTime P inp (encList encNat))
+    (hj : ComputableInPolyTime j inp encUnary) (hbase : ComputableInPolyTime base inp encUnary) :
+    ComputableInPolyTime (fun a => readNum (m a) (P a) (j a) (base a)) inp encNat := by
+  have hlist : ComputableInPolyTime
+      (fun a => (List.range (m a)).map fun r => (j a).testBit ((P a).idxOf (base a + r))) inp
+      (encList encBool) :=
+    mapWithInput (range.comp hm) (unary_testBit' (hj.comp (fst _ _))
+      (idxOfWithInput (hP.comp (fst _ _))
+        (unary_to_binary.comp (unary_add' (hbase.comp (fst _ _)) (snd _ _)))))
+  have hbits := (bits_encList_polyTime encBool).2.comp hlist
+  have hnum := (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.bitsToNat).comp hbits
+  simpa only [readNum, lsbValue_eq_ofBits, Function.comp_def] using hnum
+
+private theorem blockSrcNum' {q n : α → ℕ} (hq : ComputableInPolyTime q inp encUnary)
+    (hn : ComputableInPolyTime n inp encUnary) :
+    ComputableInPolyTime (fun a => blockSrcNum k (q a) (n a)) inp encUnary := by
+  unfold blockSrcNum
+  exact ite_decide (unary_lt' hn hq) hn (unary_div.comp ((unary_sub' hn hq).prod (const _)))
+
+/-- The letter numbers read at an old vertex are polynomial-time, at a computed edge number. -/
+theorem computableInPolyTime_lettersAt {q m v j : α → ℕ} {P : α → List ℕ}
+    (hq : ComputableInPolyTime q inp encUnary) (hm : ComputableInPolyTime m inp encUnary)
+    (hP : ComputableInPolyTime P inp (encList encNat)) (hj : ComputableInPolyTime j inp encUnary)
+    (hv : ComputableInPolyTime v inp encUnary) :
+    ComputableInPolyTime (fun p : α × ℕ => lettersAt k (q p.1) (m p.1) (P p.1) (j p.1) (v p.1) p.2)
+      (encPair inp encUnary) encNat := by
+  have ha : ComputableInPolyTime (fun p : α × ℕ => p.1) (encPair inp encUnary) inp := fst _ _
+  have hn : ComputableInPolyTime (fun p : α × ℕ => p.2) (encPair inp encUnary) encUnary :=
+    snd _ _
+  unfold lettersAt halfBase
+  refine computableInPolyTime_readNum (hm.comp ha) (hP.comp ha) (hj.comp ha)
+    (ite_decide (decide_eq' (blockSrcNum' (hq.comp ha) hn) (hv.comp ha))
+      (unary_mul' (hm.comp ha) hn) ?_)
+  exact unary_add' (unary_mul' (unary_mul' (hq.comp ha) (const _)) (hm.comp ha))
+    (unary_mul' (hm.comp ha) hn)
+
+section Tables
+
+variable [DecidableEq State] (e : State ≃ Fin s) (machine : MultiTapePTM k Bool State)
+  {x : α → List Bool} {b q σ cap : α → ℕ}
+
+/-- **Table entries on numbers are polynomial-time.** -/
+theorem computableInPolyTime_tableEntryNum {v j : α → ℕ} {P : α → List ℕ}
+    (hx : ComputableInPolyTime x inp encBits) (hb : ComputableInPolyTime b inp encUnary)
+    (hb0 : ∀ a, 0 < b a) (hq : ComputableInPolyTime q inp encUnary)
+    (hσ : ComputableInPolyTime σ inp encNat) (hcap : ComputableInPolyTime cap inp encUnary)
+    (h2b : ∀ a, 2 ^ b a ≤ cap a) (hv : ComputableInPolyTime v inp encUnary)
+    (hP : ComputableInPolyTime P inp (encList encNat)) (hj : ComputableInPolyTime j inp encUnary) :
+    ComputableInPolyTime
+      (fun a => tableEntryNum e (b a) machine (x a) (q a) (σ a) (v a) (P a) (j a)) inp encNat := by
+  have hm : ComputableInPolyTime (fun a => letterBits k s (b a)) inp encUnary := by
+    unfold letterBits
+    exact unary_mul' (const _) hb
+  have hL := computableInPolyTime_lettersAt (k := k) hq hm hP hj hv
+  have hR : ComputableInPolyTime (fun a => q a * (3 * k + 2)) inp encUnary :=
+    unary_mul' hq (const _)
+  have hE : ComputableInPolyTime (fun a => q a * (3 * k + 1)) inp encUnary :=
+    unary_mul' hq (const _)
+  have hC := controlCount' (k := k) (s := s) hb
+  have hD : ComputableInPolyTime (fun a => b a ^ (k + 1) * 3) inp encNat :=
+    binary_mul' (binary_pow' (unary_to_binary.comp hb) (const _)) (const 3)
+  -- Validity of the letters at an old vertex.
+  have hvalid : ComputableInPolyTime (fun a => validNum k (q a) s (b a) (σ a) (P a) (j a) (v a))
+      inp encBool := by
+    unfold validNum
+    have ha : ComputableInPolyTime (fun p : α × ℕ => p.1) (encPair inp encUnary) inp := fst _ _
+    have hn : ComputableInPolyTime (fun p : α × ℕ => p.2) (encPair inp encUnary) encUnary :=
+      snd _ _
+    refine allWithInput (range.comp hE) (bool_or.comp ((bool_not.comp ?_).prod ?_))
+    · exact decide_or (decide_eq' (blockSrcNum' (hq.comp ha) hn) (hv.comp ha))
+        (decide_eq' (computableInPolyTime_edgeTargetNum (hq.comp ha) (hσ.comp ha) hn) (hv.comp ha))
+    · exact binary_lt' hL ((letterCount' hb).comp ha)
+  -- The tensor of an old vertex.
+  have hold : ComputableInPolyTime (fun a => oldEntryNum e (b a) machine (x a) (q a) (σ a)
+      (lettersAt k (q a) (letterBits k s (b a)) (P a) (j a) (v a)) (v a)) inp encNat := by
+    unfold oldEntryNum
+    refine ite_decide (unary_lt' hv hq) (unary_to_binary.comp
+      (computableInPolyTime_intervalEntryNum e machine hx hb hb0 hq hσ hcap h2b hL hv))
+      (ite_decide (decide_eq' (unary_add' (unary_sub' hv hq) (const 1)) hq) ?_ (const 1))
+    unfold acceptNum
+    have hn := letter_comp
+      (L := fun a => lettersAt k (q a) (letterBits k s (b a)) (P a) (j a) (v a)) hL id'
+      (unary_sub' hv hq)
+    exact ite_decide (decide_and (binary_lt' hn hC) (decide_eq' (binary_mod.comp
+      ((binary_mod.comp (hn.prod hD)).prod (const 3))) (const 1))) (const 1) (const 0)
+  unfold tableEntryNum
+  refine ite_decide (unary_lt' hv hR) (ite hvalid hold (const 0)) ?_
+  have hc : ComputableInPolyTime (fun a => v a - q a * (3 * k + 2)) inp encUnary :=
+    unary_sub' hv hR
+  refine ite_decide (decide_eq' (unary_testBit' hj (idxOfWithInput hP (unary_to_binary.comp hc)))
+    (unary_testBit' hj (idxOfWithInput hP (unary_to_binary.comp (unary_add'
+      (unary_mul' hE hm) hc))))) (const 1) (const 0)
+
+/-- **Tables on numbers are polynomial-time.** -/
+theorem computableInPolyTime_explicitTableNum {v : α → ℕ}
+    (hx : ComputableInPolyTime x inp encBits) (hb : ComputableInPolyTime b inp encUnary)
+    (hb0 : ∀ a, 0 < b a) (hq : ComputableInPolyTime q inp encUnary)
+    (hσ : ComputableInPolyTime σ inp encNat) (hcap : ComputableInPolyTime cap inp encUnary)
+    (h2b : ∀ a, 2 ^ b a ≤ cap a) (hv : ComputableInPolyTime v inp encUnary) :
+    ComputableInPolyTime (fun a => explicitTableNum e (b a) machine (x a) (q a) (σ a) (v a)) inp
+      (encList encNat) := by
+  have hm : ComputableInPolyTime (fun a => letterBits k s (b a)) inp encUnary := by
+    unfold letterBits
+    exact unary_mul' (const _) hb
+  have hP := computableInPolyTime_explicitPortsNum (k := k) hq hm hσ hv
+  have hlen : ComputableInPolyTime
+      (fun a => 2 ^ (explicitPortsNum k (q a) (letterBits k s (b a)) (σ a) (v a)).length) inp
+      encUnary := by
+    refine binary_to_unary_bounded (binary_two_pow.comp ((length_list encNat).comp hP))
+      ((unary_pow (2 * (3 * k + 1) * (s + k + 4))).comp hcap) fun a => ?_
+    have : NeZero (b a) := ⟨(hb0 a).ne'⟩
+    have hdeg := length_explicitPortsNum_le (q := q a) machine (b a) e (σ a) (v a)
+    calc 2 ^ (explicitPortsNum k (q a) (letterBits k s (b a)) (σ a) (v a)).length
+        ≤ 2 ^ (b a * (2 * (3 * k + 1) * (s + k + 4))) := by
+          refine Nat.pow_le_pow_right two_pos (hdeg.trans (le_of_eq ?_))
+          unfold letterBits
+          ring
+      _ = (2 ^ b a) ^ (2 * (3 * k + 1) * (s + k + 4)) := pow_mul _ _ _
+      _ ≤ cap a ^ (2 * (3 * k + 1) * (s + k + 4)) := Nat.pow_le_pow_left (h2b a) _
+  unfold explicitTableNum
+  have ha : ComputableInPolyTime (fun p : α × ℕ => p.1) (encPair inp encUnary) inp := fst _ _
+  exact mapWithInput (range.comp hlen) (computableInPolyTime_tableEntryNum e machine
+    (hx.comp ha) (hb.comp ha) (fun p => hb0 p.1) (hq.comp ha) (hσ.comp ha) (hcap.comp ha)
+    (fun p => h2b p.1) (hv.comp ha) (hP.comp ha) (snd _ _))
+
+/-- **The explicit block-counting network on numbers is polynomial-time**, as its number of edges
+in unary and its list of vertices, each the pair of its ports and its table as lists of binary
+numbers. -/
+theorem computableInPolyTime_explicitNetworkNum
+    (hx : ComputableInPolyTime x inp encBits) (hb : ComputableInPolyTime b inp encUnary)
+    (hb0 : ∀ a, 0 < b a) (hq : ComputableInPolyTime q inp encUnary)
+    (hσ : ComputableInPolyTime σ inp encNat) (hcap : ComputableInPolyTime cap inp encUnary)
+    (h2b : ∀ a, 2 ^ b a ≤ cap a) :
+    ComputableInPolyTime (fun a => ((explicitNetworkNum e (b a) machine (x a) (q a) (σ a)).numEdges,
+        (explicitNetworkNum e (b a) machine (x a) (q a) (σ a)).vertices)) inp
+      (encPair encUnary (encList (encPair (encList encNat) (encList encNat)))) := by
+  have hm : ComputableInPolyTime (fun a => letterBits k s (b a)) inp encUnary := by
+    unfold letterBits
+    exact unary_mul' (const _) hb
+  have ha : ComputableInPolyTime (fun p : α × ℕ => p.1) (encPair inp encUnary) inp := fst _ _
+  refine (unary_mul' (const 2) (unary_mul' (unary_mul' hq (const _)) hm)).prod ?_
+  unfold explicitNetworkNum explicitVerticesNum
+  refine mapWithInput (range.comp (unary_add' (unary_mul' hq (const _))
+    (unary_mul' (unary_mul' hq (const _)) hm))) ((computableInPolyTime_explicitPortsNum
+      (hq.comp ha) (hm.comp ha) (hσ.comp ha) (snd _ _)).prod ?_)
+  exact computableInPolyTime_explicitTableNum e machine (hx.comp ha) (hb.comp ha) (fun p => hb0 p.1)
+    (hq.comp ha) (hσ.comp ha) (hcap.comp ha) (fun p => h2b p.1) (snd _ _)
+
+end Tables
+
+end Turing.MultiTapePTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean
index 61b1feb78a..b2581b0aa0 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean
@@ -60,7 +60,8 @@ their stored cells (`Turing.MultiTapeTM.encBiTape`), and the head positions in b
 ## Main results
 
 * `Turing.MultiTapePTM.computableInPolyTime_localRun`: replays are polynomial-time.
-* `Turing.MultiTapePTM.IntervalData.computableInPolyTime_mk`: assembling the arguments.
+* `Turing.MultiTapePTM.IntervalData.computableInPolyTime_mk`,
+  `Turing.MultiTapePTM.ControlData.computableInPolyTime_mk`: assembling the arguments.
 * `Turing.MultiTapePTM.computableInPolyTime_localIntervalCount`: interval counts are
   polynomial-time when the `2 ^ b` coin strings are polynomially many in the input.
 -/
@@ -605,6 +606,16 @@ noncomputable def encIntervalData : IntervalData k State ↪ List Bool :=
 
 variable {α : Type} {input : α ↪ List Bool}
 
+/-- Assemble a control record on plain data from its certified components. -/
+theorem ControlData.computableInPolyTime_mk {state : α → Option State}
+    {off : α → Option (Fin k) → ℕ} {track : α → OutputTrack}
+    (hstate : ComputableInPolyTime state input (encFinite (Option State)))
+    (hoff : ComputableInPolyTime off input (encPi encUnary))
+    (htrack : ComputableInPolyTime track input (encFinite OutputTrack)) :
+    ComputableInPolyTime (fun a => ((state a, off a, track a) : ControlData k State)) input
+      encControlData :=
+  (hstate.prod (hoff.prod htrack)).of_enc_eq fun _ => rfl
+
 /-- Assemble the arguments of an interval count from their certified components. -/
 theorem IntervalData.computableInPolyTime_mk {word : α → List Bool} {b : α → ℕ}
     {J : α → Option (Fin k) → ℤ} {δ : α → Option (Fin k) → SignType}
diff --git a/ComplexityTests/HPVExplicitTables.lean b/ComplexityTests/HPVExplicitTables.lean
new file mode 100644
index 0000000000..a29d7be5cd
--- /dev/null
+++ b/ComplexityTests/HPVExplicitTables.lean
@@ -0,0 +1,77 @@
+/-
+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.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.TablePolyTime
+
+/-! The tables of the explicit block-counting networks on numbers: decoded letters, table entries
+of a concrete machine read off the explicit network, and the polynomial-time certificate. -/
+
+namespace ComplexityTests.HPVExplicitTables
+
+open Turing MultiTapeMachine MultiTapePTM MultiTapeNTM.ChoiceTable Cslib.Circuits.Frontier
+
+/-- Emit the first coin and halt. No work tapes; the input head stays. -/
+private def emitCoin : MultiTapePTM 0 Bool Unit where
+  initial := ()
+  tr _ _ _ _ bit := .step
+    { inputTape := 0, workTapes := Fin.elim0, output := some bit, state := none }
+    Empty.elim Empty.elim
+
+/-! ### Decoding letters -/
+
+-- With two states, one work tape and blocks of two cells there are `3 * (2 ^ 2 * 3) = 36`
+-- control records. Letter `34` is the record of state `true`, both offsets `1` and output track
+-- `accept` (compare `HPVExplicitBlockNetwork`), and letter `44` is the block holding `true` twice.
+example : decodeControlData (k := 1) finTwoEquiv.symm 2 34 =
+    controlData (some true, (fun _ => 1 : Option (Fin 1) → ZMod 2), OutputTrack.accept) := by
+  rw [show (34 : ℕ) = letterEquiv (k := 1) (b := 2) finTwoEquiv.symm
+    (.inl (some true, fun _ => 1, .accept)) by decide]
+  simp only [letterEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inl,
+    finSumFinEquiv_apply_left, Fin.val_castAdd, decodeControlData_controlEquiv]
+
+example : contentsCellNum 1 2 2 44 0 = some true ∧ contentsCellNum 1 2 2 44 1 = some true ∧
+    acceptNum 1 2 2 34 = 1 ∧ acceptNum 1 2 2 44 = 0 := by decide
+
+/-! ### Table entries of `emitCoin` -/
+
+-- One interval of two steps; letters of `10` bits. The interval (vertex `0`) has the source
+-- halves of its control edge as ports. At index `1` its leaving letter is number `1`: halted,
+-- offsets `0`, output track `accept`, reached by the two coin strings starting with `true`.
+example : ((emitCoin.explicitBlockNetwork [] 2 (scheduleOfNat 0 1 1)
+    (Equiv.ofUnique Unit (Fin 1))).vertices[0]!.2)[1]! = 2 := by
+  rw [explicitBlockNetwork_eq_explicitNetworkNum]
+  decide +kernel
+
+-- The sink of the control edge (vertex `1`) accepts letter `1` and rejects letter `0`, whose
+-- output track is empty.
+example : ((emitCoin.explicitBlockNetwork [] 2 (scheduleOfNat 0 1 1)
+      (Equiv.ofUnique Unit (Fin 1))).vertices[1]!.2)[1]! = 1 ∧
+    ((emitCoin.explicitBlockNetwork [] 2 (scheduleOfNat 0 1 1)
+      (Equiv.ofUnique Unit (Fin 1))).vertices[1]!.2)[0]! = 0 := by
+  rw [explicitBlockNetwork_eq_explicitNetworkNum]
+  decide +kernel
+
+-- A subdivision vertex (vertex `2`) is the equality of the bits on its two ports.
+example : (emitCoin.explicitBlockNetwork [] 2 (scheduleOfNat 0 1 1)
+    (Equiv.ofUnique Unit (Fin 1))).vertices[2]!.2 = [1, 0, 0, 1] := by
+  rw [explicitBlockNetwork_eq_explicitNetworkNum]
+  decide +kernel
+
+/-! ### Polynomial time -/
+
+-- The network of `emitCoin` with blocks of two steps and one interval is polynomial-time in the
+-- schedule number, with `2 ^ 2 ≤ 4`.
+example : MultiTapeTM.ComputableInPolyTime (fun σ : ℕ =>
+    ((explicitNetworkNum (Equiv.ofUnique Unit (Fin 1)) 2 emitCoin [] 1 σ).numEdges,
+      (explicitNetworkNum (Equiv.ofUnique Unit (Fin 1)) 2 emitCoin [] 1 σ).vertices))
+    MultiTapeTM.encNat (MultiTapeTM.encPair MultiTapeTM.encUnary
+      (MultiTapeTM.encList (MultiTapeTM.encPair (MultiTapeTM.encList MultiTapeTM.encNat)
+        (MultiTapeTM.encList MultiTapeTM.encNat)))) :=
+  computableInPolyTime_explicitNetworkNum (Equiv.ofUnique Unit (Fin 1)) emitCoin (.const _)
+    (.const _) (fun _ => two_pos) (.const _) MultiTapeTM.ComputableInPolyTime.id' (.const 4)
+    (fun _ => le_refl 4)
+
+end ComplexityTests.HPVExplicitTables