diff --git a/Complexity.lean b/Complexity.lean
index 8c8caae348..ea5c7085ca 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -876,8 +876,10 @@ public import Complexity.Computability.Circuit.Frontier.Rectangle
 public import Complexity.Computability.Circuit.Frontier.Reduction
 public import Complexity.Computability.Circuit.Frontier.Sweep
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ActiveCall
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.CauchyModes
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildSize
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean
new file mode 100644
index 0000000000..cf9a248fe1
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean
@@ -0,0 +1,284 @@
+/-
+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.LocalDeformation
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery
+public import Complexity.Foundations.Data.Polynomial.RingLagrange
+public import Complexity.Foundations.Combinatorics.PacketPacking
+public import Mathlib.RingTheory.Ideal.Quotient.Defs
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildSize
+
+/-!
+# One active call of the contraction recursion
+
+This file proves the correctness of one active call of the recursive contraction algorithm of
+[OpenAI2026ETH] (§D.4.4–§D.4.7, pp. 61–64): the contraction modulo `2 ^ p` is recovered from the
+contractions of the children modulo the higher precisions `2 ^ p_t`.
+
+**Setting.** Let `K` be a `ℚ`-algebra and `B` a subring containing `ℤ_(2)` (in the manuscript,
+`K = ℚ[U] / (f)` and `B = O`), and let `N` be a Boolean tensor network with entries in `B` whose
+edges run from rows to columns. Pack its `M` edges into packets of `L = 2 ^ a` slots, and choose
+`n > M (2 L - 1)` interpolation points `ζ k ∈ B` whose differences are units (in the manuscript,
+binary-coordinate lifts of residue-field elements). For each nonzero grid point `t` of positive
+multiplicity `q_t` and each point `ζ k`, a value `v t k ∈ B` is supplied.
+
+**Recovery** (`recoverFromValues`). Interpolate the values `v t ·` at the points `ζ` over `B`
+(`Lagrange.ringInterpolate`), and apply the tapered Hermite recovery (D.9) to the interpolants
+(`Cslib.Circuits.Frontier.taperedRecovery`).
+
+**Correctness.** If every `v t k` agrees with the local deformation `F(t + α ζ k)`
+(`TensorNetwork.localDeformation`) modulo `2 ^ p_t`, `p_t = p + 8 h D_t + 8 M (a + 1)`, then the
+interpolant agrees with `F(t + α z)` modulo `2 ^ p_t` (`Lagrange.exists_ringInterpolate_eq_add`),
+and Lemma D.5 (`Cslib.Circuits.Frontier.exists_taperedRecovery_eq_add_of_params`) recovers
+`F(0) = Z(N)` modulo `2 ^ p` (`TensorNetwork.exists_recoverFromValues_eq_add`). Modulo `2 ^ p_t`,
+`F(t + α ζ)` is the deformed contraction of the reduced network along the Cauchy matrix at
+`T = t + α ζ` (`TensorNetwork.mk_eval_localDeformation`), which the child identity (D.16),
+`TensorNetwork.deformedContraction_cauchyValueMatrix_eq_sum`, writes as the sum over the mode tuples
+of the products of the contractions of the children. So the values may be computed from the
+children's contractions modulo `2 ^ p_t` (`TensorNetwork.exists_recoverFromValues_eq_add_of_mk`).
+
+**The packing bridge.** The orientation that the child identity needs is property (2) of
+Lemma D.3 for `Cslib.PacketPacking.Packing` (`TensorNetwork.packingGroup_src_tgt`), and the port
+counts of Lemma D.3 (3) are the group sizes that bound the children
+(`TensorNetwork.card_packingGroup_src`, `TensorNetwork.card_packingGroup_tgt`, with
+`TensorNetwork.ModeSplitting.mul_card_edges_child_le`).
+
+## Main definitions
+
+* `Cslib.Circuits.Frontier.integerHom`: the inclusion of `ℤ_(2)` into `B`.
+* `Cslib.Circuits.Frontier.recoverFromValues`: interpolation followed by tapered recovery.
+* `Cslib.Circuits.Frontier.TensorNetwork.packingGroup`: the group of a vertex in coordinate `i`
+  of a packing.
+
+## Main results
+
+* `Lagrange.exists_ringInterpolate_eq_add`: interpolating values that agree with a polynomial
+  modulo `π` gives a polynomial that agrees with it modulo `π`.
+* `Cslib.Circuits.Frontier.TensorNetwork.exists_recoverFromValues_eq_add`: recovery modulo
+  `2 ^ p` from values modulo `2 ^ p_t`.
+* `Cslib.Circuits.Frontier.TensorNetwork.mk_eval_localDeformation`: the values of the local
+  deformation modulo `2 ^ p_t` are deformed contractions along `cauchyValueMatrix`.
+* `Cslib.Circuits.Frontier.TensorNetwork.exists_recoverFromValues_eq_add_of_mk`: correctness of
+  one active call.
+* `Cslib.Circuits.Frontier.TensorNetwork.packingGroup_src_tgt`: the packing bridge, with
+  `packing_slot_lt`, `packing_slot_injective`, `card_packingGroup_src` and
+  `card_packingGroup_tgt`.
+* `Cslib.Circuits.Frontier.two_pow_padicValInt_dvd_and_not_dvd`: a node of valuation `i` meets
+  the divisibility hypotheses of the child identity.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.3 (p. 58),
+  §D.4.4–§D.4.7, pp. 60–64.
+-/
+
+public section
+
+open Polynomial Finset
+
+/-! ### Interpolation of congruent values -/
+
+namespace Lagrange
+
+variable {R ι : Type*} [CommRing R] [DecidableEq ι] {s : Finset ι} {v : ι → R}
+
+/-- **Interpolating congruent values.** At nodes with unit differences, if the values `r i` agree
+with a polynomial `f` of degree below `#s` modulo `π`, then so does every coefficient of their
+interpolant. -/
+theorem exists_ringInterpolate_eq_add (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j))
+    {f : R[X]} (hf : f.degree < #s) {π : R} {r : ι → R}
+    (hr : ∀ i ∈ s, ∃ c, r i = f.eval (v i) + π * c) :
+    ∃ g : R[X], ringInterpolate s v r = f + C π * g := by
+  choose! c hc using hr
+  refine ⟨∑ i ∈ s, C (c i) * ringBasis s v i, ?_⟩
+  rw [← sub_eq_iff_eq_add']
+  calc ringInterpolate s v r - f
+      = ringInterpolate s v r - ringInterpolate s v (fun i => f.eval (v i)) := by
+        rw [sub_right_inj]; exact eq_ringInterpolate hvs hf
+    _ = ringInterpolate s v (r - fun i => f.eval (v i)) := (map_sub _ _ _).symm
+    _ = ∑ i ∈ s, C (π * c i) * ringBasis s v i := by
+        rw [ringInterpolate_apply]
+        refine sum_congr rfl fun i hi => ?_
+        rw [Pi.sub_apply, hc i hi, add_sub_cancel_left]
+    _ = C π * ∑ i ∈ s, C (c i) * ringBasis s v i := by
+        rw [mul_sum]
+        exact sum_congr rfl fun i _ => by rw [C_mul, mul_assoc]
+
+end Lagrange
+
+namespace Cslib.Circuits.Frontier
+
+/-- The subring `ℤ_(2)` of rationals with odd denominator. -/
+local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
+
+variable {K : Type*} [CommRing K] [Algebra ℚ K]
+
+/-- The inclusion of `ℤ_(2)` into a subring `B` of a `ℚ`-algebra containing it. -/
+@[expose] noncomputable def integerHom (B : Subring K) (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) :
+    ℤ₍₂₎ →+* B :=
+  ((algebraMap ℚ K).comp (ℤ₍₂₎).subtype).codRestrict B fun c => hB c c.2
+
+theorem subtype_comp_integerHom (B : Subring K) (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) :
+    B.subtype.comp (integerHom B hB) = (algebraMap ℚ K).comp (ℤ₍₂₎).subtype :=
+  rfl
+
+/-- The value recovered at an active call from the values `v t k` at the interpolation points
+`ζ k`: interpolate over `B` at each node `t`, and apply tapered Hermite recovery (D.9). -/
+noncomputable def recoverFromValues (B : Subring K) (a u h : ℕ) {n : ℕ} (ζ : Fin n → B)
+    (v : ℤ → Fin n → B) : K :=
+  taperedRecovery a u h fun t => (Lagrange.ringInterpolate univ ζ (v t)).map B.subtype
+
+/-- A nonzero integer `t` of valuation `i` is divisible by `2 ^ i` but not by `2 ^ (i + 1)`. -/
+theorem two_pow_padicValInt_dvd_and_not_dvd {t : ℤ} (ht : t ≠ 0) :
+    (2 : ℤ) ^ padicValInt 2 t ∣ t ∧ ¬ (2 : ℤ) ^ (padicValInt 2 t + 1) ∣ t := by
+  refine ⟨by exact_mod_cast padicValInt_dvd (p := 2) t, fun h => ?_⟩
+  have := (padicValInt_dvd_iff (p := 2) (padicValInt 2 t + 1) t).mp (by exact_mod_cast h)
+  omega
+
+namespace TensorNetwork
+
+variable {V E P : Type*} [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P]
+
+/-- **Correctness of recovery from values.** Let `N` have entries in `B`, edges from rows to
+columns packed into packets of `2 ^ a` slots, and let `1 ≤ u ≤ M` and `3 M ≤ h u ≤ 3 M + u` for
+`M` edges. Let the `n > M (2 L - 1)` points `ζ k` have unit differences. If at every node `t` of
+positive multiplicity the values `v t k` agree with `F(t + α ζ k)` modulo `2 ^ p_t`,
+`p_t = p + 8 h D_t + 8 M (a + 1)`, then the recovered value agrees with the contraction modulo
+`2 ^ p`. -/
+theorem exists_recoverFromValues_eq_add (B : Subring K)
+    (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) (N : TensorNetwork B Bool V E) (side : V → Bool)
+    {a : ℕ} {packet : E → P} {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a)
+    (hinj : ∀ e e', packet e = packet e' → slot e = slot e' → e = e') {u h p : ℕ} (hu : 1 ≤ u)
+    (huM : u ≤ Fintype.card E) (hh : 3 * Fintype.card E ≤ h * u)
+    (hh' : h * u ≤ 3 * Fintype.card E + u) {n : ℕ} (ζ : Fin n → B)
+    (hζ : Pairwise fun k l => IsUnit (ζ k - ζ l)) (hn : Fintype.card E * (2 * 2 ^ a - 1) < n)
+    (v : ℤ → Fin n → B)
+    (hv : ∀ t ∈ recoveryNodes a, 0 < taperMult u h t → ∀ k, ∃ c : B,
+      v t k = (N.localDeformation side (integerHom B hB) a t packet slot).eval (ζ k) +
+        2 ^ (p + 8 * h * 2 ^ (a - padicValInt 2 t) + 8 * Fintype.card E * (a + 1)) * c) :
+    ∃ b ∈ B, recoverFromValues B a u h ζ v = (N.contraction : K) + 2 ^ p * b := by
+  have hF0 : (((N.map B.subtype).map C).deformedContraction side
+      ((cauchyMatrix (2 ^ a) packet slot).map (mapRingHom (algebraMap ℚ K)))).eval 0 =
+        (N.contraction : K) := by
+    rw [eval_zero_deformedContraction_cauchyMatrix _ side hslot hinj, contraction_map]
+    rfl
+  rw [← hF0]
+  refine exists_taperedRecovery_eq_add_of_params B hB hu huM hh hh'
+    (natDegree_deformedContraction_cauchyMatrix_le _ side hslot) _ fun t ht j hj => ?_
+  have htS : t ∈ cauchyGrid (2 ^ a) := mem_of_mem_erase ht
+  have hnat : (N.localDeformation side (integerHom B hB) a t packet slot).natDegree < n :=
+    (natDegree_localDeformation_le N side (integerHom B hB) hslot htS).trans_lt hn
+  have hdeg : (N.localDeformation side (integerHom B hB) a t packet slot).degree <
+      ↑(#(univ : Finset (Fin n))) := by
+    rw [card_univ, Fintype.card_fin]
+    exact (degree_le_natDegree).trans_lt (Nat.cast_lt.mpr hnat)
+  obtain ⟨g, hg⟩ := Lagrange.exists_ringInterpolate_eq_add (s := univ) (v := ζ)
+    (fun k _ l _ hkl => hζ hkl) hdeg
+    (π := 2 ^ (p + 8 * h * 2 ^ (a - padicValInt 2 t) + 8 * Fintype.card E * (a + 1)))
+    (fun k _ => hv t ht (by omega) k)
+  refine ⟨(g.coeff j : K), (g.coeff j).2, ?_⟩
+  rw [← map_localDeformation N side (integerHom B hB) B.subtype (subtype_comp_integerHom B hB)
+    hslot htS, coeff_map, coeff_map, hg, coeff_add, coeff_C_mul, map_add, map_mul, map_pow]
+  rfl
+
+/-! ### The packing bridge -/
+
+/-- The group of a vertex in coordinate `i` of a packing: its row label if it is a row and its
+column label if it is a column. -/
+@[expose] def packingGroup {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E) (side : V → Bool)
+    (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (v : V) : Fin r :=
+  if side v then Q.rowLabel v i else Q.colLabel v i
+
+omit [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] in
+/-- **The packing bridge.** For a packing of the edges of a network whose edges run from rows to
+columns (Lemma D.3 of [OpenAI2026ETH]), the groups in coordinate `i` are oriented by digit `i` of
+the slots (Lemma D.3 (2)): the hypothesis of `TensorNetwork.cauchyModeSplitting`. -/
+theorem packingGroup_src_tgt {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E)
+    (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false)
+    (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (e : E) :
+    (packingGroup N side Q i (N.src e), packingGroup N side Q i (N.tgt e)) =
+      if (Q.slot e : ℕ).testBit i then (Q.symbols (Q.packet e) i).swap
+      else Q.symbols (Q.packet e) i := by
+  simp only [packingGroup, hsrc, htgt, ↓reduceIte, Bool.false_eq_true]
+  exact Q.labels_eq e i
+
+omit [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] in
+/-- The slots of a packing lie below `2 ^ a`. -/
+theorem packing_slot_lt {R : Type*} {a r : ℕ} {N : TensorNetwork R Bool V E}
+    (Q : PacketPacking.Packing N.src N.tgt a r) (e : E) : (Q.slot e : ℕ) < 2 ^ a :=
+  (Q.slot e).isLt
+
+omit [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] in
+/-- No two edges share a slot of a packet. -/
+theorem packing_slot_injective {R : Type*} {a r : ℕ} {N : TensorNetwork R Bool V E}
+    (Q : PacketPacking.Packing N.src N.tgt a r) (e e' : E) (hp : Q.packet e = Q.packet e')
+    (hs : (Q.slot e : ℕ) = Q.slot e') : e = e' :=
+  Q.injective (Prod.ext hp (Fin.ext hs))
+
+omit [Fintype V] [DecidableEq E] [DecidableEq P] in
+/-- The rows of group `σ` in coordinate `i` of a packing are the rows with symbol `σ`. -/
+theorem card_packingGroup_src {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E)
+    (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true)
+    (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (σ : Fin r) :
+    #{e | packingGroup N side Q i (N.src e) = σ} = #{e | Q.rowLabel (N.src e) i = σ} := by
+  simp only [packingGroup, hsrc, ↓reduceIte]
+
+omit [Fintype V] [DecidableEq E] [DecidableEq P] in
+/-- The columns of group `σ` in coordinate `i` of a packing are the columns with symbol `σ`. -/
+theorem card_packingGroup_tgt {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E)
+    (side : V → Bool) (htgt : ∀ e, side (N.tgt e) = false)
+    (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (σ : Fin r) :
+    #{e | packingGroup N side Q i (N.tgt e) = σ} = #{e | Q.colLabel (N.tgt e) i = σ} := by
+  simp only [packingGroup, htgt, Bool.false_eq_true, ↓reduceIte]
+
+/-- **The values of the local deformation modulo `2 ^ p_t`** are deformed contractions of the
+reduced network along the Cauchy matrix at `T = t + α ζ` (which the child identity (D.16),
+`TensorNetwork.deformedContraction_cauchyValueMatrix_eq_sum`, expands). -/
+theorem mk_eval_localDeformation {B : Type*} [CommRing B] (N : TensorNetwork B Bool V E)
+    (side : V → Bool) (κ : ℤ₍₂₎ →+* B) (a : ℕ) (t : ℤ) (packet : E → P) (slot : E → ℕ)
+    (I : Ideal B) (ζ : B) :
+    Ideal.Quotient.mk I ((N.localDeformation side κ a t packet slot).eval ζ) =
+      (N.map (Ideal.Quotient.mk I)).deformedContraction side
+        (cauchyValueMatrix ((Ideal.Quotient.mk I).comp κ) (Ideal.Quotient.mk I ζ) a t packet
+          slot) := by
+  rw [← eval₂_hom, eval₂_localDeformation]
+
+/-- **Correctness of one active call** ([OpenAI2026ETH], §D.4.4–§D.4.7). Under the hypotheses of
+`exists_recoverFromValues_eq_add`, suppose that at every node `t` of positive multiplicity, each
+value `v t k` reduces modulo `2 ^ p_t` to the deformed contraction of the reduced network along the
+Cauchy matrix at `T = t + α ζ k`, `p_t = p + 8 h D_t + 8 M (a + 1)`: by the child identity (D.16),
+the sum over the mode tuples of the products of the contractions of the children. Then the
+recovered value agrees with the contraction modulo `2 ^ p`. -/
+theorem exists_recoverFromValues_eq_add_of_mk (B : Subring K)
+    (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) (N : TensorNetwork B Bool V E) (side : V → Bool)
+    {a : ℕ} {packet : E → P} {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a)
+    (hinj : ∀ e e', packet e = packet e' → slot e = slot e' → e = e') {u h p : ℕ} (hu : 1 ≤ u)
+    (huM : u ≤ Fintype.card E) (hh : 3 * Fintype.card E ≤ h * u)
+    (hh' : h * u ≤ 3 * Fintype.card E + u) {n : ℕ} (ζ : Fin n → B)
+    (hζ : Pairwise fun k l => IsUnit (ζ k - ζ l)) (hn : Fintype.card E * (2 * 2 ^ a - 1) < n)
+    (v : ℤ → Fin n → B)
+    (hv : ∀ t ∈ recoveryNodes a, 0 < taperMult u h t → ∀ k,
+      let I := Ideal.span {(2 : B) ^ (p + 8 * h * 2 ^ (a - padicValInt 2 t) +
+        8 * Fintype.card E * (a + 1))}
+      Ideal.Quotient.mk I (v t k) =
+        (N.map (Ideal.Quotient.mk I)).deformedContraction side
+          (cauchyValueMatrix ((Ideal.Quotient.mk I).comp (integerHom B hB))
+            (Ideal.Quotient.mk I (ζ k)) a t packet slot)) :
+    ∃ b ∈ B, recoverFromValues B a u h ζ v = (N.contraction : K) + 2 ^ p * b := by
+  refine exists_recoverFromValues_eq_add B hB N side hslot hinj hu huM hh hh' ζ hζ hn v
+    fun t ht hq k => ?_
+  have h1 := hv t ht hq k
+  simp only at h1
+  rw [← mk_eval_localDeformation, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at h1
+  obtain ⟨c, hc⟩ := h1
+  exact ⟨c, by rw [mul_comm, hc, add_sub_cancel]⟩
+
+end TensorNetwork
+
+end Cslib.Circuits.Frontier
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/CauchyModes.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/CauchyModes.lean
index 77494386cd..556464fe44 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/CauchyModes.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/CauchyModes.lean
@@ -585,6 +585,33 @@ noncomputable def cauchyModeSplitting (side : V → Bool) (hsrc : ∀ e, side (N
       simp
     rw [group_tgt_eq horient e, hb, hq]
 
+section Fields
+
+variable (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true)
+  (htgt : ∀ e, side (N.tgt e) = false)
+  (horient : ∀ e, (group (N.src e), group (N.tgt e)) =
+    if (slot e).testBit i then (sym (packet e)).swap else sym (packet e))
+  {a : ℕ} (hslot : ∀ e, slot e < 2 ^ a) (hia : i < a) (κ : ℤ₍₂₎ →+* R) (ζ : R) {p : ℕ}
+  (hp : (2 : R) ^ p = 0) {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) (hti : (2 : ℤ) ^ i ∣ t)
+  (hti' : ¬ (2 : ℤ) ^ (i + 1) ∣ t)
+
+omit [Fintype E] in
+@[simp] theorem cauchyModeSplitting_side :
+    (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').side = side := by
+  unfold cauchyModeSplitting; rfl
+
+omit [Fintype E] in
+@[simp] theorem cauchyModeSplitting_group :
+    (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group = group := by
+  unfold cauchyModeSplitting; rfl
+
+omit [Fintype E] in
+@[simp] theorem cauchyModeSplitting_packet :
+    (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').packet = packet := by
+  unfold cauchyModeSplitting; rfl
+
+end Fields
+
 omit [Fintype E] [Fintype P] in
 /-- **The modes have weight `b + 1`:** the coefficient of the mode `(q, y₀, b)` is divisible by
 `2 ^ (b + 1)`, so the child identity (D.16) applies with these weights. -/
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean
new file mode 100644
index 0000000000..390e7d8943
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean
@@ -0,0 +1,131 @@
+/-
+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.ModeExpansion
+import Mathlib.Data.Fintype.Sum
+
+/-!
+# Sizes of the child networks
+
+The child networks of a mode splitting (`TensorNetwork.ModeSplitting.child`, §D.4.6 of
+[OpenAI2026ETH], p. 63) keep the invariants of the recursion:
+
+* an old vertex keeps its degree (`ModeSplitting.card_child_src_inl`);
+* a packet vertex has one port for each port of its group in its packet
+  (`ModeSplitting.card_child_tgt_inr`), so at most `2 L` ports when no two edges share a slot of a
+  packet of `L` slots (`ModeSplitting.card_child_tgt_inr_le`): the manuscript's
+  "a new packet vertex has at most `2L ⩽ Δ` ports";
+* the child has one edge per port of its group (`ModeSplitting.card_edges_child`), so with at most
+  `c M / r` ports per group on each side (Lemma D.3 (3)) it has at most `2 c M / r` edges
+  (`ModeSplitting.mul_card_edges_child_le`): the manuscript's "at most `6M / r < M / 8` edges".
+
+## Main results
+
+* `Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting.card_child_src_inl`: old degrees are
+  unchanged.
+* `Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting.card_child_tgt_inr_le`: packet degrees are
+  at most `2 L`.
+* `Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting.mul_card_edges_child_le`: the edge bound.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.3 (pp. 58–59) and
+  §D.4.6 (p. 63).
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting
+
+open Finset
+
+variable {R V E G P M : Type*} [CommRing R] [Fintype M] {N : TensorNetwork R Bool V E}
+  {W : Matrix E E R} (S : N.ModeSplitting W G P M) [Fintype E] [DecidableEq E] [DecidableEq P]
+  [DecidableEq G] [DecidableEq M] [DecidableEq V]
+
+/-- Counting the elements of a sum type with a property. -/
+private theorem card_filter_sum {A B : Type*} [Fintype A] [Fintype B] (p : A ⊕ B → Prop)
+    [DecidablePred p] :
+    #{x | p x} = #{a | p (.inl a)} + #{b | p (.inr b)} := by
+  rw [← Fintype.card_subtype, Fintype.card_congr Equiv.subtypeSum, Fintype.card_sum,
+    Fintype.card_subtype, Fintype.card_subtype]
+
+/-- Counting the elements of a subtype with a property. -/
+private theorem card_filter_subtype {A : Type*} [Fintype A] (Q : A → Prop) [DecidablePred Q]
+    (f : A → Prop) [DecidablePred f] : #{e : {e // Q e} | f e.1} = #{e | Q e ∧ f e} := by
+  rw [← Fintype.card_subtype, Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter Q f),
+    Fintype.card_subtype]
+
+/-- **Old degrees are unchanged.** In a child, an old vertex has one port for each edge of `N`
+at it. -/
+theorem card_child_src_inl (β : M → ℕ) (g : G) (v : {v // S.group v = g}) :
+    #{x | (S.child β g).src x = .inl v} = #{e | N.src e = v.1} + #{e | N.tgt e = v.1} := by
+  rw [card_filter_sum]
+  congr 1
+  · simp only [child_src_inl, Sum.inl.injEq, Subtype.ext_iff]
+    rw [card_filter_subtype (fun e => S.group (N.src e) = g) (fun e => N.src e = v.1)]
+    exact congrArg card (filter_congr fun e _ => ⟨fun h => h.2, fun h => ⟨h ▸ v.2, h⟩⟩)
+  · simp only [child_src_inr, Sum.inl.injEq, Subtype.ext_iff]
+    rw [card_filter_subtype (fun e => S.group (N.tgt e) = g) (fun e => N.tgt e = v.1)]
+    exact congrArg card (filter_congr fun e _ => ⟨fun h => h.2, fun h => ⟨h ▸ v.2, h⟩⟩)
+
+/-- Every edge of a child ends at a packet vertex. -/
+theorem card_child_tgt_inl (β : M → ℕ) (g : G) (v : {v // S.group v = g}) :
+    #{x | (S.child β g).tgt x = .inl v} = 0 := by
+  rw [card_filter_sum]
+  simp
+
+/-- Every edge of a child starts at an old vertex. -/
+theorem card_child_src_inr (β : M → ℕ) (g : G) (q : P) :
+    #{x | (S.child β g).src x = .inr q} = 0 := by
+  rw [card_filter_sum]
+  simp
+
+/-- A packet vertex of a child has one port for each port of its group in its packet. -/
+theorem card_child_tgt_inr (β : M → ℕ) (g : G) (q : P) :
+    #{x | (S.child β g).tgt x = .inr q} =
+      #{e | S.group (N.src e) = g ∧ S.packet e = q} +
+        #{e | S.group (N.tgt e) = g ∧ S.packet e = q} := by
+  rw [card_filter_sum]
+  simp only [child_tgt_inl, child_tgt_inr, Sum.inr.injEq]
+  rw [card_filter_subtype (fun e => S.group (N.src e) = g) (fun e => S.packet e = q),
+    card_filter_subtype (fun e => S.group (N.tgt e) = g) (fun e => S.packet e = q)]
+
+omit [DecidableEq E] [DecidableEq G] [DecidableEq M] [DecidableEq V] in
+/-- At most `L` edges lie in a packet of `L` slots when no two share a slot. -/
+private theorem card_packet_le {a : ℕ} {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a)
+    (hinj : ∀ e e', S.packet e = S.packet e' → slot e = slot e' → e = e') (q : P)
+    (f : E → Prop) [DecidablePred f] : #{e | f e ∧ S.packet e = q} ≤ 2 ^ a := by
+  calc #{e | f e ∧ S.packet e = q} ≤ #(range (2 ^ a)) :=
+        card_le_card_of_injOn slot (fun e _ => by simpa using hslot e) fun e he e' he' h => by
+          simp only [coe_filter, Set.mem_ofPred_eq, mem_univ, true_and] at he he'
+          exact hinj e e' (he.2.trans he'.2.symm) h
+    _ = 2 ^ a := card_range _
+
+/-- **Packet degrees are at most `2 L`** in a child, for packets of `L = 2 ^ a` slots with no two
+edges in the same slot of a packet. -/
+theorem card_child_tgt_inr_le {a : ℕ} {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a)
+    (hinj : ∀ e e', S.packet e = S.packet e' → slot e = slot e' → e = e') (β : M → ℕ) (g : G)
+    (q : P) : #{x | (S.child β g).tgt x = .inr q} ≤ 2 * 2 ^ a := by
+  rw [card_child_tgt_inr, two_mul]
+  exact add_le_add (S.card_packet_le hslot hinj q _) (S.card_packet_le hslot hinj q _)
+
+omit [DecidableEq E] [DecidableEq P] [DecidableEq M] [DecidableEq V] in
+/-- **The edge bound.** If, in the group `g`, the rows have at most `c M / r` ports and so do the
+columns, then the child of `g` has at most `2 c M / r` edges. With Lemma D.3 (3), `c = 3` and
+`r = 64`, this is the manuscript's `6M / r < M / 8`. -/
+theorem mul_card_edges_child_le {r c : ℕ} (g : G)
+    (hrow : r * #{e | S.group (N.src e) = g} ≤ c * Fintype.card E)
+    (hcol : r * #{e | S.group (N.tgt e) = g} ≤ c * Fintype.card E) :
+    r * Fintype.card ({e // S.group (N.src e) = g} ⊕ {e // S.group (N.tgt e) = g}) ≤
+      2 * c * Fintype.card E := by
+  rw [card_edges_child, mul_add]
+  linarith
+
+end Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean
new file mode 100644
index 0000000000..dd0a261b1e
--- /dev/null
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: local-only (test driver)
+
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ActiveCall
+
+/-!
+# Tests for one active call of the contraction recursion
+
+* **The packing bridge.** The two-edge network of the Cauchy-mode tests with a hand-made packing
+  into one packet of two slots (`a = 1`, `r = 2`) satisfies the orientation hypothesis of the
+  child identity, its groups have one port per side, and the children of a mode splitting along
+  its packets have packet degree at most `2 L`.
+* **Non-vacuity of the active call.** A one-edge network over `ℤ_(2)` (`M = 1`, `a = 0`, so
+  `M (2 L - 1) = 1`), with the two interpolation points `0` and `1`, `u = 1` and `h = 3`: values
+  equal to `F(t + α ζ)` recover the contraction modulo every `2 ^ p`.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.ActiveCall
+
+open Cslib.Circuits.Frontier TensorNetwork
+
+/-- The subring `ℤ_(2)` of rationals with odd denominator. -/
+local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
+
+/-! ### The packing bridge -/
+
+/-- Edge `e` runs from row `e` to column `e + 2`, with the all-one tensors. -/
+def net : TensorNetwork ℤ Bool (Fin 4) (Fin 2) where
+  src e := ⟨e.val, by omega⟩
+  tgt e := ⟨e.val + 2, by omega⟩
+  tensor _ _ := 1
+  tensor_congr _ _ _ _ := rfl
+
+/-- The rows `0, 1`. -/
+def side (v : Fin 4) : Bool := decide (v.val < 2)
+
+/-- One packet of two slots; edge `e` in slot `e`. Row `1` and column `2` have symbol `1`, so
+edge `0` (slot `0`) runs from symbol `0` to `1` and edge `1` (slot `1`) the other way. -/
+def packing : Cslib.PacketPacking.Packing net.src net.tgt 1 2 where
+  rowLabel v _ := if v = 1 then 1 else 0
+  colLabel v _ := if v = 2 then 1 else 0
+  numPackets := 1
+  packet _ := 0
+  slot e := ⟨e.val, by have := e.isLt; simp; omega⟩
+  symbols _ _ := (0, 1)
+  injective e e' h := by fin_cases e <;> fin_cases e' <;> simp_all
+  labels_eq e i := by fin_cases e <;> fin_cases i <;> decide
+
+example (e : Fin 2) :
+    (packingGroup net side packing 0 (net.src e), packingGroup net side packing 0 (net.tgt e)) =
+      if (packing.slot e : ℕ).testBit 0 then (packing.symbols (packing.packet e) 0).swap
+      else packing.symbols (packing.packet e) 0 :=
+  packingGroup_src_tgt net side (fun e => by fin_cases e <;> decide)
+    (fun e => by fin_cases e <;> decide) packing 0 e
+
+example : Finset.card {e | packingGroup net side packing 0 (net.src e) = 1} = 1 := by
+  rw [card_packingGroup_src net side (fun e => by fin_cases e <;> decide)]
+  decide
+
+/-- **Child invariants.** For any mode splitting of `net` along the packets of `packing`, a packet
+vertex of a child has at most `2 L = 4` ports. -/
+example {M : Type} [Fintype M] [DecidableEq M] {W : Matrix (Fin 2) (Fin 2) ℤ}
+    (S : net.ModeSplitting W (Fin 2) (Fin 1) M) (hS : S.packet = packing.packet) (β : M → ℕ)
+    (g : Fin 2) (q : Fin 1) :
+    Finset.card {x | (S.child β g).tgt x = .inr q} ≤ 2 * 2 ^ 1 :=
+  S.card_child_tgt_inr_le (packing_slot_lt packing)
+    (by rw [hS]; exact packing_slot_injective packing) β g q
+
+/-! ### Non-vacuity of the active call -/
+
+/-- One edge from row `0` to column `1`, with tensor `(1, 2)` at the row and `(1, 1)` at the
+column. -/
+def net₁ : TensorNetwork ℤ₍₂₎ Bool (Fin 2) (Fin 1) where
+  src _ := 0
+  tgt _ := 1
+  tensor v x := if v = 0 ∧ x 0 then 2 else 1
+  tensor_congr v x y h := by rw [h 0 (by fin_cases v <;> simp)]
+
+/-- The interpolation points `0, 1`, whose difference is a unit. -/
+def ζ (k : Fin 2) : ℤ₍₂₎ := k.val
+
+theorem hζ : Pairwise fun k l => IsUnit (ζ k - ζ l) := by
+  intro k l hkl
+  fin_cases k <;> fin_cases l
+  · exact absurd rfl hkl
+  · simp [ζ]
+  · simp [ζ]
+  · exact absurd rfl hkl
+
+/-- Exact values of `F(t + α ζ)` recover the contraction modulo every `2 ^ p`. -/
+example (p : ℕ) : ∃ b ∈ ℤ₍₂₎,
+    recoverFromValues ℤ₍₂₎ 0 1 3 ζ (fun t k =>
+      (net₁.localDeformation (fun v => decide (v = 0)) (integerHom ℤ₍₂₎ fun _ hc => hc) 0 t
+        (fun _ => ()) (fun _ => 0)).eval (ζ k)) =
+      ((net₁.contraction : ℤ₍₂₎) : ℚ) + 2 ^ p * b :=
+  exists_recoverFromValues_eq_add_of_mk (K := ℚ) ℤ₍₂₎ (fun _ hc => hc) net₁ _
+    (fun _ => by decide) (fun e e' _ _ => Subsingleton.elim e e') le_rfl le_rfl (by simp)
+    (by simp) ζ hζ (by simp) _ fun t _ _ k =>
+      mk_eval_localDeformation net₁ _ _ 0 t _ _ _ (ζ k)
+
+end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.ActiveCall