diff --git a/Complexity.lean b/Complexity.lean
index 82d05da562..d94a033e1a 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1015,6 +1015,9 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContra
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionShape
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSize
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetwork
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetworkBounds
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetworkSize
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.KernelProduct
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation
@@ -3224,6 +3227,7 @@ public import Complexity.Foundations.Data.Int.Residue
 public import Complexity.Foundations.Data.List.Append
 public import Complexity.Foundations.Data.List.BalancedFold
 public import Complexity.Foundations.Data.List.Basic
+public import Complexity.Foundations.Data.List.Blocks
 public import Complexity.Foundations.Data.List.Boole
 public import Complexity.Foundations.Data.List.Counting
 public import Complexity.Foundations.Data.List.Equiv
@@ -3272,9 +3276,11 @@ public import Complexity.Foundations.Data.Nat.Bitwise.Sparse
 public import Complexity.Foundations.Data.Nat.Bitwise.SumTree
 public import Complexity.Foundations.Data.Nat.Card
 public import Complexity.Foundations.Data.Nat.CeilDiv
+public import Complexity.Foundations.Data.Nat.CeilQuarter
 public import Complexity.Foundations.Data.Nat.Choose
 public import Complexity.Foundations.Data.Nat.Choose.Central
 public import Complexity.Foundations.Data.Nat.Choose.Real
+public import Complexity.Foundations.Data.Nat.Choose.Vandermonde
 public import Complexity.Foundations.Data.Nat.Div
 public import Complexity.Foundations.Data.Nat.Doubling
 public import Complexity.Foundations.Data.Nat.Factorial
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean
index eeeb0d4397..38f43fa4c3 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean
@@ -147,6 +147,14 @@ theorem le_ceilNineTenths_iff {s x : ℕ} (hs : 1 ≤ s) :
     have h2 := (pow_nine_le_ceilNineTenths_pow_ten s).trans (Nat.pow_le_pow_left h1 10)
     omega
 
