diff --git a/Complexity.lean b/Complexity.lean
index 8f5f9ddb1..329dbecd4 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1847,6 +1847,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.C
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork
 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.IntervalTensor
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean
index 051a95b90..42914f7f8 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork
 public import Complexity.Foundations.Data.BitString.Counter
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.List.GetD
+import Mathlib.Data.Set.Card
 
 /-!
 # Explicit Boolean tensor networks
@@ -30,12 +31,17 @@ reads `false`, and a position past the end of a table has entry zero.
 
 Its size measures are the number of edges, the number of vertices, the maximum number of ports of
 a vertex (`ExplicitTensorNetwork.maxDegree`) and the total length of the tables
-(`ExplicitTensorNetwork.tableLength`).
+(`ExplicitTensorNetwork.tableLength`). A network is *rows-first bipartite* with `r` rows
+(`ExplicitTensorNetwork.IsRowsFirstBipartite`) when every edge is a port of exactly one of its
+first `r` vertices and of exactly one of the others.
 
 **Writing a network out** (`TensorNetwork.toExplicit`). Given numberings of the vertices and the
 edges of a Boolean tensor network on finite types, list the edges at each vertex in increasing
 order and tabulate its tensor on them. The contraction is unchanged
-(`TensorNetwork.contraction_toExplicit`).
+(`TensorNetwork.contraction_toExplicit`). The ports of a vertex are its incident edges, so the
+degree bound carries over (`TensorNetwork.maxDegree_toExplicit_le`), and a numbering that puts
+one end of every edge below `r` and the other at or above it gives a rows-first bipartite network
+(`TensorNetwork.isRowsFirstBipartite_toExplicit`).
 
 ## Main definitions
 
@@ -46,6 +52,8 @@ order and tabulate its tensor on them. The contraction is unchanged
 * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction`: the contraction.
 * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree`,
   `Cslib.Circuits.Frontier.ExplicitTensorNetwork.tableLength`: size measures.
+* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`: the bipartition with the
+  first `r` vertices as rows.
 * `Cslib.Circuits.Frontier.TensorNetwork.explicitPorts`,
   `Cslib.Circuits.Frontier.TensorNetwork.explicitTable`,
   `Cslib.Circuits.Frontier.TensorNetwork.toExplicit`: writing a Boolean tensor network out.
@@ -57,6 +65,12 @@ order and tabulate its tensor on them. The contraction is unchanged
   tensor.
 * `Cslib.Circuits.Frontier.TensorNetwork.contraction_toExplicit`: writing a network out preserves
   its contraction.
+* `Cslib.Circuits.Frontier.TensorNetwork.length_explicitPorts`: a vertex has one port per incident
+  edge.
+* `Cslib.Circuits.Frontier.TensorNetwork.maxDegree_toExplicit_le`,
+  `Cslib.Circuits.Frontier.TensorNetwork.isRowsFirstBipartite_toExplicit`,
+  `Cslib.Circuits.Frontier.TensorNetwork.length_table_toExplicit`: degree, bipartition and table
+  lengths of a written-out network.
 
 ## References
 
@@ -123,6 +137,18 @@ theorem length_le_maxDegree {v : List ℕ × List R} (hv : v ∈ d.vertices) :
     v.1.length ≤ d.maxDegree :=
   d.maxDegree_le_iff.mp le_rfl v hv
 
+/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*,
+every port names an edge, and every edge is a port of the rows exactly once and of the columns
+exactly once. So every edge joins a row to a column. -/
+def IsRowsFirstBipartite (r : ℕ) : Prop :=
+  (∀ v ∈ d.vertices, ∀ i ∈ v.1, i < d.numEdges) ∧
+    ∀ i < d.numEdges, ((d.vertices.take r).map fun v => v.1.count i).sum = 1 ∧
+      ((d.vertices.drop r).map fun v => v.1.count i).sum = 1
+
+instance (r : ℕ) : Decidable (d.IsRowsFirstBipartite r) := by
+  unfold IsRowsFirstBipartite
+  infer_instance
+
 end ExplicitTensorNetwork
 
 /-! ### Writing a tensor network out -/
@@ -163,6 +189,40 @@ theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) :
   rw [BitString.testBit_lsbValue, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map,
     List.getElem_idxOf hidx, Function.comp_apply]
 
+/-- An edge is a port of a vertex at most once. -/
+theorem nodup_explicitPorts (v : V) : (N.explicitPorts ee v).Nodup :=
+  (List.nodup_finRange m).filter _
+
+/-- **The ports of a vertex are its incident edges**: their number is its degree. -/
+theorem length_explicitPorts (v : V) :
+    (N.explicitPorts ee v).length = (N.incidenceSet v).ncard := by
+  classical
+  rw [← List.toFinset_card_of_nodup (N.nodup_explicitPorts ee v),
+    ← Set.ncard_image_of_injective _ ee.injective, ← Set.ncard_coe_finset]
+  congr 1
+  ext j
+  simp [Multigraph.mem_incidenceSet]
+
+/-- The number of times the edge numbered `j` is a port of `v`: once if it is incident to `v`, and
+never otherwise. -/
+theorem count_explicitPorts (v : V) (j : Fin m) :
+    ((N.explicitPorts ee v).map Fin.val).count j.val =
+      if N.src (ee.symm j) = v ∨ N.tgt (ee.symm j) = v then 1 else 0 := by
+  rw [List.Nodup.count ((N.nodup_explicitPorts ee v).map Fin.val_injective)]
+  simp only [List.mem_map, Fin.val_inj, exists_eq_right, mem_explicitPorts]
+
+/-- A table lists the values of the tensor at all `2 ^ (number of ports)` lists of bits on the
+ports. -/
+theorem length_explicitTable (v : V) :
+    (N.explicitTable ee v).length = 2 ^ (N.explicitPorts ee v).length := by
+  simp [explicitTable]
+
+/-- Every entry of a written-out table is a value of the tensor. -/
+theorem exists_tensor_of_mem_explicitTable {v : V} {a : R} (ha : a ∈ N.explicitTable ee v) :
+    ∃ y, a = N.tensor v y := by
+  obtain ⟨j, -, rfl⟩ := List.mem_map.mp ha
+  exact ⟨_, rfl⟩
+
 /-- A Boolean tensor network on finite types written out as an explicit network, numbering the
 vertices by `ev` and the edges by `ee`: vertex `i` is `ev.symm i`, with its ports in increasing
 order and its table. -/
@@ -171,6 +231,85 @@ def toExplicit : ExplicitTensorNetwork R where
   vertices := List.ofFn fun i =>
     ((N.explicitPorts ee (ev.symm i)).map Fin.val, N.explicitTable ee (ev.symm i))
 
+/-- The vertices of the written-out network are the ports and tables of the vertices. -/
+theorem mem_vertices_toExplicit {p : List ℕ × List R} :
+    p ∈ (N.toExplicit ev ee).vertices ↔
+      ∃ v, p = ((N.explicitPorts ee v).map Fin.val, N.explicitTable ee v) := by
+  simp only [toExplicit, List.mem_ofFn]
+  constructor
+  · rintro ⟨i, rfl⟩
+    exact ⟨_, rfl⟩
+  · rintro ⟨v, rfl⟩
+    exact ⟨ev v, by simp⟩
+
+/-- **The degree bound carries over**: a vertex of the written-out network has as many ports as
+the vertex has incident edges. -/
+theorem maxDegree_toExplicit_le [Finite E] {D : ℕ} (hD : N.MaxDegreeLE D) :
+    (N.toExplicit ev ee).maxDegree ≤ D := by
+  rw [ExplicitTensorNetwork.maxDegree_le_iff]
+  intro p hp
+  obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp
+  rw [List.length_map, length_explicitPorts]
+  exact hD v
+
+/-- Every table of the written-out network has an entry for every list of bits on its ports. -/
+theorem length_table_toExplicit {p : List ℕ × List R} (hp : p ∈ (N.toExplicit ev ee).vertices) :
+    p.2.length = 2 ^ p.1.length := by
+  obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp
+  simp [length_explicitTable]
+
+/-- Every table entry of the written-out network is a value of a tensor. -/
+theorem exists_tensor_of_mem_toExplicit {p : List ℕ × List R}
+    (hp : p ∈ (N.toExplicit ev ee).vertices) {a : R} (ha : a ∈ p.2) :
+    ∃ v y, a = N.tensor v y := by
+  obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp
+  exact ⟨v, N.exists_tensor_of_mem_explicitTable ee ha⟩
+
+private theorem sum_drop_ofFn (f : Fin n → ℕ) (r : ℕ) :
+    ((List.ofFn f).drop r).sum = ∑ a with ¬ a.val < r, f a := by
+  have h := List.sum_take_add_sum_drop (List.ofFn f) r
+  rw [List.sum_take_ofFn, List.sum_ofFn,
+    ← Finset.sum_filter_add_sum_filter_not Finset.univ (fun a : Fin n => a.val < r)] at h
+  omega
+
+/-- **Rows first.** If every edge joins a vertex numbered below `r` to one numbered at least `r`,
+the written-out network is bipartite with the first `r` vertices as rows. -/
+theorem isRowsFirstBipartite_toExplicit (r : ℕ)
+    (hside : ∀ e, (ev (N.src e) : ℕ) < r ↔ ¬ (ev (N.tgt e) : ℕ) < r) :
+    (N.toExplicit ev ee).IsRowsFirstBipartite r := by
+  refine ⟨fun p hp i hi => ?_, fun i hi => ?_⟩
+  · obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp
+    obtain ⟨j, -, rfl⟩ := List.mem_map.mp hi
+    exact j.isLt
+  · -- The edge numbered `i` is a port of its source and its target, which are distinct.
+    set j : Fin m := ⟨i, hi⟩
+    set e := ee.symm j
+    have hne : N.src e ≠ N.tgt e := fun h => by
+      have := hside e
+      rw [h] at this
+      tauto
+    have hcount : ∀ a : Fin n, ((N.explicitPorts ee (ev.symm a)).map Fin.val).count i =
+        (if ev (N.src e) = a then 1 else 0) + (if ev (N.tgt e) = a then 1 else 0) := by
+      intro a
+      rw [show i = j.val from rfl, count_explicitPorts]
+      simp only [Equiv.eq_symm_apply]
+      by_cases hs : ev (N.src e) = a <;> by_cases ht : ev (N.tgt e) = a
+      · exact absurd (ev.injective (hs.trans ht.symm)) hne
+      all_goals simp [e, hs, ht]
+    have hsum : ∀ s : Finset (Fin n),
+        ∑ a ∈ s, ((N.explicitPorts ee (ev.symm a)).map Fin.val).count i =
+          (if ev (N.src e) ∈ s then 1 else 0) + (if ev (N.tgt e) ∈ s then 1 else 0) := by
+      intro s
+      simp only [hcount, Finset.sum_add_distrib, Finset.sum_ite_eq]
+    have hv : (N.toExplicit ev ee).vertices = List.ofFn fun a =>
+        ((N.explicitPorts ee (ev.symm a)).map Fin.val, N.explicitTable ee (ev.symm a)) := rfl
+    rw [hv, List.map_take, List.map_drop, List.map_ofFn, List.sum_take_ofFn, sum_drop_ofFn]
+    simp only [Function.comp_def]
+    rw [hsum, hsum]
+    have := hside e
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
+    by_cases h : (ev (N.src e) : ℕ) < r <;> simp_all
+
 /-- **Writing a network out preserves its contraction.** -/
 theorem contraction_toExplicit [CommSemiring R] [Fintype V] [Fintype E] [DecidableEq E] :
     (N.toExplicit ev ee).contraction = N.contraction := by
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean
new file mode 100644
index 000000000..56ed22be4
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean
@@ -0,0 +1,364 @@
+/-
+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.BlockNetwork
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Data.ZMod.Basic
+public import Mathlib.Data.Nat.Log
+public import Mathlib.Logic.Equiv.Fin.Basic
+
+/-!
+# Explicit block-counting networks
+
+The block-counting network of a schedule (`Turing.MultiTapePTM.blockNetwork`) carries structured
+letters on its edges: control records and block contents (`Turing.MultiTapePTM.BlockLetter`).
+This module writes it out as an explicit Boolean tensor network
+(`Cslib.Circuits.Frontier.ExplicitTensorNetwork`), the form that a contraction algorithm reads,
+completing the construction of Lemma 2.2 of the note *Deterministic simulations of
+nondeterministic and randomized time* (30 October 2026) formalized in issue #1833:
+
+1. **Binarize** by a concrete injective code of the letters
+   (`Turing.MultiTapePTM.letterCode`), in `letterBits k s b = (s + k + 4) * b` bits, where `s`
+   numbers the states. A letter is numbered by `Turing.MultiTapePTM.letterEquiv`, composed of the
+   standard numberings of finite products, sums, options and functions (`finProdFinEquiv`,
+   `finSumFinEquiv`, `finSuccEquiv`, `finFunctionFinEquiv`); its code is the binary digits of its
+   number.
+2. **Subdivide** every Boolean edge by an equality tensor, which makes the network bipartite.
+3. **Write out** (`Cslib.Circuits.Frontier.TensorNetwork.toExplicit`), numbering the old vertices
+   (the intervals and sinks) first and the subdivision vertices after them, both by concrete
+   numberings (`Turing.MultiTapePTM.explicitVertexEquiv`, `Turing.MultiTapePTM.explicitEdgeEquiv`).
+
+Each step preserves the contraction, so the explicit networks of the schedules still sum to the
+accepting count (`Turing.MultiTapePTM.sum_contraction_explicitBlockNetwork`).
+
+**Size.** With `q` intervals, `k` work tapes and `m = letterBits k s b`, the explicit network has
+`2 * (q * (3 * k + 1) * m)` edges and maximum degree at most `2 * (3 * k + 1) * m`, both `O(b)` per
+interval. Its first `q * (3 * k + 2)` vertices are the rows of a bipartition: every edge has
+exactly one port at a row and one at a column
+(`Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`). Every table has length
+`2 ^ (number of ports)`, and its entries are at most `2 ^ b`.
+
+These are the inputs of the Boolean tensor contraction theorem [OpenAI2026ETH, Theorem D.1]
+as the counting simulation of #1833 uses it: with `b = ⌈log₂ (t + 2)⌉` and `q * b ≤ 2 t`, the
+networks have `O(t)` edges and maximum degree `O(log t)`.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.letterEquiv`, `Turing.MultiTapePTM.letterCode`,
+  `Turing.MultiTapePTM.letterBits`: the numbering and binary code of the letters.
+* `Turing.MultiTapePTM.blockEdgeEquiv`, `Turing.MultiTapePTM.explicitVertexEquiv`,
+  `Turing.MultiTapePTM.explicitEdgeEquiv`: the numberings of edges and vertices.
+* `Turing.MultiTapePTM.explicitBlockNetwork`: the explicit block-counting network of a schedule.
+
+## Main results
+
+* `Turing.MultiTapePTM.letterCode_injective`: the code is injective.
+* `Turing.MultiTapePTM.contraction_explicitBlockNetwork`: writing the network out preserves its
+  contraction.
+* `Turing.MultiTapePTM.sum_contraction_explicitBlockNetwork`: summed over the schedules, the
+  contractions are the accepting count.
+* `Turing.MultiTapePTM.admissible_explicitBlockNetwork`: at a clock `t` with `b = O(log t)` and
+  `q * b ≤ 2 t`, the network is rows-first bipartite with `O(t)` edges and degree `O(log t)`.
+* `Turing.MultiTapePTM.numEdges_explicitBlockNetwork`,
+  `Turing.MultiTapePTM.length_vertices_explicitBlockNetwork`,
+  `Turing.MultiTapePTM.maxDegree_explicitBlockNetwork_le`,
+  `Turing.MultiTapePTM.isRowsFirstBipartite_explicitBlockNetwork`,
+  `Turing.MultiTapePTM.length_table_explicitBlockNetwork`,
+  `Turing.MultiTapePTM.entry_le_explicitBlockNetwork`: size, degree, bipartition and tables.
+
+## References
+
+* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977]
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53)
+-/
+
+public section
+
+namespace Turing
+
+namespace MultiTapeNTM.ChoiceTable.OutputTrack
+
+/-- The output tracks numbered `empty ↦ 0`, `accept ↦ 1`, `other ↦ 2`. -/
+@[expose] def equivFin : OutputTrack ≃ Fin 3 where
+  toFun
+    | .empty => 0
+    | .accept => 1
+    | .other => 2
+  invFun i := if i = 0 then .empty else if i = 1 then .accept else .other
+  left_inv t := by cases t <;> rfl
+  right_inv i := by fin_cases i <;> rfl
+
+end MultiTapeNTM.ChoiceTable.OutputTrack
+
+namespace MultiTapePTM
+
+open Cslib.Circuits.Frontier MultiTapeNTM.ChoiceTable Function
+
+variable {k q s : ℕ} {State : Type} {b : ℕ}
+
+/-! ### Numbering and coding the letters -/
+
+section Letters
+
+variable [NeZero b]
+
+/-- The residues modulo `b > 0` numbered by their values. -/
+@[expose] def zmodEquiv (b : ℕ) [NeZero b] : ZMod b ≃ Fin b :=
+  (ZMod.finEquiv b).toEquiv.symm
+
+@[simp] theorem val_zmodEquiv (r : ZMod b) : (zmodEquiv b r : ℕ) = r.val := by
+  obtain _ | b := b
+  · exact absurd rfl (NeZero.ne 0)
+  · rfl
+
+/-- The contents of a cell numbered `none ↦ 0`, `some false ↦ 1`, `some true ↦ 2`. -/
+@[expose] def cellEquiv : Option Bool ≃ Fin 3 :=
+  (Equiv.optionCongr finTwoEquiv.symm).trans (finSuccEquiv 2).symm
+
+/-- The control records numbered: the state (with `none` first, then the states numbered by `e`),
+then the head offsets as `k + 1` digits in base `b`, then the output track. -/
+@[expose] def controlEquiv (e : State ≃ Fin s) :
+    BlockControl k State b ≃ Fin ((s + 1) * (b ^ (k + 1) * 3)) :=
+  (Equiv.prodCongr ((Equiv.optionCongr e).trans (finSuccEquiv s).symm)
+    ((Equiv.prodCongr
+      ((Equiv.arrowCongr (finSuccEquiv k).symm (zmodEquiv b)).trans finFunctionFinEquiv)
+      OutputTrack.equivFin).trans finProdFinEquiv)).trans finProdFinEquiv
+
+/-- The block contents numbered as `b` digits in base `3`. -/
+@[expose] def contentsEquiv (b : ℕ) [NeZero b] : (ZMod b → Option Bool) ≃ Fin (3 ^ b) :=
+  (Equiv.arrowCongr (zmodEquiv b) cellEquiv).trans finFunctionFinEquiv
+
+/-- **The letters numbered**: the control records first (`Turing.MultiTapePTM.controlEquiv`),
+then the block contents (`Turing.MultiTapePTM.contentsEquiv`). -/
+@[expose] def letterEquiv (e : State ≃ Fin s) :
+    BlockLetter k State b ≃ Fin ((s + 1) * (b ^ (k + 1) * 3) + 3 ^ b) :=
+  (Equiv.sumCongr (controlEquiv e) (contentsEquiv b)).trans finSumFinEquiv
+
+/-- The number of bits of a letter: `(s + k + 4) * b`, for `s` states and `k` work tapes. -/
+@[expose] def letterBits (k s b : ℕ) : ℕ := (s + k + 4) * b
+
+/-- Every letter number fits in `letterBits k s b` bits. -/
+theorem card_letter_le_two_pow :
+    (s + 1) * (b ^ (k + 1) * 3) + 3 ^ b ≤ 2 ^ letterBits k s b := by
+  have hb : 1 ≤ b := Nat.one_le_iff_ne_zero.mpr (NeZero.ne b)
+  have hs : s + 1 ≤ 2 ^ (s * b) :=
+    (Nat.lt_two_pow_self).trans_le (Nat.pow_le_pow_right two_pos (Nat.le_mul_of_pos_right s hb))
+  have hbk : b ^ (k + 1) ≤ 2 ^ ((k + 1) * b) := by
+    rw [mul_comm, pow_mul]
+    exact Nat.pow_le_pow_left (Nat.lt_two_pow_self).le _
+  have h3 : 3 ≤ 2 ^ (2 * b) := by
+    calc 3 ≤ 2 ^ 2 := by norm_num
+      _ ≤ 2 ^ (2 * b) := Nat.pow_le_pow_right two_pos (by omega)
+  have h3b : 3 ^ b ≤ 2 ^ (2 * b) := by
+    rw [pow_mul]
+    exact Nat.pow_le_pow_left (by norm_num) _
+  have hctl : (s + 1) * (b ^ (k + 1) * 3) ≤ 2 ^ ((s + k + 3) * b) := by
+    calc (s + 1) * (b ^ (k + 1) * 3) ≤ 2 ^ (s * b) * (2 ^ ((k + 1) * b) * 2 ^ (2 * b)) :=
+          Nat.mul_le_mul hs (Nat.mul_le_mul hbk h3)
+      _ = 2 ^ ((s + k + 3) * b) := by rw [← pow_add, ← pow_add]; ring_nf
+  have hcon : 3 ^ b ≤ 2 ^ ((s + k + 3) * b) :=
+    h3b.trans (Nat.pow_le_pow_right two_pos (Nat.mul_le_mul_right b (by omega)))
+  calc _ ≤ 2 ^ ((s + k + 3) * b) + 2 ^ ((s + k + 3) * b) := Nat.add_le_add hctl hcon
+    _ = 2 ^ ((s + k + 3) * b + 1) := by rw [pow_succ]; ring
+    _ ≤ 2 ^ letterBits k s b :=
+        Nat.pow_le_pow_right two_pos (by unfold letterBits; nlinarith)
+
+/-- **The letter code**: the `letterBits k s b` binary digits, least significant first, of the
+number of a letter (`Turing.MultiTapePTM.letterEquiv`). -/
+@[expose] def letterCode (e : State ≃ Fin s) (l : BlockLetter k State b) :
+    Fin (letterBits k s b) → Bool :=
+  fun j => (letterEquiv e l : ℕ).testBit j
+
+/-- **The letter code is injective**: letter numbers fit in `letterBits k s b` bits. -/
+theorem letterCode_injective (e : State ≃ Fin s) :
+    Injective (letterCode (k := k) (b := b) e) := by
+  intro l l' h
+  have hlt : ∀ l : BlockLetter k State b, (letterEquiv e l : ℕ) < 2 ^ letterBits k s b :=
+    fun l => (letterEquiv e l).isLt.trans_le card_letter_le_two_pow
+  refine (letterEquiv e).injective (Fin.ext (Nat.eq_of_testBit_eq fun j => ?_))
+  by_cases hj : j < letterBits k s b
+  · exact congrFun h ⟨j, hj⟩
+  · rw [Nat.testBit_lt_two_pow ((hlt l).trans_le (Nat.pow_le_pow_right two_pos (not_lt.mp hj))),
+      Nat.testBit_lt_two_pow ((hlt l').trans_le (Nat.pow_le_pow_right two_pos (not_lt.mp hj)))]
+
+instance : Nonempty (BlockLetter k State b) := ⟨.inr fun _ => none⟩
+
+end Letters
+
+/-! ### Numbering the edges and vertices -/
+
+-- A named instance keeps the instances on the vertex types of the explicit network small.
+instance (k q : ℕ) : DecidableEq (BlockEdge k q) :=
+  inferInstanceAs (DecidableEq (Fin q ⊕ (Fin q × Fin k × Fin 3)))
+
+/-- The edges of a block-counting network numbered: the control edges first, then the block edges
+`(i, h, d)` in lexicographic order. -/
+@[expose] def blockEdgeEquiv (k q : ℕ) : BlockEdge k q ≃ Fin (q * (3 * k + 1)) :=
+  ((Equiv.sumCongr (Equiv.refl _)
+    ((Equiv.prodCongr (Equiv.refl _) finProdFinEquiv).trans finProdFinEquiv)).trans
+      finSumFinEquiv).trans (finCongr (by ring))
+
+/-- The vertices of the explicit network numbered: the old vertices first (the intervals, then the
+sinks in the order of their edges), then the subdivision vertices, one for each copy `(e, j)` of an
+edge. -/
+@[expose] def explicitVertexEquiv (k q m : ℕ) :
+    (Fin q ⊕ BlockEdge k q) ⊕ (BlockEdge k q × Fin m) ≃
+      Fin (q * (3 * k + 2) + q * (3 * k + 1) * m) :=
+  (Equiv.sumCongr
+    (((Equiv.sumCongr (Equiv.refl _) (blockEdgeEquiv k q)).trans finSumFinEquiv).trans
+      (finCongr (by ring)))
+    ((Equiv.prodCongr (blockEdgeEquiv k q) (Equiv.refl _)).trans finProdFinEquiv)).trans
+    finSumFinEquiv
+
+/-- The edges of the explicit network numbered: the source halves of the copies `(e, j)` first,
+then their target halves. -/
+@[expose] def explicitEdgeEquiv (k q m : ℕ) :
+    (BlockEdge k q × Fin m) ⊕ (BlockEdge k q × Fin m) ≃ Fin (2 * (q * (3 * k + 1) * m)) :=
+  ((Equiv.sumCongr ((Equiv.prodCongr (blockEdgeEquiv k q) (Equiv.refl _)).trans finProdFinEquiv)
+    ((Equiv.prodCongr (blockEdgeEquiv k q) (Equiv.refl _)).trans finProdFinEquiv)).trans
+      finSumFinEquiv).trans (finCongr (by ring))
+
+/-- The old vertices come first. -/
+theorem explicitVertexEquiv_inl (k q m : ℕ) (v : Fin q ⊕ BlockEdge k q) :
+    (explicitVertexEquiv k q m (.inl v) : ℕ) < q * (3 * k + 2) := by
+  simp only [explicitVertexEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inl,
+    finSumFinEquiv_apply_left, Fin.val_castAdd]
+  exact Fin.isLt _
+
+/-- The subdivision vertices come after the old ones. -/
+theorem le_explicitVertexEquiv_inr (k q m : ℕ) (p : BlockEdge k q × Fin m) :
+    q * (3 * k + 2) ≤ (explicitVertexEquiv k q m (.inr p) : ℕ) := by
+  simp only [explicitVertexEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inr,
+    finSumFinEquiv_apply_right, Fin.val_natAdd]
+  omega
+
+/-! ### The explicit network -/
+
+variable (machine : MultiTapePTM k Bool State) (input : List Bool) (b : ℕ) [NeZero b]
+  (σ : Schedule k q) (e : State ≃ Fin s)
+
+/-- **The explicit block-counting network** of the schedule `σ`: the block-counting network
+binarized by the letter code (`Turing.MultiTapePTM.letterCode`), subdivided by equality tensors
+and written out with the old vertices first. Its first `q * (3 * k + 2)` vertices are the rows of
+its bipartition. -/
+@[expose] noncomputable def explicitBlockNetwork : ExplicitTensorNetwork ℕ :=
+  ((machine.blockNetwork input b σ).binarize (letterCode e)).subdivide.toExplicit
+    (explicitVertexEquiv k q (letterBits k s b)) (explicitEdgeEquiv k q (letterBits k s b))
+
+/-- **Writing the network out preserves its contraction.** -/
+theorem contraction_explicitBlockNetwork [Fintype State] :
+    (machine.explicitBlockNetwork input b σ e).contraction =
+      (machine.blockNetwork input b σ).contraction := by
+  rw [explicitBlockNetwork, TensorNetwork.contraction_toExplicit,
+    TensorNetwork.contraction_subdivide,
+    TensorNetwork.contraction_binarize _ (letterCode_injective e)]
+
+/-- **The block-counting identity for the explicit networks** (the note's Lemma 2.2, equation
+(2)). Summed over the movement schedules of `q > 0` intervals of `b` bits, the contractions of the
+explicit block-counting networks are the accepting count on `q * b` bits. -/
+theorem sum_contraction_explicitBlockNetwork [Finite State] (hq : 0 < q) :
+    ∑ σ : Schedule k q, (machine.explicitBlockNetwork input b σ e).contraction =
+      machine.acceptCount input (q * b) := by
+  have := Fintype.ofFinite State
+  simp only [contraction_explicitBlockNetwork]
+  exact machine.sum_contraction_blockNetwork input b hq
+
+/-- The explicit network has `2 * (q * (3 * k + 1) * letterBits k s b)` edges: two halves of each
+of the `letterBits k s b` copies of each of the `q * (3 * k + 1)` edges. -/
+theorem numEdges_explicitBlockNetwork :
+    (machine.explicitBlockNetwork input b σ e).numEdges =
+      2 * (q * (3 * k + 1) * letterBits k s b) := rfl
+
+/-- The explicit network has `q * (3 * k + 2)` old vertices and one subdivision vertex for each
+copy of an edge. -/
+theorem length_vertices_explicitBlockNetwork :
+    (machine.explicitBlockNetwork input b σ e).vertices.length =
+      q * (3 * k + 2) + q * (3 * k + 1) * letterBits k s b := by
+  simp [explicitBlockNetwork, TensorNetwork.toExplicit]
+
+/-- **The degree bound**: at most `2 * (3 * k + 1) * letterBits k s b` ports at every vertex,
+`O(b)` for a fixed machine. -/
+theorem maxDegree_explicitBlockNetwork_le :
+    (machine.explicitBlockNetwork input b σ e).maxDegree ≤
+      2 * (3 * k + 1) * letterBits k s b := by
+  have hm : 1 ≤ letterBits k s b :=
+    Nat.mul_pos (by omega) (Nat.pos_of_neZero b)
+  refine TensorNetwork.maxDegree_toExplicit_le _ _ _
+    (TensorNetwork.maxDegreeLE_subdivide _ ?_ ?_ ?_)
+  · exact TensorNetwork.loopless_binarize _ _ (machine.loopless_blockNetwork input b σ)
+  · exact TensorNetwork.maxDegreeLE_binarize _ _ (machine.maxDegreeLE_blockNetwork input b σ)
+  · nlinarith
+
+/-- **The bipartition**: the first `q * (3 * k + 2)` vertices, the old ones, are rows; every edge
+joins an old vertex to a subdivision vertex. -/
+theorem isRowsFirstBipartite_explicitBlockNetwork :
+    (machine.explicitBlockNetwork input b σ e).IsRowsFirstBipartite (q * (3 * k + 2)) := by
+  refine TensorNetwork.isRowsFirstBipartite_toExplicit _ _ _ _ fun p => ?_
+  rcases p with p | p <;>
+  simp only [TensorNetwork.subdivide_src_inl, TensorNetwork.subdivide_src_inr,
+    TensorNetwork.subdivide_tgt_inl, TensorNetwork.subdivide_tgt_inr] <;>
+  exact iff_of_true (explicitVertexEquiv_inl _ _ _ _)
+    (not_lt.mpr (le_explicitVertexEquiv_inr _ _ _ _))
+
+/-- **Admissibility at a clock `t`.** With blocks of `b ≤ 3 ⌊log₂ t⌋` steps and padded time
+`q * b ≤ 2 t`, the explicit network is rows-first bipartite with `O(t)` edges and maximum degree
+`O(log t)`, with the constant `6 (3 k + 1) (s + k + 4)` of the machine. For the counting
+simulation, `b = ⌈log₂ (t + 2)⌉` (`Nat.clog_two_add_two_le_three_mul_log_two`). -/
+theorem admissible_explicitBlockNetwork {t : ℕ} (hb : b ≤ 3 * Nat.log 2 t) (hqb : q * b ≤ 2 * t) :
+    (machine.explicitBlockNetwork input b σ e).IsRowsFirstBipartite (q * (3 * k + 2)) ∧
+      (machine.explicitBlockNetwork input b σ e).numEdges ≤ 6 * (3 * k + 1) * (s + k + 4) * t ∧
+      (machine.explicitBlockNetwork input b σ e).maxDegree ≤
+        6 * (3 * k + 1) * (s + k + 4) * Nat.log 2 t := by
+  refine ⟨machine.isRowsFirstBipartite_explicitBlockNetwork input b σ e, ?_, ?_⟩
+  · rw [numEdges_explicitBlockNetwork, letterBits]
+    calc 2 * (q * (3 * k + 1) * ((s + k + 4) * b))
+        = 2 * (3 * k + 1) * (s + k + 4) * (q * b) := by ring
+      _ ≤ 2 * (3 * k + 1) * (s + k + 4) * (2 * t) := Nat.mul_le_mul_left _ hqb
+      _ ≤ 6 * (3 * k + 1) * (s + k + 4) * t := by
+          have h4 : 2 * (3 * k + 1) * (s + k + 4) * (2 * t) =
+              4 * ((3 * k + 1) * (s + k + 4) * t) := by ring
+          have h6 : 6 * (3 * k + 1) * (s + k + 4) * t = 6 * ((3 * k + 1) * (s + k + 4) * t) := by
+            ring
+          omega
+  · refine (machine.maxDegree_explicitBlockNetwork_le input b σ e).trans ?_
+    rw [letterBits]
+    calc 2 * (3 * k + 1) * ((s + k + 4) * b) = 2 * (3 * k + 1) * (s + k + 4) * b := by ring
+      _ ≤ 2 * (3 * k + 1) * (s + k + 4) * (3 * Nat.log 2 t) := Nat.mul_le_mul_left _ hb
+      _ = 6 * (3 * k + 1) * (s + k + 4) * Nat.log 2 t := by ring
+
+/-- Every table of the explicit network lists the values at all bits on its ports. -/
+theorem length_table_explicitBlockNetwork {p : List ℕ × List ℕ}
+    (hp : p ∈ (machine.explicitBlockNetwork input b σ e).vertices) :
+    p.2.length = 2 ^ p.1.length :=
+  TensorNetwork.length_table_toExplicit _ _ _ hp
+
+/-- **The entry bound**: every table entry of the explicit network is at most `2 ^ b`. -/
+theorem entry_le_explicitBlockNetwork {p : List ℕ × List ℕ}
+    (hp : p ∈ (machine.explicitBlockNetwork input b σ e).vertices) {a : ℕ} (ha : a ∈ p.2) :
+    a ≤ 2 ^ b := by
+  obtain ⟨v, y, rfl⟩ := TensorNetwork.exists_tensor_of_mem_toExplicit _ _ _ hp ha
+  have hone : (1 : ℕ) ≤ 2 ^ b := Nat.one_le_two_pow
+  rcases v with v | p
+  · rw [TensorNetwork.subdivide_tensor_inl]
+    rcases TensorNetwork.tensor_binarize_eq_zero_or (machine.blockNetwork input b σ)
+      (letterCode e) v _ with h | ⟨x, h⟩
+    · rw [h]
+      exact Nat.zero_le _
+    · rw [h]
+      exact machine.tensor_blockNetwork_le input b σ v x
+  · rw [TensorNetwork.subdivide_tensor_inr]
+    split_ifs
+    · exact hone
+    · exact Nat.zero_le _
+
+end MultiTapePTM
+
+end Turing
diff --git a/Complexity/Foundations/Data/Nat/Log.lean b/Complexity/Foundations/Data/Nat/Log.lean
index e3387cc1f..5f468fde9 100644
--- a/Complexity/Foundations/Data/Nat/Log.lean
+++ b/Complexity/Foundations/Data/Nat/Log.lean
@@ -31,6 +31,7 @@ stays polynomial after logarithmically many rounds. Similarly `2 ^ (⌊log₂ n
 * `Nat.mul_log_le_add_sq`: `m * ⌊log_b n⌋ ≤ n + m * m` for `1 < b`.
 * `Nat.clog_two_le_two_mul_of_le_two_mul`: `⌈log₂ n⌉ ≤ 2 * ⌈log₂ n'⌉` when `n ≤ 2 * n'` and
   `2 ≤ n'`.
+* `Nat.clog_two_add_two_le_three_mul_log_two`: `⌈log₂ (n + 2)⌉ ≤ 3 ⌊log₂ n⌋` for `n ≥ 2`.
 -/
 
 @[expose] public section
@@ -109,4 +110,14 @@ theorem clog_two_le_two_mul_of_le_two_mul {n n' : ℕ} (hn : n ≤ 2 * n') (hn'
   have h3 : clog 2 n ≤ clog 2 n' + 1 := (clog_le_iff_le_pow Nat.one_lt_two).mpr h2
   omega
 
+/-- From `n = 2` on, `⌈log₂ (n + 2)⌉ ≤ 3 ⌊log₂ n⌋`: the left side is at most `⌊log₂ n⌋ + 2`, and
+`⌊log₂ n⌋ ≥ 1`. -/
+theorem clog_two_add_two_le_three_mul_log_two {n : ℕ} (hn : 2 ≤ n) :
+    clog 2 (n + 2) ≤ 3 * log 2 n := by
+  have hL : 1 ≤ log 2 n := le_log_of_pow_le Nat.one_lt_two (by simpa using hn)
+  have hlt : n < 2 ^ (log 2 n + 1) := lt_pow_succ_log_self Nat.one_lt_two n
+  refine (clog_le_iff_le_pow Nat.one_lt_two).mpr ?_
+  calc n + 2 ≤ 2 ^ (log 2 n + 2) := by rw [Nat.pow_succ]; omega
+    _ ≤ 2 ^ (3 * log 2 n) := Nat.pow_le_pow_right Nat.two_pos (by omega)
+
 end Nat
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean
index 27d867afd..f03082855 100644
--- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit
 public import Mathlib.Data.ZMod.Defs
+public import Mathlib.Logic.Equiv.Fin.Basic
 
 /-!
 # Tests for tensor networks
@@ -90,6 +91,34 @@ example : parallelNetwork.subdivide.contraction = 70 ∧ parallelNetwork.subdivi
     decide
   · exact (Set.ncard_le_card _).trans (by simp)
 
+/-! ### Rows-first bipartitions -/
+
+/-- In `parallel`, the first vertex is a row and the second a column. -/
+example : parallel.IsRowsFirstBipartite 1 := by decide
+
+/-- With both vertices as rows, no edge has a column port. -/
+example : ¬ parallel.IsRowsFirstBipartite 2 := by decide
+
+/-- In the four-cycle the rows `r₀, r₁` are vertices `0` and `2`, not the first two. -/
+example : ¬ (cycle eqTable).IsRowsFirstBipartite 2 := by decide
+
+/-- A port naming no edge is excluded. -/
+example : ¬ (⟨1, [([0], [1, 1]), ([0, 5], [1, 1, 1, 1])]⟩ :
+    ExplicitTensorNetwork ℕ).IsRowsFirstBipartite 1 := by decide
+
+/-- Written out with the old vertices first, the subdivision of `parallelNetwork` is rows-first
+bipartite with degree `2`, both by the general lemmas and by evaluation. -/
+example : (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).IsRowsFirstBipartite
+      2 ∧ (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).maxDegree ≤ 2 :=
+  ⟨parallelNetwork.subdivide.isRowsFirstBipartite_toExplicit _ _ 2 (by decide),
+    parallelNetwork.subdivide.maxDegree_toExplicit_le _ _
+      (parallelNetwork.maxDegreeLE_subdivide (fun e => by simp [parallelNetwork])
+        (fun v => (Set.ncard_le_card _).trans (by simp)) le_rfl)⟩
+
+example : (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).IsRowsFirstBipartite
+      2 ∧ (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).maxDegree = 2 := by
+  decide
+
 /-! ### Constraint networks -/
 
 /-- Two vertices joined by two parallel edges, each requiring its two edges to agree. -/
diff --git a/ComplexityTests/HPVExplicitBlockNetwork.lean b/ComplexityTests/HPVExplicitBlockNetwork.lean
new file mode 100644
index 000000000..eb3e8ac2b
--- /dev/null
+++ b/ComplexityTests/HPVExplicitBlockNetwork.lean
@@ -0,0 +1,99 @@
+/-
+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
+import Complexity.Foundations.Data.Nat.Log
+
+/-! Explicit block-counting networks of concrete fair-coin machines: the letter numbering on
+concrete letters, the counting identity, and the size, degree and bipartition of the networks. -/
+
+namespace ComplexityTests.HPVExplicitBlockNetwork
+
+open Turing MultiTapeMachine MultiTapePTM 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
+
+/-- On one work tape, write every coin and move right. The first step emits its coin; then the
+machine keeps walking without output. -/
+private def walk : MultiTapePTM 1 Bool Bool where
+  initial := false
+  tr state _ _ _ bit := .step
+    { inputTape := 1,
+      workTapes := fun _ => (some (some bit), 1),
+      output := if state then none else some bit, state := some true }
+    Empty.elim Empty.elim
+
+/-! ### The letter numbering -/
+
+/-- With two states, one work tape and blocks of two cells, there are
+`3 * (2 ^ 2 * 3) = 36` control records, numbered first. The block holding `true` twice is
+contents number `2 + 2 * 3 = 8`, so letter number `44`. -/
+example : (letterEquiv (k := 1) (b := 2) finTwoEquiv.symm (.inr fun _ => some true) : ℕ) = 44 :=
+  by decide
+
+/-- The record of state `true` with both offsets `1` and output track `accept`: state digit `2`,
+offset digits `1 + 1 * 2 = 3`, track digit `1`, so number `2 * 12 + (3 * 3 + 1) = 34`. -/
+example : (letterEquiv (k := 1) (b := 2) finTwoEquiv.symm
+    (.inl (some true, fun _ => 1, .accept)) : ℕ) = 34 := by decide
+
+/-- The code of letter `44 = 0b101100` in `(2 + 1 + 4) * 2 = 14` bits, least significant first. -/
+example : List.ofFn (letterCode (k := 1) (b := 2) finTwoEquiv.symm (.inr fun _ => some true)) =
+    [false, false, true, true, false, true, false, false, false, false, false, false, false,
+      false] := by decide
+
+/-! ### The counting identity -/
+
+-- One interval of two bits: the strings starting with `true` accept.
+example : ∑ σ : Schedule 0 1,
+    (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).contraction = 2 := by
+  rw [sum_contraction_explicitBlockNetwork _ _ _ _ one_pos,
+    show emitCoin.acceptCount [] (1 * 2) = 2 by decide]
+
+-- Two intervals of two bits, with windows on the work tape: half of the `16` strings accept.
+example : ∑ σ : Schedule 1 2,
+    (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).contraction = 8 := by
+  rw [sum_contraction_explicitBlockNetwork _ _ _ _ two_pos,
+    show walk.acceptCount [true] (2 * 2) = 8 by decide]
+
+/-! ### Size, degree and bipartition -/
+
+-- Letters of `14` bits; `2 * (2 * 4 * 14) = 224` edges; `10` old vertices and `112` subdivision
+-- vertices; degree at most `2 * 4 * 14 = 112`; the `10` old vertices are the rows; every table has
+-- an entry for each list of bits on its ports, and every entry is at most `2 ^ 2`.
+example (σ : Schedule 1 2) :
+    letterBits 1 2 2 = 14 ∧
+      (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).numEdges = 224 ∧
+      (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).vertices.length = 122 ∧
+      (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).maxDegree ≤ 112 ∧
+      (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).IsRowsFirstBipartite 10 ∧
+      ∀ p ∈ (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).vertices,
+        p.2.length = 2 ^ p.1.length ∧ ∀ a ∈ p.2, a ≤ 4 :=
+  ⟨rfl, numEdges_explicitBlockNetwork .., length_vertices_explicitBlockNetwork ..,
+    maxDegree_explicitBlockNetwork_le .., isRowsFirstBipartite_explicitBlockNetwork ..,
+    fun _ hp => ⟨length_table_explicitBlockNetwork _ _ _ _ _ hp,
+      fun _ ha => entry_le_explicitBlockNetwork _ _ _ _ _ hp ha⟩⟩
+
+-- At the clock `t = 2`, blocks of `⌈log₂ 4⌉ = 2` steps and one interval: the network of
+-- `emitCoin` is rows-first bipartite with at most `6 * 1 * 5 * 2 = 60` edges (it has
+-- `2 * (1 * 1 * 10) = 20`) and degree at most `6 * 1 * 5 * ⌊log₂ 2⌋ = 30`.
+example (σ : Schedule 0 1) :
+    (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).IsRowsFirstBipartite 2 ∧
+      (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).numEdges ≤ 60 ∧
+      (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).maxDegree ≤ 30 := by
+  have hb : 2 ≤ 3 * Nat.log 2 2 := by
+    simpa [show Nat.clog 2 (2 + 2) = 2 by decide] using
+      Nat.clog_two_add_two_le_three_mul_log_two (le_refl 2)
+  have h := emitCoin.admissible_explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1)) hb
+    (by norm_num)
+  rw [show Nat.log 2 2 = 1 by decide] at h
+  simpa using h
+
+end ComplexityTests.HPVExplicitBlockNetwork