+/-- `x ≤ ⌈s ^ (9/10)⌉` whenever `x ^ 10 ≤ s ^ 9` and `s ≥ 1`. -/
+theorem le_ceilNineTenths_of_pow_le {x s : ℕ} (hs : 1 ≤ s) (h : x ^ 10 ≤ s ^ 9) :
+    x ≤ ceilNineTenths s := by
+  rw [le_ceilNineTenths_iff hs]
+  rcases Nat.eq_zero_or_pos x with rfl | hx
+  · simpa using Nat.pow_pos (n := 9) hs
+  · exact (Nat.pow_lt_pow_left (by omega) (by norm_num)).trans_le h
+
 /-- `⌈s ^ (9/10)⌉ ≤ s`. -/
 theorem ceilNineTenths_le_self (s : ℕ) : ceilNineTenths s ≤ s :=
   ceilNineTenths_le (pow_nine_le_pow_ten_self s)
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetwork.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetwork.lean
new file mode 100644
index 0000000000..eaa398dc8a
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetwork.lean
@@ -0,0 +1,385 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit
+public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile
+public import Complexity.Foundations.Data.List.Blocks
+import Complexity.Foundations.Data.List.OfFn
+
+/-!
+# The incidence network of Lemma D.2
+
+Lemma D.2 of [OpenAI2026ETH] (pp. 54–56) counts the common zeros of a sparse polynomial system
+over `𝔽₂` by contracting, for each *degree array*, a bipartite Boolean tensor network whose wires
+index the monomials of the incidence polynomial. This file builds that network as a described
+network (`DescribedNetwork`) and proves its shape: it is rows-first bipartite, and its edges,
+vertices and ports are counted. The entries of its vertices, their native evaluation, the wire
+bound (D.3) and the contraction are separate.
+
+**The system.** A system on `n` variables is a list `sys` of equations, each a list of monomials,
+each a list of variable indices (the representation of `Cslib.Complexity.evalSystem`). The *scope*
+of test `i` is `equationVars sys[i]`, its variables in increasing order without repetition, and an
+*incidence* is a pair of a test and a variable of its scope.
+
+**Groups and arrays** (p. 55). The tests and the variables are split separately into `J` groups by
+their residues modulo `J` (`List.residueClass`), so that group sizes differ by at most one. The
+incidences between test group `g` and variable group `h` are listed by `pairInc J sys g h`, as
+pairs of the position of the test in its group and the variable. A *degree array* is a list `d`
+whose entry `g J + h` is the number `d_gh` of selected incidences of the pair `(g, h)`. It is *live*
+(`live`) when its entries below `J²` sum to at most `K`; this is the paper's bound
+`Σ d_gh ≤ K`.
+
+**Index wires** (p. 55). The pair `(g, h)` gets `⌈log₂ C_gh⌉` wires (`width`), where
+`C_gh = C(N_gh, d_gh)` is the number of subsets of size `d_gh` of its `N_gh` incidences; the bits on
+them index such a subset. The wires of the `J²` pairs are numbered consecutively in the order
+`g J + h` (`List.blockStart`, `List.blockRange`), and there are `numWires` of them. Test group `g`
+is a row whose ports are the wires of the pairs `(g, 0), …, (g, J - 1)` in order (`rowPorts`), and
+variable group `h` is a column whose ports are those of `(0, h), …, (J - 1, h)` (`colPorts`).
+
+**Descriptors** (`Desc`). A row carries the precision `P`, the truncation order `ℓ`, the monomials
+of the tests of its group and, for each variable group, the incidences of the pair and their
+selected number. A column carries `P`, the variables of its group and the same lists for each test
+group. A fixed table, read as in an explicit network, describes the other vertices.
+
+**Padding and dead arrays** (`network`). Theorem D.1 is applied at a size `s`, and its interface
+asks for at least `s` edges (`Cslib.Circuits.Frontier.EntryAdmissible`). The network adds
+`s - M` disjoint edges, `M` the number of index wires, each with a row whose table `[1, 0]` is
+`[x = 0]` and a column whose table `[1, 1]` is the constant one; they leave the contraction
+unchanged. A dead array (not live) gets only the `s` padding edges and one isolated row with the
+table `[0]`, so its contraction is zero; the loop of Lemma D.2 can then sum over all arrays
+without a validity test.
+
+## Main definitions
+
+* `Cslib.Circuits.Frontier.IncidenceNetwork.pairInc`: the incidences of a pair of groups.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.width`: the number of index wires of a pair.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.live`: the arrays with `Σ d_gh ≤ K`.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.Desc`: the descriptors.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.network`: the network of an array, with its number of
+  rows.
+
+## Main results
+
+* `Cslib.Circuits.Frontier.IncidenceNetwork.flatMap_rowPorts`: the ports of the rows are the
+  index wires.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.isRowsFirstBipartite_network`: the network is
+  rows-first bipartite.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.numEdges_network`: it has `max M s` edges.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.length_vertices_network`: it has `2 J + 2 (s - M)`
+  vertices when live, and `1 + 2 s` when dead.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.length_rowPorts`,
+  `Cslib.Circuits.Frontier.IncidenceNetwork.length_colPorts`: the degrees of the group vertices.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.2 (pp. 54–56).
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier.IncidenceNetwork
+
+open Cslib.Complexity
+
+/-! ### Groups and incidences -/
+
+/-- **The incidences of the pair `(g, h)`**: for each test of group `g`, in order, the pairs
+`(t, v)` of its position `t` in the group and a variable `v` of its scope in group `h`, in
+increasing order. -/
+@[expose] def pairInc (J : ℕ) (sys : List (List (List ℕ))) (g h : ℕ) : List (ℕ × ℕ) :=
+  (List.residueClass J sys.length g).zipIdx.flatMap fun p =>
+    ((equationVars (sys.getD p.1 [])).filter (· % J = h)).map fun v => (p.2, v)
+
+/-- **The number of index wires of the pair `(g, h)`** for the array `d`: `⌈log₂ C(N_gh, d_gh)⌉`,
+where `N_gh` is the number of incidences of the pair and `d_gh` the entry `g J + h` of `d`. -/
+@[expose] def width (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (g h : ℕ) : ℕ :=
+  Nat.clog 2 ((pairInc J sys g h).length.choose (d.getD (g * J + h) 0))
+
+/-- The number of index wires of block `b`, the pair `(b / J, b % J)`. -/
+@[expose] def blockWidth (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (b : ℕ) : ℕ :=
+  width J sys d (b / J) (b % J)
+
+/-- The number of index wires of all `J²` pairs. -/
+@[expose] def numWires (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) : ℕ :=
+  List.blockStart (blockWidth J sys d) (J * J)
+
+/-- **The ports of test group `g`**: the wires of the pairs `(g, 0), …, (g, J - 1)`. -/
+@[expose] def rowPorts (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (g : ℕ) : List ℕ :=
+  (List.range J).flatMap fun h => List.blockRange (blockWidth J sys d) (g * J + h)
+
+/-- **The ports of variable group `h`**: the wires of the pairs `(0, h), …, (J - 1, h)`. -/
+@[expose] def colPorts (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (h : ℕ) : List ℕ :=
+  (List.range J).flatMap fun g => List.blockRange (blockWidth J sys d) (g * J + h)
+
+/-- **Live arrays**: the entries of `d` below `J²` sum to at most `K`. -/
+@[expose] def live (J K : ℕ) (d : List ℕ) : Bool :=
+  decide (((List.range (J * J)).map (d.getD · 0)).sum ≤ K)
+
+/-! ### Descriptors and the network -/
+
+/-- A block of a group vertex: the incidences of a pair of groups and their selected number. -/
+abbrev Block : Type := List (ℕ × ℕ) × ℕ
+
+/-- **The descriptor of a vertex**: a test group (`inl`: the precision `P`, the truncation order
+`ℓ`, the monomials of its tests and its blocks), a variable group (`inr (inl …)`: the precision,
+its variables and its blocks), or a fixed table (`inr (inr …)`), read as in an explicit network. -/
+abbrev Desc : Type :=
+  (ℕ × ℕ × List (List (List ℕ)) × List Block) ⊕ (ℕ × List ℕ × List Block) ⊕ List ℕ
+
+/-- The blocks of test group `g`: the pairs `(g, 0), …, (g, J - 1)`. -/
+@[expose] def rowBlocks (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (g : ℕ) :
+    List Block :=
+  (List.range J).map fun h => (pairInc J sys g h, d.getD (g * J + h) 0)
+
+/-- The blocks of variable group `h`: the pairs `(0, h), …, (J - 1, h)`. -/
+@[expose] def colBlocks (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (h : ℕ) :
+    List Block :=
+  (List.range J).map fun g => (pairInc J sys g h, d.getD (g * J + h) 0)
+
+/-- The vertex of test group `g`. -/
+@[expose] def rowVertex (P ℓ J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (g : ℕ) :
+    List ℕ × Desc :=
+  (rowPorts J sys d g, .inl (P, ℓ, (List.residueClass J sys.length g).map (sys.getD · []),
+    rowBlocks J sys d g))
+
+/-- The vertex of variable group `h` among `n` variables. -/
+@[expose] def colVertex (P J n : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) (h : ℕ) :
+    List ℕ × Desc :=
+  (colPorts J sys d h, .inr (.inl (P, List.residueClass J n h, colBlocks J sys d h)))
+
+/-- The padding row on edge `e`: the table `[1, 0]`, that is `[x = 0]`. -/
+@[expose] def padRow (e : ℕ) : List ℕ × Desc := ([e], .inr (.inr [1, 0]))
+
+/-- The padding column on edge `e`: the table `[1, 1]`, the constant one. -/
+@[expose] def padCol (e : ℕ) : List ℕ × Desc := ([e], .inr (.inr [1, 1]))
+
+/-- The isolated row of a dead array: the table `[0]`. -/
+@[expose] def deadRow : List ℕ × Desc := ([], .inr (.inr [0]))
+
+/-- The number of index wires of the network: `numWires` for a live array, none for a dead one. -/
+@[expose] def mainWires (J K : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) : ℕ :=
+  if live J K d then numWires J sys d else 0
+
+/-- The rows of the network: the test groups for a live array, or the isolated row for a dead
+one, then the padding rows. -/
+@[expose] def rows (P ℓ J K s : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) :
+    List (List ℕ × Desc) :=
+  (if live J K d then (List.range J).map (rowVertex P ℓ J sys d) else [deadRow]) ++
+    (List.range (s - mainWires J K sys d)).map fun e => padRow (mainWires J K sys d + e)
+
+/-- The columns of the network: the variable groups for a live array, then the padding
+columns. -/
+@[expose] def cols (P J K s n : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) :
+    List (List ℕ × Desc) :=
+  (if live J K d then (List.range J).map (colVertex P J n sys d) else []) ++
+    (List.range (s - mainWires J K sys d)).map fun e => padCol (mainWires J K sys d + e)
+
+/-- **The incidence network of the array `d`** (Lemma D.2, pp. 55–56), with its number of rows:
+for `J` groups, degree cap `K`, size `s`, precision `P`, truncation order `ℓ`, and the system `sys`
+on `n` variables. A live array gets the index wires and the group vertices; every array gets
+padding up to `s` edges. -/
+@[expose] def network (P ℓ J K s n : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) :
+    ℕ × DescribedNetwork Desc :=
+  ((rows P ℓ J K s sys d).length,
+    ⟨mainWires J K sys d + (s - mainWires J K sys d),
+      rows P ℓ J K s sys d ++ cols P J K s n sys d⟩)
+
+/-! ### Counting ports -/
+
+variable {J : ℕ} {sys : List (List (List ℕ))} {d : List ℕ}
+
+/-- The block of the pair `(g, h)` has the index wires of the pair. -/
+theorem blockWidth_mul_add {g h : ℕ} (hh : h < J) :
+    blockWidth J sys d (g * J + h) = width J sys d g h := by
+  have hJ : 0 < J := by omega
+  rw [blockWidth, Nat.add_comm, Nat.add_mul_div_right _ _ hJ, Nat.add_mul_mod_self_right,
+    Nat.div_eq_of_lt hh, Nat.mod_eq_of_lt hh, Nat.zero_add]
+
+/-- The ports of all test groups, in order, are the index wires. -/
+theorem flatMap_rowPorts (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) :
+    (List.range J).flatMap (rowPorts J sys d) = List.range (numWires J sys d) := by
+  have h := congrArg (List.flatMap (List.blockRange (blockWidth J sys d)))
+    (List.flatMap_range_mul J J)
+  rw [List.flatMap_assoc, List.flatMap_blockRange] at h
+  rw [numWires, ← h]
+  simp only [List.flatMap_map]
+  rfl
+
+/-- The number of times a number is a port of the test groups: once if it is an index wire. -/
+theorem sum_count_rowPorts (i : ℕ) :
+    ((List.range J).map fun g => (rowPorts J sys d g).count i).sum =
+      if i < numWires J sys d then 1 else 0 := by
+  have h := congrArg (List.count i) (flatMap_rowPorts J sys d)
+  rw [List.count_flatMap, List.count_range] at h
+  simpa [Function.comp_def] using h
+
+/-- The number of times a number is a port of the variable groups: once if it is an index wire. -/
+theorem sum_count_colPorts (i : ℕ) :
+    ((List.range J).map fun h => (colPorts J sys d h).count i).sum =
+      if i < numWires J sys d then 1 else 0 := by
+  rw [← sum_count_rowPorts]
+  simp only [rowPorts, colPorts, List.count_flatMap, List.sum_map_range_eq_sum_range,
+    Function.comp_def]
+  exact Finset.sum_comm
+
+/-- A port of a test group `g < J` is an index wire. -/
+theorem lt_of_mem_rowPorts {g i : ℕ} (hg : g < J) (hi : i ∈ rowPorts J sys d g) :
+    i < numWires J sys d := by
+  have : i ∈ (List.range J).flatMap (rowPorts J sys d) :=
+    List.mem_flatMap.mpr ⟨g, List.mem_range.mpr hg, hi⟩
+  rw [flatMap_rowPorts] at this
+  exact List.mem_range.mp this
+
+/-- A port of a variable group `h < J` is an index wire. -/
+theorem lt_of_mem_colPorts {h i : ℕ} (hh : h < J) (hi : i ∈ colPorts J sys d h) :
+    i < numWires J sys d := by
+  have hc : 0 < (colPorts J sys d h).count i := List.count_pos_iff.mpr hi
+  have h1 := sum_count_colPorts (J := J) (sys := sys) (d := d) i
+  have h2 : (colPorts J sys d h).count i ≤
+      ((List.range J).map fun h => (colPorts J sys d h).count i).sum :=
+    List.le_sum_of_mem (List.mem_map.mpr ⟨h, List.mem_range.mpr hh, rfl⟩)
+  by_contra hn
+  rw [ite_eq_right hn] at h1
+  omega
+
+/-- **The degree of a test group** `g`: the index wires of its pairs. -/
+theorem length_rowPorts (g : ℕ) :
+    (rowPorts J sys d g).length = ∑ h ∈ Finset.range J, width J sys d g h := by
+  rw [rowPorts, List.length_flatMap, List.sum_map_range_eq_sum_range]
+  exact Finset.sum_congr rfl fun h hh => by
+    rw [List.blockRange, List.length_range', blockWidth_mul_add (Finset.mem_range.mp hh)]
+
+/-- **The degree of a variable group** `h`: the index wires of its pairs. -/
+theorem length_colPorts (h : ℕ) (hh : h < J) :
+    (colPorts J sys d h).length = ∑ g ∈ Finset.range J, width J sys d g h := by
+  rw [colPorts, List.length_flatMap, List.sum_map_range_eq_sum_range]
+  exact Finset.sum_congr rfl fun g _ => by
+    rw [List.blockRange, List.length_range', blockWidth_mul_add hh]
+
+/-- **The number of index wires** is the sum over the pairs. -/
+theorem numWires_eq (J : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) :
+    numWires J sys d = ∑ g ∈ Finset.range J, ∑ h ∈ Finset.range J, width J sys d g h := by
+  have h := congrArg List.length (flatMap_rowPorts J sys d)
+  rw [List.length_range, List.length_flatMap, List.sum_map_range_eq_sum_range] at h
+  rw [← h]
+  exact Finset.sum_congr rfl fun g _ => length_rowPorts g
+
+/-! ### The shape of the network -/
+
+variable {P ℓ K s n : ℕ}
+
+/-- The padding edges `M, …, M + q - 1`, one per padding vertex, in order. -/
+private theorem sum_count_pad (M q i : ℕ) (f : ℕ → List ℕ × Desc) (hf : ∀ e, (f e).1 = [e]) :
+    ((List.range q).map fun e => (f (M + e)).1.count i).sum =
+      if M ≤ i ∧ i < M + q then 1 else 0 := by
+  induction q with
+  | zero => simp
+  | succ q ih =>
+    rw [List.range_succ, List.map_append, List.sum_append, ih, List.map_singleton,
+      List.sum_singleton, hf, List.count_singleton]
+    split_ifs <;> simp_all <;> omega
+
+/-- The number of rows. -/
+theorem fst_network : (network P ℓ J K s n sys d).1 = (rows P ℓ J K s sys d).length := rfl
+
+/-- **The network has `max M s` edges**, for `M` its index wires: at least `s`. -/
+theorem numEdges_network :
+    (network P ℓ J K s n sys d).2.numEdges = max (mainWires J K sys d) s := by
+  change mainWires J K sys d + (s - mainWires J K sys d) = _
+  omega
+
+/-- The number of rows: `J` or one, plus the padding. -/
+theorem length_rows :
+    (rows P ℓ J K s sys d).length =
+      (if live J K d then J else 1) + (s - mainWires J K sys d) := by
+  unfold rows
+  split_ifs <;> simp [Nat.add_comm]
+
+/-- The number of columns: `J` or none, plus the padding. -/
+theorem length_cols :
+    (cols P J K s n sys d).length =
+      (if live J K d then J else 0) + (s - mainWires J K sys d) := by
+  unfold cols
+  split_ifs <;> simp [Nat.add_comm]
+
+/-- **The number of vertices**: `2 J + 2 (s - M)` for a live array, `1 + 2 s` for a dead one. -/
+theorem length_vertices_network :
+    (network P ℓ J K s n sys d).2.vertices.length =
+      (if live J K d then 2 * J else 1) + 2 * (s - mainWires J K sys d) := by
+  change (rows P ℓ J K s sys d ++ cols P J K s n sys d).length = _
+  rw [List.length_append, length_rows, length_cols]
+  split_ifs <;> omega
+
+/-- **The network is rows-first bipartite**: every port is an edge, and every edge is a port of
+exactly one row and of exactly one column. -/
+theorem isRowsFirstBipartite_network :
+    (network P ℓ J K s n sys d).2.IsRowsFirstBipartite (network P ℓ J K s n sys d).1 := by
+  set M := mainWires J K sys d with hM
+  have hv : (network P ℓ J K s n sys d).2.vertices =
+      rows P ℓ J K s sys d ++ cols P J K s n sys d := rfl
+  have hE : (network P ℓ J K s n sys d).2.numEdges = M + (s - M) := rfl
+  rw [fst_network]
+  unfold DescribedNetwork.IsRowsFirstBipartite
+  rw [hv, hE, List.take_left, List.drop_left]
+  refine ⟨fun v hv i hi => ?_, fun i hi => ⟨?_, ?_⟩⟩
+  · -- Every port names an edge.
+    rcases List.mem_append.mp hv with hv | hv
+    · rcases List.mem_append.mp hv with hv | hv
+      · by_cases hl : live J K d
+        · rw [ite_eq_left hl] at hv
+          obtain ⟨g, hg, rfl⟩ := List.mem_map.mp hv
+          have := lt_of_mem_rowPorts (List.mem_range.mp hg) hi
+          rw [hM, mainWires, ite_eq_left hl]
+          omega
+        · rw [ite_eq_right hl] at hv
+          rw [List.mem_singleton.mp hv] at hi
+          simp [deadRow] at hi
+      · obtain ⟨e, he, rfl⟩ := List.mem_map.mp hv
+        rw [List.mem_range] at he
+        simp only [padRow, List.mem_singleton] at hi
+        omega
+    · rcases List.mem_append.mp hv with hv | hv
+      · by_cases hl : live J K d
+        · rw [ite_eq_left hl] at hv
+          obtain ⟨h, hh, rfl⟩ := List.mem_map.mp hv
+          have := lt_of_mem_colPorts (List.mem_range.mp hh) hi
+          rw [hM, mainWires, ite_eq_left hl]
+          omega
+        · rw [ite_eq_right hl] at hv
+          simp at hv
+      · obtain ⟨e, he, rfl⟩ := List.mem_map.mp hv
+        rw [List.mem_range] at he
+        simp only [padCol, List.mem_singleton] at hi
+        omega
+  · -- Exactly one row.
+    rw [rows, List.map_append, List.sum_append, List.map_map]
+    simp only [Function.comp_def]
+    rw [sum_count_pad M (s - M) i padRow fun _ => rfl]
+    by_cases hl : live J K d
+    · simp only [ite_eq_left hl, List.map_map, Function.comp_def, rowVertex]
+      rw [sum_count_rowPorts]
+      have : M = numWires J sys d := by rw [hM, mainWires, ite_eq_left hl]
+      split_ifs <;> omega
+    · simp only [ite_eq_right hl, List.map_singleton, deadRow, List.count_nil, List.sum_singleton]
+      have : M = 0 := by rw [hM, mainWires, ite_eq_right hl]
+      split_ifs <;> omega
+  · -- Exactly one column.
+    rw [cols, List.map_append, List.sum_append, List.map_map]
+    simp only [Function.comp_def]
+    rw [sum_count_pad M (s - M) i padCol fun _ => rfl]
+    by_cases hl : live J K d
+    · simp only [ite_eq_left hl, List.map_map, Function.comp_def, colVertex]
+      rw [sum_count_colPorts]
+      have : M = numWires J sys d := by rw [hM, mainWires, ite_eq_left hl]
+      split_ifs <;> omega
+    · simp only [ite_eq_right hl, List.map_nil, List.sum_nil]
+      have : M = 0 := by rw [hM, mainWires, ite_eq_right hl]
+      split_ifs <;> omega
+
+end Cslib.Circuits.Frontier.IncidenceNetwork
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetworkBounds.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetworkBounds.lean
new file mode 100644
index 0000000000..6f152c1ba2
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetworkBounds.lean
@@ -0,0 +1,245 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetwork
+public import Complexity.Foundations.Data.Nat.Choose.Vandermonde
+import Mathlib.Data.List.GetD
+import Mathlib.Data.Nat.Choose.Bounds
+
+/-!
+# Degrees and the wire bound (D.3) of the incidence network
+
+Bounds on the incidence network of Lemma D.2 of [OpenAI2026ETH]
+(`Cslib.Circuits.Frontier.IncidenceNetwork.network`), in terms of the system: the degrees of the
+group vertices (pp. 55–56) and the number of index wires (D.3) (p. 56).
+
+**Degrees.** The pair `(g, h)` has at most as many index wires as incidences, since
+`C(N, d) ≤ 2 ^ N` (`IncidenceNetwork.width_le`). So a test group has at most as many ports as the
+incidences of its tests, at most `(a / J + 1) S` if every scope has at most `S` variables
+(`IncidenceNetwork.length_rowPorts_le`), and a variable group at most `(n / J + 1) D` if every
+variable lies in at most `D` scopes (`IncidenceNetwork.length_colPorts_le`). These are the
+paper's bounds `n ^ (3/4) λ ^ O(1)` at `J = ⌈n ^ (1/4)⌉`.
+
+**Wires** (D.3). With `N` incidences in all (`IncidenceNetwork.numInc`), a live array has
+`2 ^ M ≤ 2 ^ (J²) C(N + K, K)` for its `M` index wires (`IncidenceNetwork.two_pow_numWires_le`):
+`⌈log₂ C⌉ < log₂ C + 1`, and the subsets of the pairs together form one subset of size at most
+`K` of the `N` incidences, which the paper bounds by stars and bars. When `N + K ≤ R K`,
+`C(N + K, K) ≤ (3 R) ^ K` (`IncidenceNetwork.choose_add_le_pow`, from `K ^ K ≤ 3 ^ K K!`), so
+`M ≤ J² + K ⌈log₂ (3 R)⌉` (`IncidenceNetwork.numWires_le`). This is (D.3) in the form
+`J² + K log₂ (e (N + K) / K)` with `e` replaced by `3`.
+
+## Main definitions
+
+* `Cslib.Circuits.Frontier.IncidenceNetwork.numInc`: the number of incidences.
+
+## Main results
+
+* `Cslib.Circuits.Frontier.IncidenceNetwork.length_rowPorts_le`,
+  `Cslib.Circuits.Frontier.IncidenceNetwork.length_colPorts_le`: the degrees.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.two_pow_numWires_le`,
+  `Cslib.Circuits.Frontier.IncidenceNetwork.numWires_le`: the wire bound (D.3).
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.2 (pp. 54–56).
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier.IncidenceNetwork
+
+open Cslib.Complexity Finset
+
+/-- **The number of incidences** of a system: the sum of the sizes of the scopes. -/
+@[expose] def numInc (sys : List (List (List ℕ))) : ℕ :=
+  (sys.map fun eq => (equationVars eq).length).sum
+
+/-! ### Incidences -/
+
+variable {J : ℕ} {sys : List (List (List ℕ))} {d : List ℕ}
+
+/-- **A pair has at most as many index wires as incidences**: `C(N, d) ≤ 2 ^ N`. -/
+theorem width_le (g h : ℕ) : width J sys d g h ≤ (pairInc J sys g h).length :=
+  Nat.clog_le_of_le_pow (Nat.choose_le_two_pow _ _)
+
+/-- The incidences of a pair, test by test. -/
+theorem length_pairInc (g h : ℕ) :
+    (pairInc J sys g h).length = ((List.residueClass J sys.length g).map fun i =>
+      ((equationVars (sys.getD i [])).filter (· % J = h)).length).sum := by
+  rw [pairInc, List.length_flatMap]
+  conv_rhs => rw [← List.zipIdx_map_fst 0 (List.residueClass J sys.length g), List.map_map]
+  simp [Function.comp_def]
+
+/-- **The incidences of a test group** are those of its tests. -/
+theorem sum_length_pairInc_row (hJ : 0 < J) (g : ℕ) :
+    ∑ h ∈ range J, (pairInc J sys g h).length =
+      ((List.residueClass J sys.length g).map fun i =>
+        (equationVars (sys.getD i [])).length).sum := by
+  simp only [length_pairInc]
+  rw [Finset.sum_list_sum_comm]
+  simp only [List.sum_length_filter_mod hJ]
+
+
+/-- **The incidences of all pairs** are the incidences of the system. -/
+theorem sum_sum_length_pairInc (hJ : 0 < J) :
+    ∑ g ∈ range J, ∑ h ∈ range J, (pairInc J sys g h).length = numInc sys := by
+  rw [Finset.sum_congr rfl fun g _ => sum_length_pairInc_row hJ g, List.sum_residueClass hJ, numInc]
+  conv_rhs => rw [← List.map_getD_range sys []]
+  rw [List.map_map]
+  rfl
+
+/-- **The incidences of a variable group**, test by test. -/
+theorem sum_length_pairInc_col (hJ : 0 < J) (h : ℕ) :
+    ∑ g ∈ range J, (pairInc J sys g h).length = ((List.range sys.length).map fun i =>
+      ((equationVars (sys.getD i [])).filter (· % J = h)).length).sum := by
+  simp only [length_pairInc]
+  exact List.sum_residueClass hJ _ _
+
+/-! ### Degrees -/
+
+/-- **The degree of a test group**: at most `(a / J + 1) S` for `a` tests, if every scope has at
+most `S` variables. -/
+theorem length_rowPorts_le (hJ : 0 < J) (g : ℕ) {S : ℕ}
+    (hS : ∀ eq ∈ sys, (equationVars eq).length ≤ S) :
+    (rowPorts J sys d g).length ≤ (sys.length / J + 1) * S := by
+  rw [length_rowPorts]
+  calc ∑ h ∈ range J, width J sys d g h ≤ ∑ h ∈ range J, (pairInc J sys g h).length :=
+        Finset.sum_le_sum fun h _ => width_le g h
+    _ = ((List.residueClass J sys.length g).map fun i =>
+          (equationVars (sys.getD i [])).length).sum :=
+        sum_length_pairInc_row hJ g
+    _ ≤ (List.residueClass J sys.length g).length * S := by
+        refine (List.sum_le_length_nsmul _ S fun x hx => ?_).trans (by simp)
+        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hx
+        have hi' : i < sys.length := List.mem_range.mp (List.mem_filter.mp hi).1
+        rw [List.getD_eq_getElem _ _ hi']
+        exact hS _ (List.getElem_mem hi')
+    _ ≤ (sys.length / J + 1) * S :=
+        Nat.mul_le_mul_right _ (List.length_residueClass_le J sys.length g)
+
+/-- The number of scopes containing a variable, as a sum over the tests. -/
+theorem varDegree_eq_sum (v : ℕ) :
+    varDegree v sys = ((List.range sys.length).map fun i =>
+      if v ∈ equationVars (sys.getD i []) then 1 else 0).sum := by
+  rw [varDegree]
+  conv_lhs => rw [← List.map_getD_range sys []]
+  rw [List.countP_map, List.countP_eq_length_filter, List.length_filter_eq_sum]
+  simp
+
+/-- **The degree of a variable group** `h < J`: at most `(n / J + 1) D` if every variable is
+below `n` and lies in at most `D` scopes. -/
+theorem length_colPorts_le (hJ : 0 < J) {h : ℕ} (hh : h < J) {n D : ℕ}
+    (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hD : ∀ v < n, varDegree v sys ≤ D) :
+    (colPorts J sys d h).length ≤ (n / J + 1) * D := by
+  rw [length_colPorts h hh]
+  -- Per test, the scope variables in group `h` are the variables of group `h` in the scope.
+  have hper : ∀ i < sys.length, ((equationVars (sys.getD i [])).filter (· % J = h)).length =
+      ((List.residueClass J n h).filter fun v => v ∈ equationVars (sys.getD i [])).length := by
+    intro i hi
+    refine List.Perm.length_eq ((List.perm_ext_iff_of_nodup ((nodup_sortDedup _).filter _)
+      (((List.nodup_range).filter _).filter _)).mpr fun v => ?_)
+    have hm : v ∈ equationVars (sys.getD i []) → v < n := fun hv => by
+      obtain ⟨m, hm, hvm⟩ := mem_equationVars.mp hv
+      rw [List.getD_eq_getElem _ _ hi] at hm
+      exact hvars _ (List.getElem_mem hi) m hm v hvm
+    simp only [List.mem_filter, List.mem_range, decide_eq_true_eq]
+    constructor
+    · rintro ⟨hv, hJv⟩
+      exact ⟨⟨hm hv, hJv⟩, hv⟩
+    · rintro ⟨⟨_, hJv⟩, hv⟩
+      exact ⟨hv, hJv⟩
+  calc ∑ g ∈ range J, width J sys d g h ≤ ∑ g ∈ range J, (pairInc J sys g h).length :=
+        Finset.sum_le_sum fun g _ => width_le g h
+    _ = ((List.range sys.length).map fun i =>
+          ((equationVars (sys.getD i [])).filter (· % J = h)).length).sum :=
+        sum_length_pairInc_col hJ h
+    _ = ((List.residueClass J n h).map fun v => varDegree v sys).sum := by
+        rw [List.map_congr_left fun i hi => hper i (List.mem_range.mp hi)]
+        simp only [List.length_filter_eq_sum, decide_eq_true_eq]
+        rw [List.sum_map_range_eq_sum_range, Finset.sum_list_sum_comm]
+        simp only [varDegree_eq_sum, List.sum_map_range_eq_sum_range]
+    _ ≤ (List.residueClass J n h).length * D := by
+        refine (List.sum_le_length_nsmul _ D fun x hx => ?_).trans (by simp)
+        obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hx
+        exact hD v (List.mem_range.mp (List.mem_filter.mp hv).1)
+    _ ≤ (n / J + 1) * D := Nat.mul_le_mul_right _ (List.length_residueClass_le J n h)
+
+/-! ### The wire bound (D.3) -/
+
+/-- **The index wires of one pair**: `2 ^ ⌈log₂ C(N, d)⌉ ≤ 2 C(N, d')`, where `d' = d` if
+`d ≤ N` and `d' = 0` otherwise. -/
+theorem two_pow_clog_choose_le (N d : ℕ) :
+    2 ^ Nat.clog 2 (N.choose d) ≤ 2 * N.choose (if d ≤ N then d else 0) := by
+  split_ifs with hd
+  · have hC := Nat.choose_pos hd
+    rcases Nat.lt_or_ge 1 (N.choose d) with h1 | h1
+    · have h2 := Nat.pow_pred_clog_lt_self one_lt_two h1
+      have h3 : 1 ≤ Nat.clog 2 (N.choose d) := Nat.succ_le_of_lt (Nat.clog_pos one_lt_two h1)
+      calc 2 ^ Nat.clog 2 (N.choose d) = 2 * 2 ^ (Nat.clog 2 (N.choose d)).pred := by
+            conv_lhs => rw [← Nat.succ_pred_eq_of_pos h3]
+            rw [pow_succ']
+        _ ≤ 2 * N.choose d := by omega
+    · have : N.choose d = 1 := by omega
+      rw [this]
+      simp
+  · rw [Nat.choose_eq_zero_of_lt (by omega)]
+    simp
+
+/-- The entries of the array below `J²`, pair by pair. -/
+theorem sum_getD_eq (J : ℕ) (d : List ℕ) :
+    ∑ g ∈ range J, ∑ h ∈ range J, d.getD (g * J + h) 0 =
+      ((List.range (J * J)).map (d.getD · 0)).sum := by
+  rw [← List.flatMap_range_mul, List.sum_map_flatMap, List.sum_map_range_eq_sum_range]
+  simp only [List.map_map, List.sum_map_range_eq_sum_range, Function.comp_def]
+
+/-- **The wire bound (D.3), exponential form**: a live array has `2 ^ M ≤ 2 ^ (J²) C(N + K, K)`
+for its `M` index wires and the `N` incidences of the system. -/
+theorem two_pow_numWires_le (hJ : 0 < J) {K : ℕ} (hlive : live J K d = true) :
+    2 ^ numWires J sys d ≤ 2 ^ (J * J) * (numInc sys + K).choose K := by
+  set D' : ℕ → ℕ → ℕ := fun g h =>
+    if d.getD (g * J + h) 0 ≤ (pairInc J sys g h).length then d.getD (g * J + h) 0 else 0
+  have hD' : ∑ g ∈ range J, ∑ h ∈ range J, D' g h ≤ K := by
+    have hK : ((List.range (J * J)).map (d.getD · 0)).sum ≤ K := by
+      simpa [live] using hlive
+    refine le_trans (Finset.sum_le_sum fun g _ => Finset.sum_le_sum fun h _ => ?_)
+      ((sum_getD_eq J d).le.trans hK)
+    simp only [D']
+    split_ifs <;> omega
+  calc 2 ^ numWires J sys d
+      = ∏ g ∈ range J, ∏ h ∈ range J, 2 ^ width J sys d g h := by
+        rw [numWires_eq, ← Finset.prod_pow_eq_pow_sum]
+        exact Finset.prod_congr rfl fun g _ => (Finset.prod_pow_eq_pow_sum _ _ _).symm
+    _ ≤ ∏ g ∈ range J, ∏ h ∈ range J, (2 * (pairInc J sys g h).length.choose (D' g h)) :=
+        Finset.prod_le_prod fun g _ => Finset.prod_le_prod fun h _ => two_pow_clog_choose_le _ _
+    _ = 2 ^ (J * J) * ∏ g ∈ range J, ∏ h ∈ range J, (pairInc J sys g h).length.choose (D' g h) := by
+        simp only [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range, ← pow_mul]
+    _ ≤ 2 ^ (J * J) * (numInc sys).choose (∑ g ∈ range J, ∑ h ∈ range J, D' g h) := by
+        refine Nat.mul_le_mul_left _ ?_
+        rw [← sum_sum_length_pairInc hJ]
+        exact (Finset.prod_le_prod fun g _ => Nat.prod_choose_le_choose_sum _ _ _).trans
+          (Nat.prod_choose_le_choose_sum _ _ _)
+    _ ≤ 2 ^ (J * J) * (numInc sys + K).choose K :=
+        Nat.mul_le_mul_left _ (Nat.choose_le_add_choose_of_le hD')
+
+/-- **The wire bound (D.3)**: if `N + K ≤ R K` for the `N` incidences of the system, a live array
+has at most `J² + K ⌈log₂ (3 R)⌉` index wires. -/
+theorem numWires_le (hJ : 0 < J) {K R : ℕ} (hlive : live J K d = true)
+    (hR : numInc sys + K ≤ R * K) :
+    numWires J sys d ≤ J * J + K * Nat.clog 2 (3 * R) := by
+  have h1 := two_pow_numWires_le (sys := sys) hJ hlive
+  have h2 : (numInc sys + K).choose K ≤ 2 ^ (K * Nat.clog 2 (3 * R)) :=
+    (Nat.add_choose_le_three_mul_pow hR).trans (by
+      rw [pow_mul']
+      exact Nat.pow_le_pow_left (Nat.le_pow_clog one_lt_two _) _)
+  have h3 : 2 ^ numWires J sys d ≤ 2 ^ (J * J + K * Nat.clog 2 (3 * R)) := by
+    rw [pow_add]
+    exact h1.trans (Nat.mul_le_mul_left _ h2)
+  exact (Nat.pow_le_pow_iff_right (by norm_num)).mp h3
+
+end Cslib.Circuits.Frontier.IncidenceNetwork
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetworkSize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetworkSize.lean
new file mode 100644
index 0000000000..663a126e99
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceNetworkSize.lean
@@ -0,0 +1,238 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetworkBounds
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContraction
+public import Complexity.Foundations.Data.Nat.CeilQuarter
+import Complexity.Foundations.Data.Nat.Asymptotics
+
+/-!
+# The size of the incidence network at `s = n ν`
+
+Lemma D.2 of [OpenAI2026ETH] applies Theorem D.1 to the incidence network
+(`Cslib.Circuits.Frontier.IncidenceNetwork.network`) with `J = ⌈n ^ (1/4)⌉` groups
+(`Nat.ceilQuarter`), size parameter `s = n ν` and precision and truncation order `n + 1`, where
+`λ = ⌈log₂ n⌉` and `ν = ⌈log₂ λ⌉` (p. 56). This file fixes these parameters
+(`IncidenceNetwork.lemmaNetwork`) and proves the shape hypotheses of Theorem D.1 for all
+sufficiently large `n` (`IncidenceNetwork.exists_size`): at least `s` and at most `C s` edges, at
+most `C s` vertices, and degree at most `⌈s ^ (9/10)⌉`.
+
+The hypotheses are those of a reduced branch of Lemma D.2 (p. 54), up to constants: at most `c n`
+tests, every scope with at most `λ ^ c` variables, every variable in at most `λ ^ c` scopes, and
+`n ≤ K ≤ c n` for the degree cap. The paper's `K = k (a + 2 (ℓ - 1))` with `ℓ = n + 1` satisfies
+the last for `k ≥ 1`.
+
+* *Edges.* By (D.3) (`IncidenceNetwork.numWires_le`) with `R = c λ ^ c + 1`, a live array has at
+  most `J² + K ⌈log₂ (3 R)⌉ ≤ 4 n + c n (⌈log₂ (3 c + 3)⌉ + c) ν` index wires.
+* *Degrees.* A group vertex has at most `(c n / J + 1) λ ^ c` ports
+  (`IncidenceNetwork.length_rowPorts_le`, `IncidenceNetwork.length_colPorts_le`), and
+  `(c n / J) ^ 4 ≤ c ^ 4 n ³`, so its tenth power is at most `n ^ (15/2) λ ^ (10 c)` up to
+  constants, below `s ^ 9` once `λ ^ (40 c)` is below `n ^ 6`.
+
+## Main definitions
+
+* `Cslib.Circuits.Frontier.IncidenceNetwork.sizeParam`: `s = n ν`.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.lemmaNetwork`: the network of Lemma D.2.
+
+## Main results
+
+* `Cslib.Circuits.Frontier.IncidenceNetwork.length_ports_le`: the ports of any vertex.
+* `Cslib.Circuits.Frontier.IncidenceNetwork.exists_size`: the shape hypotheses of Theorem D.1.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.2 (pp. 54–56).
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier.IncidenceNetwork
+
+open Cslib.Complexity
+
+/-! ### Parameters -/
+
+/-- **The size parameter of Lemma D.2**: `s = n ν`, for `λ = ⌈log₂ n⌉` and `ν = ⌈log₂ λ⌉`. -/
+@[expose] def sizeParam (n : ℕ) : ℕ := n * Nat.clog 2 (Nat.clog 2 n)
+
+/-- **The network of Lemma D.2** for the array `d` of a system on `n` variables with degree cap
+`K`: `⌈n ^ (1/4)⌉` groups, size `n ν`, precision and truncation order `n + 1` (p. 56). -/
+@[expose] def lemmaNetwork (K n : ℕ) (sys : List (List (List ℕ))) (d : List ℕ) :
+    ℕ × DescribedNetwork Desc :=
+  network (n + 1) (n + 1) (Nat.ceilQuarter n) K (sizeParam n) n sys d
+
+/-! ### Ports of all vertices -/
+
+variable {P ℓ J K s n : ℕ} {sys : List (List (List ℕ))} {d : List ℕ}
+
+/-- **The ports of every vertex**: a padding vertex has one, the isolated row none, and a group
+vertex at most `(a / J + 1) S` or `(n / J + 1) D` under the hypotheses of the degree bounds. -/
+theorem length_ports_le (hJ : 0 < J) {S D : ℕ}
+    (hS : ∀ eq ∈ sys, (equationVars eq).length ≤ S)
+    (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hD : ∀ v < n, varDegree v sys ≤ D) :
+    ∀ v ∈ (network P ℓ J K s n sys d).2.vertices,
+      v.1.length ≤ max 1 (max ((sys.length / J + 1) * S) ((n / J + 1) * D)) := by
+  intro v hv
+  change v ∈ rows P ℓ J K s sys d ++ cols P J K s n sys d at hv
+  rcases List.mem_append.mp hv with hv | hv
+  · rcases List.mem_append.mp hv with hv | hv
+    · by_cases hl : live J K d
+      · rw [ite_eq_left hl] at hv
+        obtain ⟨g, -, rfl⟩ := List.mem_map.mp hv
+        exact (length_rowPorts_le hJ g hS).trans (le_max_of_le_right (le_max_left _ _))
+      · rw [ite_eq_right hl] at hv
+        rw [List.mem_singleton.mp hv]
+        simp [deadRow]
+    · obtain ⟨e, -, rfl⟩ := List.mem_map.mp hv
+      simp [padRow]
+  · rcases List.mem_append.mp hv with hv | hv
+    · by_cases hl : live J K d
+      · rw [ite_eq_left hl] at hv
+        obtain ⟨h, hh, rfl⟩ := List.mem_map.mp hv
+        exact (length_colPorts_le hJ (List.mem_range.mp hh) hvars hD).trans
+          (le_max_of_le_right (le_max_right _ _))
+      · rw [ite_eq_right hl] at hv
+        simp at hv
+    · obtain ⟨e, -, rfl⟩ := List.mem_map.mp hv
+      simp [padCol]
+
+/-! ### Asymptotics -/
+
+/-- `(c n / J) ^ 4 ≤ c ^ 4 n ³` when `n ≤ J ^ 4`. -/
+theorem div_pow_four_le {c n J : ℕ} (hJ : 0 < J) (hn : n ≤ J ^ 4) :
+    (c * n / J) ^ 4 ≤ c ^ 4 * n ^ 3 := by
+  have h1 : (c * n / J * J) ^ 4 ≤ (c * n) ^ 4 := Nat.pow_le_pow_left (Nat.div_mul_le_self _ _) _
+  have hJ4 : 0 < J ^ 4 := Nat.pow_pos (n := 4) hJ
+  refine Nat.le_of_mul_le_mul_right ?_ hJ4
+  calc (c * n / J) ^ 4 * J ^ 4 = (c * n / J * J) ^ 4 := (Nat.mul_pow _ _ _).symm
+    _ ≤ (c * n) ^ 4 := h1
+    _ = c ^ 4 * n ^ 3 * n := by ring
+    _ ≤ c ^ 4 * n ^ 3 * J ^ 4 := Nat.mul_le_mul_left _ hn
+
+/-- **The shape hypotheses of Theorem D.1 for the network of Lemma D.2.** For every `c` there are
+`C` and `n₀` such that for all `n ≥ n₀`, every system on `n` variables with at most `c n` tests,
+scopes of at most `λ ^ c` variables, and every variable in at most `λ ^ c` scopes, every degree cap
+`n ≤ K ≤ c n` and every array, the network of Lemma D.2 at size `s = n ν` has between `s` and
+`C s` edges, at most `C s` vertices, and maximum degree at most `⌈s ^ (9/10)⌉`. -/
+theorem exists_size (c : ℕ) : ∃ C n₀ : ℕ, ∀ n, n₀ ≤ n → ∀ (K : ℕ) (sys : List (List (List ℕ)))
+    (d : List ℕ), sys.length ≤ c * n → n ≤ K → K ≤ c * n →
+    (∀ eq ∈ sys, (equationVars eq).length ≤ Nat.clog 2 n ^ c) →
+    (∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) →
+    (∀ v < n, varDegree v sys ≤ Nat.clog 2 n ^ c) →
+    sizeParam n ≤ (lemmaNetwork K n sys d).2.numEdges ∧
+      (lemmaNetwork K n sys d).2.numEdges ≤ C * sizeParam n ∧
+      (lemmaNetwork K n sys d).2.vertices.length ≤ C * sizeParam n ∧
+      ∀ v ∈ (lemmaNetwork K n sys d).2.vertices, v.1.length ≤ ceilNineTenths (sizeParam n) := by
+  set c' := c + 1
+  set A := Nat.clog 2 (3 * c + 3)
+  set B := (16 * (c' ^ 4 + 1)) ^ 10
+  obtain ⟨L₀, hL₀⟩ := Filter.eventually_atTop.mp
+    (Nat.eventually_mul_add_one_pow_le_pow_div B (40 * c') 2 one_lt_two (by norm_num))
+  refine ⟨5 + c * (A + c), 2 ^ (L₀ + 2) + 5, fun n hn K sys d hsys hnK hKn hS hvars hD => ?_⟩
+  set lam := Nat.clog 2 n with hlam
+  set nu := Nat.clog 2 lam with hnu
+  set J := Nat.ceilQuarter n with hJdef
+  have hn5 : 5 ≤ n := (Nat.le_add_left 5 _).trans hn
+  have hn1 : 1 ≤ n := by omega
+  have hJ : 0 < J := Nat.ceilQuarter_pos hn1
+  -- `λ ≥ L₀ + 2 ≥ 2` and `ν ≥ 1`.
+  have hlamL : L₀ + 2 ≤ lam := by
+    have := Nat.clog_mono_right 2 ((Nat.le_add_right (2 ^ (L₀ + 2)) 5).trans hn)
+    rwa [Nat.clog_pow 2 _ one_lt_two] at this
+  have hnu1 : 1 ≤ nu := Nat.clog_pos one_lt_two (by omega)
+  have hlam1 : 1 ≤ lam ^ c := Nat.one_le_pow _ _ (by omega)
+  have hs : sizeParam n = n * nu := rfl
+  have hns : n ≤ sizeParam n := by rw [hs]; exact Nat.le_mul_of_pos_right _ hnu1
+  -- The index wires.
+  have hM : mainWires J K sys d ≤ (4 + c * (A + c)) * (n * nu) := by
+    unfold mainWires
+    split_ifs with hl
+    · have hinc : numInc sys ≤ c * n * lam ^ c :=
+        (List.sum_le_length_nsmul _ _ fun x hx => by
+          obtain ⟨eq, heq, rfl⟩ := List.mem_map.mp hx
+          exact hS eq heq).trans (by simp only [List.length_map, smul_eq_mul]; nlinarith)
+      have hR : numInc sys + K ≤ (c * lam ^ c + 1) * K := by nlinarith
+      have hW := numWires_le hJ hl hR
+      have hlog : Nat.clog 2 (3 * (c * lam ^ c + 1)) ≤ (A + c) * nu := by
+        refine Nat.clog_le_of_le_pow ?_
+        have hlamle : lam ≤ 2 ^ nu := Nat.le_pow_clog one_lt_two _
+        have hA : 3 * c + 3 ≤ 2 ^ A := Nat.le_pow_clog one_lt_two _
+        calc 3 * (c * lam ^ c + 1) ≤ (3 * c + 3) * lam ^ c := by nlinarith
+          _ ≤ 2 ^ A * (2 ^ nu) ^ c := Nat.mul_le_mul hA (Nat.pow_le_pow_left hlamle _)
+          _ = 2 ^ (A + nu * c) := by rw [← pow_mul, ← pow_add]
+          _ ≤ 2 ^ ((A + c) * nu) := Nat.pow_le_pow_right (by norm_num) (by nlinarith)
+      have hJJ := Nat.ceilQuarter_mul_self_le hn1
+      calc numWires J sys d ≤ J * J + K * Nat.clog 2 (3 * (c * lam ^ c + 1)) := hW
+        _ ≤ 4 * n + c * n * ((A + c) * nu) := Nat.add_le_add hJJ (Nat.mul_le_mul hKn hlog)
+        _ ≤ (4 + c * (A + c)) * (n * nu) := by nlinarith
+    · exact Nat.zero_le _
+  have hE : (lemmaNetwork K n sys d).2.numEdges = max (mainWires J K sys d) (sizeParam n) :=
+    numEdges_network
+  refine ⟨hE ▸ le_max_right _ _, ?_, ?_, ?_⟩
+  · rw [hE, hs]
+    refine max_le (hM.trans (Nat.mul_le_mul_right _ (by omega))) ?_
+    nlinarith
+  · have hV := length_vertices_network (P := n + 1) (ℓ := n + 1) (J := J) (K := K)
+      (s := sizeParam n) (n := n) (sys := sys) (d := d)
+    change (network (n + 1) (n + 1) J K (sizeParam n) n sys d).2.vertices.length ≤ _
+    rw [hV]
+    have hJn : J ≤ n := Nat.ceilQuarter_le_self n
+    have : (if live J K d = true then 2 * J else 1) ≤ 2 * n := by split_ifs <;> omega
+    have h5 : 5 * sizeParam n ≤ (5 + c * (A + c)) * sizeParam n :=
+      Nat.mul_le_mul_right _ (by omega)
+    omega
+  · -- Degrees.
+    intro v hv
+    have hports := length_ports_le (P := n + 1) (ℓ := n + 1) (K := K) (s := sizeParam n)
+      (d := d) hJ hS hvars hD v hv
+    have hs1 : 1 ≤ sizeParam n := hn1.trans hns
+    -- The bound `x = (c' n / J + 1) λ ^ c` on both group degrees.
+    set a := c' * n / J with ha
+    have hx : (a + 1) * lam ^ c ≤ ceilNineTenths (sizeParam n) := by
+      refine le_ceilNineTenths_of_pow_le hs1
+        ((Nat.pow_le_pow_iff_left (n := 4) (by norm_num)).mp ?_)
+      have ha4 : a ^ 4 ≤ c' ^ 4 * n ^ 3 := div_pow_four_le hJ (Nat.le_ceilQuarter_pow n)
+      have ha1 : (a + 1) ^ 4 ≤ 16 * (c' ^ 4 + 1) * n ^ 3 := by
+        have hn3 : 1 ≤ n ^ 3 := Nat.one_le_pow _ _ hn1
+        have h16 : (a + 1) ^ 4 ≤ 16 * (a ^ 4 + 1) := by
+          rcases Nat.eq_zero_or_pos a with h0 | h0
+          · simp [h0]
+          · calc (a + 1) ^ 4 ≤ (2 * a) ^ 4 := Nat.pow_le_pow_left (by omega) _
+              _ = 16 * a ^ 4 := by ring
+              _ ≤ 16 * (a ^ 4 + 1) := by omega
+        calc (a + 1) ^ 4 ≤ 16 * (a ^ 4 + 1) := h16
+          _ ≤ 16 * (c' ^ 4 * n ^ 3 + n ^ 3) := by omega
+          _ = 16 * (c' ^ 4 + 1) * n ^ 3 := by ring
+      -- `B λ ^ (40 c) ≤ n`.
+      have hB : B * lam ^ (40 * c) ≤ n := by
+        have h1 : B * lam ^ (40 * c) ≤ B * (lam + 1) ^ (40 * c') :=
+          Nat.mul_le_mul_left _ ((Nat.pow_le_pow_left (Nat.le_succ _) _).trans
+            (Nat.pow_le_pow_right (by omega) (by omega)))
+        have h2 := hL₀ lam (by omega)
+        have h3 : 2 ^ (lam / 2) ≤ 2 ^ (lam - 1) := Nat.pow_le_pow_right (by norm_num) (by omega)
+        have h4 : 2 ^ (lam - 1) < n := by
+          have := Nat.pow_pred_clog_lt_self one_lt_two (show 1 < n by omega)
+          rwa [Nat.pred_eq_sub_one] at this
+        omega
+      have hns36 : n ^ 36 ≤ sizeParam n ^ 36 := Nat.pow_le_pow_left hns _
+      calc (((a + 1) * lam ^ c) ^ 10) ^ 4 = ((a + 1) ^ 4) ^ 10 * lam ^ (40 * c) := by ring
+        _ ≤ (16 * (c' ^ 4 + 1) * n ^ 3) ^ 10 * lam ^ (40 * c) :=
+            Nat.mul_le_mul_right _ (Nat.pow_le_pow_left ha1 _)
+        _ = n ^ 30 * (B * lam ^ (40 * c)) := by ring
+        _ ≤ n ^ 30 * n ^ 6 := Nat.mul_le_mul_left _ (hB.trans (Nat.le_self_pow (by norm_num) _))
+        _ = n ^ 36 := by ring
+        _ ≤ (sizeParam n ^ 9) ^ 4 := by rw [← pow_mul]; exact hns36
+    refine hports.trans (max_le ?_ (max_le ?_ ?_))
+    · exact le_ceilNineTenths_of_pow_le hs1 (by simpa using Nat.one_le_pow 9 _ hs1)
+    · refine le_trans (Nat.mul_le_mul_right _ (Nat.add_le_add_right ?_ 1)) hx
+      exact Nat.div_le_div_right (hsys.trans (Nat.mul_le_mul_right _ (by omega)))
+    · refine le_trans (Nat.mul_le_mul_right _ (Nat.add_le_add_right ?_ 1)) hx
+      exact Nat.div_le_div_right (Nat.le_mul_of_pos_left _ (by omega))
+
+end Cslib.Circuits.Frontier.IncidenceNetwork
diff --git a/Complexity/Foundations/Data/List/Blocks.lean b/Complexity/Foundations/Data/List/Blocks.lean
new file mode 100644
index 0000000000..9b52c73375
--- /dev/null
+++ b/Complexity/Foundations/Data/List/Blocks.lean
@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Data.Finset.Card
+import Complexity.Foundations.Data.List.OfFn
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Data.List.GetD
+
+/-!
+# Sums over ranges, consecutive blocks and residue classes
+
+Small facts about lists of natural numbers.
+
+* **Sums over ranges.** A list sum over `List.range n` is the `Finset` sum over `range n`
+  (`List.sum_map_range_eq_sum_range`); a list is its entries at `0, …, length - 1`
+  (`List.map_getD_range`); sums over a `flatMap` and of a filter's length
+  (`List.sum_map_flatMap`, `List.length_filter_eq_sum`), and a `Finset` sum of list sums is a
+  list sum of `Finset` sums (`Finset.sum_list_sum_comm`).
+* **Consecutive blocks.** Numbering blocks of sizes `w 0, w 1, …` consecutively, block `b` is
+  `List.blockRange w b`, starting at `List.blockStart w b`; the blocks below `B` are the numbers
+  below `List.blockStart w B` (`List.flatMap_blockRange`). The pairs `g J + h` for `g < G`,
+  `h < J` are the numbers below `G J` (`List.flatMap_range_mul`).
+* **Residue classes.** `List.residueClass J m g` is the numbers below `m` congruent to `g` modulo
+  `J`. Summing over the residue classes modulo `J > 0` sums over the list (`List.sum_filter_mod`),
+  and a residue class below `m` has at most `m / J + 1` numbers
+  (`List.length_residueClass_le`).
+
+## Main definitions
+
+* `List.blockStart`, `List.blockRange`: consecutive blocks.
+* `List.residueClass`: a residue class below `m`.
+
+## Main results
+
+* `List.sum_map_range_eq_sum_range`, `List.map_getD_range`, `List.sum_map_flatMap`,
+  `List.length_filter_eq_sum`, `Finset.sum_list_sum_comm`: sums.
+* `List.flatMap_blockRange`, `List.flatMap_range_mul`: consecutive blocks.
+* `List.sum_filter_mod`, `List.sum_residueClass`, `List.sum_length_filter_mod`,
+  `List.length_residueClass_le`: residue classes.
+-/
+
+public section
+
+open Finset
+
+namespace List
+
+/-! ### Sums over ranges -/
+
+/-- A list sum over `List.range n` is the `Finset` sum over `range n`. -/
+theorem sum_map_range_eq_sum_range {M : Type*} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) :
+    ((List.range n).map f).sum = ∑ i ∈ Finset.range n, f i :=
+  (List.sum_map_range n f).trans (Finset.sum_range f).symm
+
+/-- A list is its entries at `0, …, length - 1`. -/
+theorem map_getD_range {α : Type*} (l : List α) (x : α) :
+    (List.range l.length).map (l.getD · x) = l := by
+  refine List.ext_getElem (by simp) fun i h₁ h₂ => ?_
+  simp [List.getElem?_eq_getElem h₂]
+
+/-- A sum over a `flatMap` sums the inner sums. -/
+theorem sum_map_flatMap {α β : Type*} (l : List α) (f : α → List β) (g : β → ℕ) :
+    ((l.flatMap f).map g).sum = (l.map fun x => ((f x).map g).sum).sum := by
+  induction l with
+  | nil => rfl
+  | cons x l ih => simp [List.flatMap_cons, ih]
+
+/-- The length of a filtered list counts its elements satisfying the predicate. -/
+theorem length_filter_eq_sum {α : Type*} (l : List α) (q : α → Bool) :
+    (l.filter q).length = (l.map fun x => if q x then 1 else 0).sum := by
+  induction l with
+  | nil => rfl
+  | cons x l ih => by_cases hx : q x <;> simp [hx, ih, Nat.add_comm]
+
+end List
+
+/-- A `Finset` sum of list sums is the list sum of the `Finset` sums. -/
+theorem Finset.sum_list_sum_comm {ι α : Type*} (s : Finset ι) (l : List α) (f : ι → α → ℕ) :
+    ∑ h ∈ s, (l.map (f h)).sum = (l.map fun x => ∑ h ∈ s, f h x).sum := by
+  induction l with
+  | nil => simp
+  | cons x l ih => simp only [List.map_cons, List.sum_cons, Finset.sum_add_distrib, ih]
+
+namespace List
+
+/-! ### Consecutive blocks -/
+
+/-- The first number of block `b` when block `b'` has `w b'` numbers: `Σ_{b' < b} w b'`. -/
+@[expose] def blockStart (w : ℕ → ℕ) (b : ℕ) : ℕ := ((List.range b).map w).sum
+
+/-- The numbers of block `b`: `blockStart w b, …, blockStart w b + w b - 1`. -/
+@[expose] def blockRange (w : ℕ → ℕ) (b : ℕ) : List ℕ := List.range' (blockStart w b) (w b)
+
+theorem blockStart_succ (w : ℕ → ℕ) (b : ℕ) : blockStart w (b + 1) = blockStart w b + w b := by
+  simp [blockStart, List.range_succ]
+
+/-- **Consecutive blocks**: the numbers of the blocks below `B`, in order, are the numbers below
+`blockStart w B`. -/
+theorem flatMap_blockRange (w : ℕ → ℕ) (B : ℕ) :
+    (List.range B).flatMap (blockRange w) = List.range (blockStart w B) := by
+  induction B with
+  | zero => simp [blockStart]
+  | succ B ih =>
+    rw [List.range_succ, List.flatMap_append, ih, List.flatMap_singleton, blockRange,
+      List.range_eq_range', List.range_eq_range', blockStart_succ]
+    simpa using List.range'_append_1 (s := 0) (m := blockStart w B) (n := w B)
+
+/-- The pairs `g J + h` for `g < G` and `h < J`, in order, are the numbers below `G J`. -/
+theorem flatMap_range_mul (G J : ℕ) :
+    (List.range G).flatMap (fun g => (List.range J).map (g * J + ·)) = List.range (G * J) := by
+  induction G with
+  | zero => simp
+  | succ G ih =>
+    rw [List.range_succ, List.flatMap_append, ih, List.flatMap_singleton,
+      ← List.range'_eq_map_range, List.range_eq_range', List.range_eq_range', Nat.succ_mul]
+    simpa using List.range'_append_1 (s := 0) (m := G * J) (n := J)
+
+/-! ### Residue classes -/
+
+/-- **The residue class of `g` modulo `J` below `m`**: the numbers below `m` congruent to `g`,
+in increasing order. -/
+@[expose] def residueClass (J m g : ℕ) : List ℕ := (List.range m).filter (· % J = g)
+
+/-- Summing over the residue classes modulo `J > 0` sums over the list. -/
+theorem sum_filter_mod {J : ℕ} (hJ : 0 < J) (l : List ℕ) (f : ℕ → ℕ) :
+    ∑ h ∈ Finset.range J, ((l.filter (· % J = h)).map f).sum = (l.map f).sum := by
+  induction l with
+  | nil => simp
+  | cons x l ih =>
+    have hc : ∀ h, (((x :: l).filter (· % J = h)).map f).sum =
+        (if x % J = h then f x else 0) + ((l.filter (· % J = h)).map f).sum := by
+      intro h
+      by_cases hx : x % J = h <;> simp [hx]
+    rw [Finset.sum_congr rfl fun h _ => hc h, Finset.sum_add_distrib, ih,
+      Finset.sum_ite_eq (Finset.range J) (x % J) (fun _ => f x),
+      ite_eq_left (Finset.mem_range.mpr (Nat.mod_lt x hJ))]
+    simp
+
+/-- Summing over the residue classes below `m` sums over the numbers below `m`. -/
+theorem sum_residueClass {J : ℕ} (hJ : 0 < J) (m : ℕ) (f : ℕ → ℕ) :
+    ∑ g ∈ Finset.range J, ((residueClass J m g).map f).sum = ((List.range m).map f).sum :=
+  sum_filter_mod hJ _ f
+
+/-- Summing the sizes of the residue classes modulo `J > 0` gives the length. -/
+theorem sum_length_filter_mod {J : ℕ} (hJ : 0 < J) (l : List ℕ) :
+    ∑ h ∈ Finset.range J, (l.filter (· % J = h)).length = l.length := by
+  simpa using sum_filter_mod hJ l fun _ => 1
+
+/-- **A residue class below `m` has at most `m / J + 1` numbers.** -/
+theorem length_residueClass_le (J m g : ℕ) : (residueClass J m g).length ≤ m / J + 1 := by
+  rw [residueClass, ← List.toFinset_card_of_nodup ((List.nodup_range).filter _)]
+  calc #((List.range m).filter (· % J = g)).toFinset
+      ≤ #(Finset.range (m / J + 1)) := by
+        refine Finset.card_le_card_of_injOn (· / J) (fun x hx => ?_) (fun x hx y hy hxy => ?_)
+        · simp only [Finset.mem_coe, List.mem_toFinset, List.mem_filter, List.mem_range,
+            decide_eq_true_eq] at hx
+          simp only [Finset.coe_range, Set.mem_Iio]
+          exact Nat.lt_succ_of_le (Nat.div_le_div_right hx.1.le)
+        · simp only [Finset.mem_coe, List.mem_toFinset, List.mem_filter, List.mem_range,
+            decide_eq_true_eq] at hx hy
+          rw [← Nat.div_add_mod x J, ← Nat.div_add_mod y J, hx.2, hy.2]
+          exact congrArg (J * · + g) hxy
+    _ = m / J + 1 := Finset.card_range _
+
+end List
diff --git a/Complexity/Foundations/Data/Nat/CeilQuarter.lean b/Complexity/Foundations/Data/Nat/CeilQuarter.lean
new file mode 100644
index 0000000000..28142a085c
--- /dev/null
+++ b/Complexity/Foundations/Data/Nat/CeilQuarter.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Data.Nat.Find
+import Mathlib.Algebra.Order.Group.Nat
+import Mathlib.Tactic.Linarith
+
+/-!
+# The ceiling of the fourth root
+
+`Nat.ceilQuarter n` is `⌈n ^ (1/4)⌉`, the least `J` with `n ≤ J ^ 4`. It is positive for `n ≥ 1`,
+at most `n`, and its square is at most `4 n`.
+
+## Main definitions
+
+* `Nat.ceilQuarter`: `⌈n ^ (1/4)⌉`.
+
+## Main results
+
+* `Nat.le_ceilQuarter_pow`, `Nat.ceilQuarter_pos`, `Nat.ceilQuarter_le_self`,
+  `Nat.ceilQuarter_mul_self_le`: its bounds.
+-/
+
+public section
+
+namespace Nat
+
+/-- **`⌈n ^ (1/4)⌉`**, the least `J` with `n ≤ J ^ 4`. -/
+@[expose] def ceilQuarter (n : ℕ) : ℕ :=
+  Nat.find (⟨n, Nat.le_self_pow (by norm_num) n⟩ : ∃ J, n ≤ J ^ 4)
+
+theorem le_ceilQuarter_pow (n : ℕ) : n ≤ ceilQuarter n ^ 4 :=
+  Nat.find_spec (⟨n, Nat.le_self_pow (by norm_num) n⟩ : ∃ J, n ≤ J ^ 4)
+
+theorem ceilQuarter_pos {n : ℕ} (hn : 1 ≤ n) : 0 < ceilQuarter n := by
+  rcases Nat.eq_zero_or_pos (ceilQuarter n) with h0 | h
+  · have := le_ceilQuarter_pow n
+    rw [h0, zero_pow (by norm_num)] at this
+    omega
+  · exact h
+
+theorem ceilQuarter_le_self (n : ℕ) : ceilQuarter n ≤ n :=
+  Nat.find_min' _ (Nat.le_self_pow (by norm_num) n)
+
+/-- `J² ≤ 4 n` for `J = ⌈n ^ (1/4)⌉` and `n ≥ 1`. -/
+theorem ceilQuarter_mul_self_le {n : ℕ} (hn : 1 ≤ n) : ceilQuarter n * ceilQuarter n ≤ 4 * n := by
+  set J := ceilQuarter n
+  have hJ := ceilQuarter_pos hn
+  have hmin : ¬ n ≤ (J - 1) ^ 4 :=
+    Nat.find_min (⟨n, Nat.le_self_pow (by norm_num) n⟩ : ∃ J, n ≤ J ^ 4)
+      (show J - 1 < ceilQuarter n by omega)
+  have h2 : (J - 1) * (J - 1) ≤ (J - 1) ^ 4 := by
+    rcases Nat.eq_zero_or_pos (J - 1) with h | h
+    · simp [h]
+    · calc (J - 1) * (J - 1) = (J - 1) ^ 2 := (sq _).symm
+        _ ≤ (J - 1) ^ 4 := Nat.pow_le_pow_right h (by norm_num)
+  rcases Nat.lt_or_ge J 2 with hJ2 | hJ2
+  · have : J = 1 := by omega
+    rw [this]
+    omega
+  · have : J ≤ 2 * (J - 1) := by omega
+    nlinarith
+
+end Nat
diff --git a/Complexity/Foundations/Data/Nat/Choose/Vandermonde.lean b/Complexity/Foundations/Data/Nat/Choose/Vandermonde.lean
new file mode 100644
index 0000000000..dc037ecc37
--- /dev/null
+++ b/Complexity/Foundations/Data/Nat/Choose/Vandermonde.lean
@@ -0,0 +1,92 @@
+/-
+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 (Mathlib, `Mathlib/Data/Nat/Choose/Vandermonde.lean`)
+
+public import Complexity.Init
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Data.Nat.Choose.Basic
+import Complexity.Foundations.Data.Nat.Factorial
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Data.Nat.Choose.Vandermonde
+
+/-!
+# Products and sums of binomial coefficients
+
+Choosing `D x` of `N x` elements in each of several disjoint blocks chooses `Σ D x` of the
+`Σ N x` elements, so a product of binomial coefficients is at most the binomial coefficient of the
+sums (`Nat.prod_choose_le_choose_sum`, from Vandermonde's identity). Fewer selected elements are
+absorbed by stars and bars: `C(N, D) ≤ C(N + K, K)` for `D ≤ K`
+(`Nat.choose_le_add_choose_of_le`). Quantitatively, `C(N + K, K) ≤ (3 R) ^ K` when `N + K ≤ R K`
+(`Nat.add_choose_le_three_mul_pow`), from `K ^ K ≤ 3 ^ K K!`; this is the bound
+`C(N + K, K) ≤ (e (N + K) / K) ^ K` with `e` replaced by `3`.
+
+## Main results
+
+* `Nat.prod_choose_le_choose_sum`: Vandermonde's inequality.
+* `Nat.choose_le_choose_add_add`, `Nat.choose_le_add_choose_of_le`: monotonicity.
+* `Nat.add_choose_le_three_mul_pow`: `C(N + K, K) ≤ (3 R) ^ K` when `N + K ≤ R K`.
+-/
+
+public section
+
+namespace Nat
+
+open Finset
+
+/-- `C(n, k) ≤ C(n + j, k + j)`. -/
+theorem choose_le_choose_add_add (n k j : ℕ) : n.choose k ≤ (n + j).choose (k + j) := by
+  induction j with
+  | zero => rfl
+  | succ j ih =>
+    refine ih.trans ?_
+    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.choose_succ_succ]
+    omega
+
+/-- **Fewer selected elements**: `C(N, D) ≤ C(N + K, K)` for `D ≤ K`. -/
+theorem choose_le_add_choose_of_le {N D K : ℕ} (hD : D ≤ K) : N.choose D ≤ (N + K).choose K := by
+  calc N.choose D ≤ (N + (K - D)).choose (D + (K - D)) := choose_le_choose_add_add _ _ _
+    _ = (N + (K - D)).choose K := by rw [Nat.add_sub_cancel' hD]
+    _ ≤ (N + K).choose K := Nat.choose_le_choose _ (by omega)
+
+/-- **Vandermonde's inequality**: a product of binomial coefficients is at most the binomial
+coefficient of the sums. -/
+theorem prod_choose_le_choose_sum {ι : Type*} (s : Finset ι) (N D : ι → ℕ) :
+    ∏ x ∈ s, (N x).choose (D x) ≤ (∑ x ∈ s, N x).choose (∑ x ∈ s, D x) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert a s ha ih =>
+    rw [Finset.prod_insert ha, Finset.sum_insert ha, Finset.sum_insert ha]
+    calc (N a).choose (D a) * ∏ x ∈ s, (N x).choose (D x)
+        ≤ (N a).choose (D a) * (∑ x ∈ s, N x).choose (∑ x ∈ s, D x) :=
+          Nat.mul_le_mul_left _ ih
+      _ ≤ (N a + ∑ x ∈ s, N x).choose (D a + ∑ x ∈ s, D x) := by
+          rw [Nat.add_choose_eq]
+          have hm : (D a, ∑ x ∈ s, D x) ∈ antidiagonal (D a + ∑ x ∈ s, D x) :=
+            Finset.mem_antidiagonal.mpr rfl
+          exact Finset.single_le_sum
+            (f := fun ij : ℕ × ℕ => (N a).choose ij.1 * (∑ x ∈ s, N x).choose ij.2)
+            (fun _ _ => Nat.zero_le _) hm
+
+/-- **Stars and bars, quantitatively**: if `N + K ≤ R K`, then `C(N + K, K) ≤ (3 R) ^ K`. -/
+theorem add_choose_le_three_mul_pow {N K R : ℕ} (hR : N + K ≤ R * K) :
+    (N + K).choose K ≤ (3 * R) ^ K := by
+  have hf := K.factorial_pos
+  refine Nat.le_of_mul_le_mul_left ?_ hf
+  calc K.factorial * (N + K).choose K = (N + K).descFactorial K :=
+        (Nat.descFactorial_eq_factorial_mul_choose _ _).symm
+    _ ≤ (N + K) ^ K := Nat.descFactorial_le_pow _ _
+    _ ≤ (R * K) ^ K := Nat.pow_le_pow_left hR _
+    _ = R ^ K * K ^ K := Nat.mul_pow _ _ _
+    _ ≤ R ^ K * (3 ^ K * K.factorial) :=
+        Nat.mul_le_mul_left _ (pow_self_le_three_pow_mul_factorial K)
+    _ = K.factorial * (3 * R) ^ K := by
+        rw [Nat.mul_pow]
+        ring
+
+end Nat
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceNetwork.lean
new file mode 100644
index 0000000000..e2fe70b798
--- /dev/null
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceNetwork.lean
@@ -0,0 +1,88 @@
+/-
+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: local-only (test driver)
+
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetworkSize
+
+/-!
+# Tests for the incidence network of Lemma D.2
+
+A system of three tests on three variables, in two groups on each side. The array `[1, 1, 0, 1]`
+selects one incidence of the pairs `(0, 0)`, `(0, 1)` and `(1, 1)`. The pairs have `4, 2, 0, 1`
+incidences, so `2, 1, 0, 0` index wires; padding to size `6` adds three edges. The network is
+rows-first bipartite, and the hypotheses of the degree and wire bounds hold for it.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.TensorNetworkIncidenceNetwork
+
+open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.IncidenceNetwork Cslib.Complexity
+
+/-- Three tests on the variables `0, 1, 2`: `x₀ x₁ + x₂`, `x₁` and `x₀ + x₁ x₂`. -/
+abbrev sys : List (List (List ℕ)) := [[[0, 1], [2]], [[1]], [[0], [1, 2]]]
+
+/-- The network of the array `[1, 1, 0, 1]`: two groups, degree cap `4`, size `6`, precision and
+truncation order `4`, three variables. -/
+abbrev G : ℕ × DescribedNetwork Desc := network 4 4 2 4 6 3 sys [1, 1, 0, 1]
+
+example : List.residueClass 2 3 0 = [0, 2] := by decide
+example : pairInc 2 sys 0 0 = [(0, 0), (0, 2), (1, 0), (1, 2)] := by decide
+example : pairInc 2 sys 0 1 = [(0, 1), (1, 1)] := by decide
+example : pairInc 2 sys 1 0 = [] := by decide
+example : pairInc 2 sys 1 1 = [(0, 1)] := by decide
+example : numInc sys = 7 := by decide
+
+example : live 2 4 [1, 1, 0, 1] = true := by decide
+example : live 2 2 [1, 1, 0, 1] = false := by decide
+
+example : numWires 2 sys [1, 1, 0, 1] = 3 := by decide
+example : rowPorts 2 sys [1, 1, 0, 1] 0 = [0, 1, 2] := by decide
+example : colPorts 2 sys [1, 1, 0, 1] 1 = [2] := by decide
+example : G.1 = 5 := by decide
+example : G.2.numEdges = 6 := by decide
+example : G.2.vertices.length = 10 := by decide
+
+-- The network is rows-first bipartite.
+example : G.2.IsRowsFirstBipartite G.1 := isRowsFirstBipartite_network
+
+-- A dead array gets the padding and one isolated row.
+example : (network 4 4 2 2 6 3 sys [1, 1, 0, 1]).2.vertices.length = 13 := by
+  rw [length_vertices_network]
+  decide
+
+/-! ### The bounds are not vacuous -/
+
+-- Every scope has at most three variables, and every variable lies in at most three scopes.
+example : (rowPorts 2 sys [1, 1, 0, 1] 0).length ≤ (3 / 2 + 1) * 3 :=
+  length_rowPorts_le (by norm_num) 0 (S := 3) (by decide)
+
+example : (colPorts 2 sys [1, 1, 0, 1] 0).length ≤ (3 / 2 + 1) * 3 :=
+  length_colPorts_le (by norm_num) (by norm_num) (by decide) (D := 3) (by decide)
+
+-- `N + K = 7 + 4 ≤ 3 K`, so the wire bound gives at most `4 + 4 ⌈log₂ 9⌉ = 20` wires.
+example : numWires 2 sys [1, 1, 0, 1] ≤ 2 * 2 + 4 * Nat.clog 2 (3 * 3) :=
+  numWires_le (by norm_num) (by decide) (R := 3) (by decide)
+
+-- Stars and bars: `C(11, 4) = 330 ≤ 9 ^ 4`.
+example : (7 + 4).choose 4 ≤ (3 * 3) ^ 4 := Nat.add_choose_le_three_mul_pow (by norm_num)
+
+/-! ### The parameters of Lemma D.2 -/
+
+-- `⌈16 ^ (1/4)⌉ = 2` and `⌈17 ^ (1/4)⌉ = 3`.
+example : Nat.ceilQuarter 16 = 2 :=
+  le_antisymm (Nat.find_min' _ (by norm_num)) (by
+    by_contra h
+    have := Nat.le_ceilQuarter_pow 16
+    interval_cases (Nat.ceilQuarter 16) <;> simp_all)
+
+-- `16 ≤ J ^ 4` and `J ² ≤ 4 · 16` at `J = ⌈16 ^ (1/4)⌉`.
+example : 16 ≤ Nat.ceilQuarter 16 ^ 4 ∧ Nat.ceilQuarter 16 * Nat.ceilQuarter 16 ≤ 4 * 16 :=
+  ⟨Nat.le_ceilQuarter_pow 16, Nat.ceilQuarter_mul_self_le (by norm_num)⟩
+
+end ComplexityTests.TensorNetworkIncidenceNetwork