diff --git a/Complexity.lean b/Complexity.lean
index 12dd9699ed..db991b7aa6 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -881,7 +881,9 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformatio
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery
 public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness
 public import Complexity.Computability.Circuit.Frontier.Unconditional
 public import Complexity.Computability.Circuit.Frontier.Witness
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/LocalDeformation.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/LocalDeformation.lean
new file mode 100644
index 0000000000..5f497f546d
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/LocalDeformation.lean
@@ -0,0 +1,223 @@
+/-
+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.CauchyModes
+
+/-!
+# The deformed contraction in local coordinates
+
+This file connects the polynomial `F(T)` of (D.8) in [OpenAI2026ETH] (§D.4.3, p. 59) with its
+values at the interpolation points of §D.4.4–§D.4.5 (pp. 61–62).
+
+Let `B` be a commutative ring receiving `ℤ_(2)` through `κ`, and let `N` be a Boolean tensor network
+with entries in `B`. For a packing of the edges into packets of `2 ^ a` slots and a grid point `t`,
+the *local deformation* (`TensorNetwork.localDeformation`) is the deformed contraction of `N` along
+the matrix of local kernels `W_{y - x}(t + α z)` over `B[z]` (`cauchyLocalMatrix`), built from
+`Cslib.Circuits.Frontier.localKernel`. It is the manuscript's `F(t + α z) ∈ A[z]`:
+
+* in a `ℚ`-algebra `R` receiving `B` compatibly with `ℚ`, its image is `F(t + α z)`, where `F(T)`
+  is the deformed contraction along the Cauchy matrix
+  (`TensorNetwork.map_localDeformation`), whose value at `0` is the contraction
+  (`TensorNetwork.eval_zero_deformedContraction_cauchyMatrix`);
+* under any ring homomorphism `π : B → R'`, its value at `z = ζ` is the deformed contraction of the
+  reduced network along the Cauchy matrix at `T = t + α ζ`
+  (`TensorNetwork.eval₂_localDeformation`), which the child identity
+  `TensorNetwork.deformedContraction_cauchyValueMatrix_eq_sum` expands when `2 ^ p = 0` in `R'`.
+
+So the values of the children of §D.4.6 at `ζ` are values of one polynomial over `B`, and
+interpolation recovers its reduction.
+
+## Main definitions
+
+* `Cslib.Circuits.Frontier.cauchyLocalMatrix`: the Cauchy matrix of a packing in local
+  coordinates, over `B[z]`.
+* `Cslib.Circuits.Frontier.TensorNetwork.localDeformation`: `F(t + α z)` over `B`.
+
+## Main results
+
+* `Cslib.Circuits.Frontier.TensorNetwork.map_localDeformation`: its image in a `ℚ`-algebra is
+  `F(t + α z)`.
+* `Cslib.Circuits.Frontier.TensorNetwork.eval₂_localDeformation`: its values are deformed
+  contractions along `cauchyValueMatrix`.
+* `Cslib.Circuits.Frontier.TensorNetwork.natDegree_deformedContraction_le`,
+  `Cslib.Circuits.Frontier.TensorNetwork.natDegree_localDeformation_le`,
+  `Cslib.Circuits.Frontier.TensorNetwork.natDegree_deformedContraction_cauchyMatrix_le`: both have
+  degree at most `M (2 L - 1)` for `M` edges and `L` slots.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.3–§D.4.5,
+  pp. 59–62.
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier
+
+open Polynomial
+
+/-- The subring `ℤ_(2)` of rationals with odd denominator. -/
+local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
+
+variable {B V E P : Type*} [CommRing B]
+
+/-- The Cauchy matrix of a packing into packets of `2 ^ a` slots in local coordinates
+`z ↦ W(t + α z)`, `α = 2 ^ (a + 1)`, over `B[z]` for a ring `B` receiving `ℤ_(2)` through `κ`:
+between two edges of the same packet, the local kernel at the difference of their slots, and zero
+between packets. -/
+@[expose] noncomputable def cauchyLocalMatrix [DecidableEq P] (κ : ℤ₍₂₎ →+* B) (a : ℕ) (t : ℤ)
+    (packet : E → P) (slot : E → ℕ) : Matrix E E B[X] :=
+  fun e e' =>
+    if packet e = packet e' then (localKernel a t ((slot e' : ℤ) - slot e)).map κ else 0
+
+namespace TensorNetwork
+
+/-- Mapping the tensors twice is mapping them by the composition. -/
+theorem map_map {R S T U : Type*} [CommSemiring R] [CommSemiring S] [CommSemiring T]
+    (f : R →+* S) (g : S →+* T) (N : TensorNetwork R U V E) : (N.map f).map g = N.map (g.comp f) :=
+  rfl
+
+variable [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P]
+
+/-- The deformed contraction along the Cauchy matrix of a packing in local coordinates at the grid
+point `t`, as a polynomial in `z` over `B`: the manuscript's `F(t + α z) ∈ A[z]`. -/
+@[expose] noncomputable def localDeformation (N : TensorNetwork B Bool V E) (side : V → Bool)
+    (κ : ℤ₍₂₎ →+* B) (a : ℕ) (t : ℤ) (packet : E → P) (slot : E → ℕ) : B[X] :=
+  (N.map C).deformedContraction side (cauchyLocalMatrix κ a t packet slot)
+
+/-- **The local deformation is `F(t + α z)`.** In a `ℚ`-algebra `R` receiving `B` through `ι`
+compatibly with `ℚ`, the image of the local deformation at a grid point `t` is the deformed
+contraction `F(T)` along the Cauchy matrix, composed with `T = t + α z`. -/
+theorem map_localDeformation {R : Type*} [CommRing R] [Algebra ℚ R] (N : TensorNetwork B Bool V E)
+    (side : V → Bool) (κ : ℤ₍₂₎ →+* B) (ι : B →+* R)
+    (hκ : ι.comp κ = (algebraMap ℚ R).comp (ℤ₍₂₎).subtype) {a : ℕ} {packet : E → P}
+    {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a) {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) :
+    (N.localDeformation side κ a t packet slot).map ι =
+      (((N.map ι).map C).deformedContraction side
+        ((cauchyMatrix (2 ^ a) packet slot).map (mapRingHom (algebraMap ℚ R)))).comp
+          (C (t : R) + C (2 ^ (a + 1)) * X) := by
+  rw [← coe_mapRingHom, localDeformation, ← deformedContraction_map, ← coe_compRingHom_apply,
+    ← deformedContraction_map, map_map, map_map, map_map]
+  have hlin : (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X).map (algebraMap ℚ R) =
+      C (t : R) + C (2 ^ (a + 1)) * X := by
+    rw [Polynomial.map_add, Polynomial.map_mul, Polynomial.map_C, Polynomial.map_C,
+      Polynomial.map_X, map_intCast, map_pow, map_ofNat]
+  congr 1
+  · congr 1
+    ext x : 1
+    simp only [RingHom.coe_comp, Function.comp_apply, coe_mapRingHom, Polynomial.map_C,
+      coe_compRingHom_apply, C_comp]
+  · ext e e'
+    simp only [Matrix.map_apply, cauchyLocalMatrix, cauchyMatrix, coe_mapRingHom,
+      coe_compRingHom_apply]
+    split_ifs with hp
+    · rw [Polynomial.map_map, hκ, ← Polynomial.map_map,
+        map_localKernel ht (sub_mem_cauchyGrid (hslot e) (hslot e')), Polynomial.map_comp, hlin]
+    · rw [Polynomial.map_zero, Polynomial.map_zero, zero_comp]
+
+/-- **Values of the local deformation.** Under a ring homomorphism `π : B → R'`, the value of the
+local deformation at `z = ζ` is the deformed contraction of the reduced network along the Cauchy
+matrix at `T = t + α ζ`. -/
+theorem eval₂_localDeformation {R' : Type*} [CommRing R'] (N : TensorNetwork B Bool V E)
+    (side : V → Bool) (κ : ℤ₍₂₎ →+* B) (π : B →+* R') (ζ : R') (a : ℕ) (t : ℤ) (packet : E → P)
+    (slot : E → ℕ) :
+    (N.localDeformation side κ a t packet slot).eval₂ π ζ =
+      (N.map π).deformedContraction side (cauchyValueMatrix (π.comp κ) ζ a t packet slot) := by
+  rw [← coe_eval₂RingHom, localDeformation, ← deformedContraction_map, map_map]
+  congr 1
+  · congr 1
+    ext x : 1
+    simp only [RingHom.coe_comp, Function.comp_apply, coe_eval₂RingHom, eval₂_C]
+  · ext e e'
+    simp only [Matrix.map_apply, cauchyLocalMatrix, cauchyValueMatrix, coe_eval₂RingHom]
+    split_ifs
+    · rw [eval₂_map]
+      rfl
+    · exact eval₂_zero _ _
+
+/-! ### Degrees -/
+
+/-- **Degree of a deformed contraction.** For tensors that are constants and a matrix whose entries
+have degree at most `d`, the deformed contraction has degree at most `d` times the number of
+edges: it is a sum of products of one affine factor per edge. -/
+theorem natDegree_deformedContraction_le {R : Type*} [CommRing R] (N : TensorNetwork R Bool V E)
+    (side : V → Bool) (W : Matrix E E R[X]) {d : ℕ} (hW : ∀ e e', (W e e').natDegree ≤ d) :
+    ((N.map C).deformedContraction side W).natDegree ≤ Fintype.card E * d := by
+  unfold deformedContraction
+  refine natDegree_sum_le_of_forall_le _ _ fun X _ => natDegree_sum_le_of_forall_le _ _
+    fun Y _ => ?_
+  have hc : ∀ s : Finset V, ∀ x : E → Bool, (∏ v ∈ s, (N.map C).tensor v x).natDegree = 0 :=
+    fun s x => by simp only [map_tensor, ← map_prod, natDegree_C]
+  have hv : ∀ e, (W.mulVec (fun e' => if X e' then (1 : R[X]) else 0) e).natDegree ≤ d := by
+    intro e
+    refine natDegree_sum_le_of_forall_le _ _ fun e' _ => ?_
+    dsimp only
+    split_ifs
+    · rw [mul_one]; exact hW e e'
+    · rw [mul_zero, natDegree_zero]; exact Nat.zero_le _
+  have hprod : (∏ e, affineFactor (Y e)
+      (W.mulVec (fun e' => if X e' then (1 : R[X]) else 0) e)).natDegree ≤ Fintype.card E * d := by
+    refine (natDegree_prod_le _ _).trans ?_
+    rw [← smul_eq_mul, ← Finset.card_univ, ← Finset.sum_const]
+    refine Finset.sum_le_sum fun e _ => ?_
+    unfold affineFactor
+    split_ifs
+    · exact hv e
+    · exact (natDegree_sub_le _ _).trans (max_le (by rw [natDegree_one]; exact Nat.zero_le _)
+        (hv e))
+  refine (natDegree_mul_le).trans ?_
+  have h2 := natDegree_mul_le (p := ∏ v ∈ Finset.univ.filter (side · = true), (N.map C).tensor v Y)
+    (q := ∏ v ∈ Finset.univ.filter (side · = false), (N.map C).tensor v X)
+  rw [hc, hc] at h2
+  omega
+
+/-- On the grid, the local kernel has degree at most `2 L - 1`, `L = 2 ^ a`. -/
+theorem natDegree_localKernel_le {a : ℕ} {t d : ℤ} (ht : t ∈ cauchyGrid (2 ^ a))
+    (hd : d ∈ cauchyGrid (2 ^ a)) : (localKernel a t d).natDegree ≤ 2 * 2 ^ a - 1 := by
+  rw [← natDegree_map_eq_of_injective (f := (ℤ₍₂₎).subtype) Subtype.val_injective,
+    map_localKernel ht hd]
+  refine natDegree_comp_le.trans ?_
+  rw [natDegree_cauchyKernel hd]
+  have : (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X).natDegree ≤ 1 :=
+    (natDegree_add_le _ _).trans (max_le (by rw [natDegree_C]; exact Nat.zero_le _)
+      ((natDegree_C_mul_le _ _).trans natDegree_X_le))
+  calc (2 * 2 ^ a - 1) * (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X).natDegree
+      ≤ (2 * 2 ^ a - 1) * 1 := Nat.mul_le_mul_left _ this
+    _ = 2 * 2 ^ a - 1 := mul_one _
+
+/-- The local deformation has degree at most `M (2 L - 1)` for `M` edges. -/
+theorem natDegree_localDeformation_le (N : TensorNetwork B Bool V E) (side : V → Bool)
+    (κ : ℤ₍₂₎ →+* B) {a : ℕ} {packet : E → P} {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a)
+    {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) :
+    (N.localDeformation side κ a t packet slot).natDegree ≤ Fintype.card E * (2 * 2 ^ a - 1) := by
+  refine natDegree_deformedContraction_le N side _ fun e e' => ?_
+  unfold cauchyLocalMatrix
+  split_ifs
+  · exact natDegree_map_le.trans
+      (natDegree_localKernel_le ht (sub_mem_cauchyGrid (hslot e) (hslot e')))
+  · rw [natDegree_zero]; exact Nat.zero_le _
+
+/-- The deformed contraction `F(T)` along the Cauchy matrix of a packing into packets of `L` slots
+has degree at most `M (2 L - 1)` for `M` edges (§D.4.3 of [OpenAI2026ETH], p. 59). -/
+theorem natDegree_deformedContraction_cauchyMatrix_le {R : Type*} [CommRing R] [Algebra ℚ R]
+    (N : TensorNetwork R Bool V E) (side : V → Bool) {L : ℕ} {packet : E → P} {slot : E → ℕ}
+    (hslot : ∀ e, slot e < L) :
+    ((N.map C).deformedContraction side
+        ((cauchyMatrix L packet slot).map (mapRingHom (algebraMap ℚ R)))).natDegree ≤
+      Fintype.card E * (2 * L - 1) := by
+  refine natDegree_deformedContraction_le N side _ fun e e' => ?_
+  simp only [Matrix.map_apply, cauchyMatrix, coe_mapRingHom]
+  split_ifs
+  · exact natDegree_map_le.trans
+      (natDegree_cauchyKernel (sub_mem_cauchyGrid (hslot e) (hslot e'))).le
+  · rw [Polynomial.map_zero, natDegree_zero]; exact Nat.zero_le _
+
+end TensorNetwork
+
+end Cslib.Circuits.Frontier
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TaperedRecovery.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TaperedRecovery.lean
new file mode 100644
index 0000000000..4d914e4644
--- /dev/null
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TaperedRecovery.lean
@@ -0,0 +1,475 @@
+/-
+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.IntegralCoordinates
+public import Complexity.Foundations.Data.Polynomial.TaperedHermite
+import Mathlib.Algebra.Polynomial.Eval.Degree
+import Mathlib.RingTheory.PowerSeries.Trunc
+
+/-!
+# Tapered Hermite recovery with finite precision
+
+This file finishes Lemma D.5 of [OpenAI2026ETH] (§D.4.4, pp. 60–61): the value `F(0)` modulo
+`2 ^ p` is recovered from the local jets of `F(t + α z)` modulo `2 ^ p_t`.
+
+**Setting.** Let `K` be a `ℚ`-algebra and `B` a subring of `K` containing `ℤ_(2)`, the rationals
+with odd denominator (in the manuscript, `K = ℚ[U] / (f)` and `B = O`). The nodes are the nonzero
+points `t` of the grid `S = [-L, L)` of `L = 2 ^ a` slots (`recoveryNodes`), with the tapered
+multiplicities `q_t = h max(0, u - v₂ t)` (`taperMult`), and `α = 2 ^ (a + 1)`. From polynomials
+`G t ∈ K[z]`, the recovered value (`taperedRecovery`) is the right side of (D.9),
+
+  `∑_t E_t(0) (G t / E_t(t + α z) mod z ^ q_t)(-t / α)`,
+
+with the Hermite basis `E_t` and quotient of
+`Polynomial.eval_eq_sum_hermiteBasis_mul_hermiteQuotient`. For `G t = F(t + α z)` and
+`deg F < ∑_t q_t` it is `F(0)` (`eval_zero_eq_taperedRecovery`), the manuscript's (D.9).
+
+**Precision.** Each `E_t(t + α z)` is a product of powers of `1 + α z / (t - q)`, so it has
+coefficients in `ℤ_(2)` and constant term one, and so has the inverse power series
+(`hermiteBasis_comp_eq_map`, `coeff_invOfUnit_hermiteBasis_comp_mem`). The quotient of a jet that
+is divisible by `2 ^ p_t` is therefore divisible by `2 ^ p_t`. Evaluating a polynomial of degree
+at most `q_t` at `-t / α` multiplies by rationals of valuation at least `-q_t (a + 1)`, and `E_t(0)`
+has valuation at least `-6 h D_t` with `D_t = 2 ^ (a - v₂ t)` ((D.10),
+`Polynomial.neg_le_padicValRat_eval_zero_hermiteBasis_taper`). So if the jets `G t` agree with
+`F(t + α z)` modulo `2 ^ p_t` below `z ^ q_t`, where `p + 6 h D_t + q_t (a + 1) ≤ p_t`, the
+recovered value agrees with `F(0)` modulo `2 ^ p` (`exists_taperedRecovery_eq_add`). The
+manuscript's choice `p_t = p + 8 h D_t + 8 M (a + 1)` satisfies this when `q_t ≤ 4 M`
+(`taperMult_le`); the manuscript's multiplicities have enough total weight
+(`le_sum_taperMult`).
+
+Congruences are stated in `K` as `x = y + 2 ^ p * b` with `b ∈ B`.
+
+## Main definitions
+
+* `Cslib.Circuits.Frontier.recoveryNodes`: the nonzero points of the grid.
+* `Cslib.Circuits.Frontier.taperMult`: the tapered multiplicities `q_t`.
+* `Cslib.Circuits.Frontier.taperedRecovery`: the right side of (D.9) for given jets.
+
+## Main results
+
+* `Cslib.Circuits.Frontier.le_sum_taperMult`: the total multiplicity is at least `2 ^ a h u`.
+* `Cslib.Circuits.Frontier.taperMult_le`: `q_t ≤ 4 M` for `h = ⌈3 M / u⌉` and `u ≤ M`.
+* `Cslib.Circuits.Frontier.eval_zero_eq_taperedRecovery`: (D.9).
+* `Cslib.Circuits.Frontier.hermiteBasis_comp_eq_map`: `E_t(t + α z)` is integral with constant
+  term one.
+* `Cslib.Circuits.Frontier.exists_taperedRecovery_eq_add`: recovery modulo `2 ^ p` from jets
+  modulo `2 ^ p_t`.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.4, Lemma D.5,
+  (D.9)–(D.10), pp. 60–61.
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier
+
+open Polynomial Finset
+
+/-- The subring `ℤ_(2)` of rationals with odd denominator. -/
+local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
+
+/-! ### Nodes and multiplicities -/
+
+/-- The nodes of tapered Hermite recovery: the nonzero points of the grid of `2 ^ a` slots. -/
+@[expose] def recoveryNodes (a : ℕ) : Finset ℤ :=
+  (cauchyGrid (2 ^ a)).erase 0
+
+/-- The tapered multiplicity `q_t = h max(0, u - v₂ t)` of Lemma D.5, with natural
+subtraction. -/
+@[expose] def taperMult (u h : ℕ) (t : ℤ) : ℕ :=
+  h * (u - padicValInt 2 t)
+
+/-- The grid of `2 ^ a` slots is `[-2 ^ a, 2 ^ a)`. -/
+theorem cauchyGrid_two_pow (a : ℕ) : cauchyGrid (2 ^ a) = Ico (-(2 : ℤ) ^ a) (2 ^ a) := by
+  simp only [cauchyGrid, Nat.cast_pow, Nat.cast_ofNat]
+
+theorem recoveryNodes_eq (a : ℕ) : recoveryNodes a = (Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0 := by
+  rw [recoveryNodes, cauchyGrid_two_pow]
+
+/-- **There is enough multiplicity.** The `2 ^ a` odd nodes have multiplicity `h u` each. -/
+theorem le_sum_taperMult (a u h : ℕ) :
+    2 ^ a * (h * u) ≤ ∑ t ∈ recoveryNodes a, taperMult u h t := by
+  have key := sum_Ico_erase_zero_padicValInt_two a fun j => ((h * (u - j) : ℕ) : ℤ)
+  rw [← recoveryNodes_eq] at key
+  have hsum : ((∑ t ∈ recoveryNodes a, taperMult u h t : ℕ) : ℤ) =
+      ∑ j ∈ range (a + 1), 2 ^ (a - j) * ((h * (u - j) : ℕ) : ℤ) := by
+    rw [← key]
+    push_cast [taperMult]
+    rfl
+  have hle : ((2 ^ a * (h * u) : ℕ) : ℤ) ≤
+      ∑ j ∈ range (a + 1), 2 ^ (a - j) * ((h * (u - j) : ℕ) : ℤ) := by
+    rw [sum_range_succ']
+    simp only [Nat.sub_zero, Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat]
+    have : 0 ≤ ∑ j ∈ range a, (2 : ℤ) ^ (a - (j + 1)) * ((h : ℤ) * ((u - (j + 1) : ℕ) : ℤ)) :=
+      sum_nonneg fun j _ => by positivity
+    linarith
+  exact_mod_cast hle.trans hsum.symm.le
+
+/-- **Multiplicities are at most `4 M`** when `h = ⌈3 M / u⌉` (any `h ≤ 3 M / u + 1`) and
+`u ≤ M`. -/
+theorem taperMult_le {u h M : ℕ} (hh : h * u ≤ 3 * M + u) (huM : u ≤ M) (t : ℤ) :
+    taperMult u h t ≤ 4 * M := by
+  unfold taperMult
+  calc h * (u - padicValInt 2 t) ≤ h * u := Nat.mul_le_mul_left _ (Nat.sub_le _ _)
+    _ ≤ 4 * M := by omega
+
+/-! ### The recovered value -/
+
+variable {K : Type*} [CommRing K] [Algebra ℚ K]
+
+/-- The value recovered by tapered Hermite interpolation from the polynomials `G t`: the right
+side of (D.9) of [OpenAI2026ETH], `∑_t E_t(0) (G t / E_t(t + α z) mod z ^ q_t)(-t / α)` over the
+nonzero grid points `t`, with `α = 2 ^ (a + 1)`. Only the first `q_t` coefficients of `G t`
+matter (`Polynomial.hermiteQuotient_trunc`). -/
+noncomputable def taperedRecovery (a u h : ℕ) (G : ℤ → K[X]) : K :=
+  ∑ t ∈ recoveryNodes a,
+    (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h) t).eval 0 *
+      (hermiteQuotient (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h) (2 ^ (a + 1)) t
+        (G t)).eval (algebraMap ℚ K (-(t : ℚ) / 2 ^ (a + 1)))
+
+/-- `2 ^ n` as a unit of a `ℚ`-algebra. -/
+private noncomputable def twoPowUnit (K : Type*) [CommRing K] [Algebra ℚ K] (n : ℕ) : Kˣ :=
+  Units.map (algebraMap ℚ K : ℚ →* K) (Units.mk0 ((2 : ℚ) ^ n) (by positivity))
+
+private theorem coe_twoPowUnit (n : ℕ) : ((twoPowUnit K n : Kˣ) : K) = 2 ^ n := by
+  simp [twoPowUnit, map_pow, map_ofNat]
+
+private theorem coe_twoPowUnit_inv (n : ℕ) :
+    ((twoPowUnit K n)⁻¹ : Kˣ) = algebraMap ℚ K ((2 : ℚ) ^ n)⁻¹ := by
+  simp [twoPowUnit, Units.val_inv_eq_inv_val]
+
+/-- Distinct integers are units of a `ℚ`-algebra apart. -/
+private theorem pairwise_isUnit_sub (s : Finset ℤ) :
+    (s : Set ℤ).Pairwise fun i j => IsUnit ((i : K) - (j : K)) := by
+  intro i _ j _ hij
+  have h : ((i : ℚ) - j) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast hij)
+  have := (isUnit_iff_ne_zero.mpr h).map (algebraMap ℚ K)
+  simpa using this
+
+/-- **Hermite reconstruction (D.9)** of [OpenAI2026ETH]: for `deg F < ∑_t q_t`, the recovered value
+from the local polynomials `F(t + α z)` is `F(0)`. -/
+theorem eval_zero_eq_taperedRecovery {a u h : ℕ} {F : K[X]}
+    (hF : F.degree < ↑(∑ t ∈ recoveryNodes a, taperMult u h t)) :
+    F.eval 0 = taperedRecovery a u h fun t => F.comp (C (t : K) + C (2 ^ (a + 1)) * X) := by
+  rw [eval_eq_sum_hermiteBasis_mul_hermiteQuotient (pairwise_isUnit_sub _) (twoPowUnit K (a + 1))
+    hF 0, taperedRecovery]
+  refine sum_congr rfl fun t _ => ?_
+  rw [coe_twoPowUnit, coe_twoPowUnit_inv, zero_sub, ← map_intCast (algebraMap ℚ K) t, ← map_neg,
+    ← map_mul]
+  congr 3
+  ring
+
+/-! ### Integrality of the Hermite basis in local coordinates -/
+
+/-- The rationals `α / (t - q)` with `t ≠ q` on the grid, `α = 2 ^ (a + 1)`, lie in `ℤ_(2)`. -/
+private theorem padicValuation_two_pow_div_le_one {a : ℕ} {t q : ℤ} (ht : t ∈ cauchyGrid (2 ^ a))
+    (hq : q ∈ cauchyGrid (2 ^ a)) (hne : q ≠ t) :
+    Rat.padicValuation 2 ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) ≤ 1 := by
+  have hle := padicValuation_two_pow_le_sub ht hq hne
+  have hne' : ((t : ℚ) - q) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast hne.symm)
+  rw [map_div₀, div_le_one₀ ((Rat.padicValuation 2).pos_iff.mpr hne')]
+  refine le_trans ?_ hle
+  rw [pow_succ, map_mul]
+  exact mul_le_of_le_one_right' (by
+    rw [show (2 : ℚ) = ((2 : ℕ) : ℚ) by norm_num, Rat.padicValuation_natCast]
+    exact Int.padicValuation_le_one 2 2)
+
+/-- The Hermite basis over `ℚ` in local coordinates is a product of powers of
+`1 + α / (t - q) z`. -/
+private theorem hermiteBasis_comp_rat (a u h : ℕ) (t : ℤ) :
+    (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : ℚ)) (taperMult u h) t).comp
+        (C (t : ℚ) + C (2 ^ (a + 1)) * X) =
+      ∏ q ∈ (recoveryNodes a).erase t,
+        (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X) ^ taperMult u h q := by
+  rw [hermiteBasis, Polynomial.prod_comp]
+  refine prod_congr rfl fun q hq => ?_
+  have hqt : ((t : ℚ) - q) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast (ne_of_mem_erase hq).symm)
+  rw [pow_comp, mul_comp, C_comp, sub_comp, X_comp, C_comp, Ring.inverse_eq_inv']
+  congr 1
+  rw [show C (t : ℚ) + C (2 ^ (a + 1)) * X - C (q : ℚ) =
+      C ((t : ℚ) - q) * (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X) by
+    rw [mul_add, mul_one, ← mul_assoc, ← C_mul, mul_div_cancel₀ _ hqt, C_sub]; ring,
+    ← mul_assoc, ← C_mul, inv_mul_cancel₀ hqt, C_1, one_mul]
+
+/-- **Lemma D.5, integrality.** For a nonzero grid point `t`, the Hermite basis polynomial in
+local coordinates, `E_t(t + α z)`, is the image of a polynomial over `ℤ_(2)` with constant term
+one: each factor is a power of `1 + α z / (t - q)` with `α / (t - q)` in `ℤ_(2)`. -/
+theorem hermiteBasis_comp_eq_map (a u h : ℕ) {t : ℤ} (ht : t ∈ recoveryNodes a) :
+    ∃ E : ℤ₍₂₎[X], E.coeff 0 = 1 ∧
+      (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h) t).comp
+          (C (t : K) + C (2 ^ (a + 1)) * X) =
+        E.map ((algebraMap ℚ K).comp (ℤ₍₂₎).subtype) := by
+  have htS : t ∈ cauchyGrid (2 ^ a) := mem_of_mem_erase ht
+  -- each factor is integral
+  have hfac : ∀ q ∈ (recoveryNodes a).erase t,
+      (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X) ∈ lifts (ℤ₍₂₎).subtype := fun q hq =>
+    add_mem (one_mem _) (mul_mem (C_mem_lifts _ (⟨_, padicValuation_two_pow_div_le_one htS
+      (mem_of_mem_erase (mem_of_mem_erase hq)) (ne_of_mem_erase hq)⟩ : ℤ₍₂₎)) (X_mem_lifts _))
+  obtain ⟨E, hE⟩ := (mem_lifts _).mp (Subsemiring.prod_mem _ fun q hq =>
+    Subsemiring.pow_mem _ (hfac q hq) (taperMult u h q))
+  have hEq : E.map (ℤ₍₂₎).subtype = (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : ℚ))
+      (taperMult u h) t).comp (C (t : ℚ) + C (2 ^ (a + 1)) * X) := by
+    rw [hE, hermiteBasis_comp_rat]
+  refine ⟨E, ?_, ?_⟩
+  · apply Subtype.val_injective
+    have h0 := congrArg (fun P => Polynomial.coeff P 0) hEq
+    simp only [coeff_map, Subring.coe_subtype] at h0
+    rw [h0, coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_C, eval_mul, eval_C, eval_X,
+      mul_zero, add_zero, eval_hermiteBasis_self (pairwise_isUnit_sub _) ht]
+    rfl
+  · have hv : (fun q : ℤ => algebraMap ℚ K (q : ℚ)) = fun q : ℤ => (q : K) :=
+      funext fun q => map_intCast _ q
+    have hlin : (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X).map (algebraMap ℚ K) =
+        C (t : K) + C (2 ^ (a + 1)) * X := by
+      rw [Polynomial.map_add, Polynomial.map_mul, Polynomial.map_C, Polynomial.map_C,
+        Polynomial.map_X, map_intCast, map_pow, map_ofNat]
+    rw [← Polynomial.map_map, hEq, Polynomial.map_comp,
+      map_hermiteBasis _ (pairwise_isUnit_sub _) ht, hv, hlin]
+
+/-- The inverse power series of `E_t(t + α z)` is the image of a power series over `ℤ_(2)`. -/
+private theorem invOfUnit_hermiteBasis_comp_eq_map (a u h : ℕ) {t : ℤ} (ht : t ∈ recoveryNodes a) :
+    ∃ ψ : PowerSeries ℤ₍₂₎,
+      PowerSeries.invOfUnit (((hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : K))
+          (taperMult u h) t).comp (C (t : K) + C (2 ^ (a + 1)) * X) : K[X]) : PowerSeries K) 1 =
+        PowerSeries.map ((algebraMap ℚ K).comp (ℤ₍₂₎).subtype) ψ := by
+  obtain ⟨E, hE0, hE⟩ := hermiteBasis_comp_eq_map (K := K) a u h ht
+  refine ⟨PowerSeries.invOfUnit (E : PowerSeries ℤ₍₂₎) 1, ?_⟩
+  set κ := (algebraMap ℚ K).comp (ℤ₍₂₎).subtype
+  set φ : PowerSeries K := ((E.map κ : K[X]) : PowerSeries K)
+  have hφ : φ = PowerSeries.map κ (E : PowerSeries ℤ₍₂₎) := Polynomial.polynomial_map_coe
+  have h1 : φ * PowerSeries.invOfUnit φ 1 = 1 :=
+    PowerSeries.mul_invOfUnit _ _ (by
+      rw [Polynomial.constantCoeff_coe, coeff_map, hE0, map_one, Units.val_one])
+  have h2 : φ * PowerSeries.map κ (PowerSeries.invOfUnit (E : PowerSeries ℤ₍₂₎) 1) = 1 := by
+    rw [hφ, ← map_mul, PowerSeries.mul_invOfUnit _ _ (by
+      rw [Polynomial.constantCoeff_coe, hE0, Units.val_one]), map_one]
+  rw [hE]
+  calc PowerSeries.invOfUnit φ 1
+      = PowerSeries.invOfUnit φ 1 * (φ * PowerSeries.map κ
+          (PowerSeries.invOfUnit (E : PowerSeries ℤ₍₂₎) 1)) := by rw [h2, mul_one]
+    _ = PowerSeries.map κ (PowerSeries.invOfUnit (E : PowerSeries ℤ₍₂₎) 1) := by
+      rw [← mul_assoc, mul_comm _ φ, h1, one_mul]
+
+/-! ### Congruences modulo powers of two -/
+
+private theorem padicValRat_two : padicValRat 2 (2 : ℚ) = 1 := by
+  exact_mod_cast padicValRat.self (p := 2) one_lt_two
+
+omit [Algebra ℚ K] in
+/-- `x` is `2 ^ n` times an element of `B`. -/
+private def InTwoPow (B : Subring K) (n : ℕ) (x : K) : Prop :=
+  ∃ b ∈ B, x = 2 ^ n * b
+
+omit [Algebra ℚ K] in
+private theorem inTwoPow_zero (B : Subring K) (n : ℕ) : InTwoPow B n (0 : K) :=
+  ⟨0, B.zero_mem, (mul_zero _).symm⟩
+
+omit [Algebra ℚ K] in
+private theorem InTwoPow.add {B : Subring K} {n : ℕ} {x y : K} (hx : InTwoPow B n x)
+    (hy : InTwoPow B n y) : InTwoPow B n (x + y) := by
+  obtain ⟨b, hb, rfl⟩ := hx
+  obtain ⟨c, hc, rfl⟩ := hy
+  exact ⟨b + c, B.add_mem hb hc, by ring⟩
+
+omit [Algebra ℚ K] in
+private theorem InTwoPow.sub {B : Subring K} {n : ℕ} {x y : K} (hx : InTwoPow B n x)
+    (hy : InTwoPow B n y) : InTwoPow B n (x - y) := by
+  obtain ⟨b, hb, rfl⟩ := hx
+  obtain ⟨c, hc, rfl⟩ := hy
+  exact ⟨b - c, B.sub_mem hb hc, by ring⟩
+
+omit [Algebra ℚ K] in
+private theorem inTwoPow_sum {B : Subring K} {n : ℕ} {ι : Type*} (s : Finset ι) {f : ι → K}
+    (hf : ∀ i ∈ s, InTwoPow B n (f i)) : InTwoPow B n (∑ i ∈ s, f i) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => exact inTwoPow_zero B n
+  | insert j s hj ih =>
+    rw [sum_insert hj]
+    exact (hf j (mem_insert_self j s)).add (ih fun i hi => hf i (mem_insert_of_mem hi))
+
+omit [Algebra ℚ K] in
+private theorem InTwoPow.mul_left {B : Subring K} {n : ℕ} {x y : K} (hx : InTwoPow B n x)
+    (hy : y ∈ B) : InTwoPow B n (x * y) := by
+  obtain ⟨b, hb, rfl⟩ := hx
+  exact ⟨b * y, B.mul_mem hb hy, by ring⟩
+
+/-- A rational of valuation at least `-k` maps `2 ^ (n + k) B` into `2 ^ n B`. -/
+private theorem InTwoPow.algebraMap_mul {B : Subring K}
+    (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {n k : ℕ} {x : K} (hx : InTwoPow B (n + k) x)
+    {r : ℚ} (hr : r ≠ 0) (hv : -(k : ℤ) ≤ padicValRat 2 r) :
+    InTwoPow B n (algebraMap ℚ K r * x) := by
+  obtain ⟨b, hb, rfl⟩ := hx
+  have hr2 : r * 2 ^ k ∈ ℤ₍₂₎ := by
+    have hne : r * 2 ^ k ≠ 0 := mul_ne_zero hr (by positivity)
+    have hval : 0 ≤ padicValRat 2 (r * 2 ^ k) := by
+      rw [padicValRat.mul hr (by positivity), padicValRat.pow, padicValRat_two]
+      omega
+    change Rat.padicValuation 2 (r * 2 ^ k) ≤ 1
+    simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
+      hne, ↓reduceIte]
+    rw [← WithZero.exp_zero, WithZero.exp_le_exp]
+    omega
+  refine ⟨algebraMap ℚ K (r * 2 ^ k) * b, B.mul_mem (hB _ hr2) hb, ?_⟩
+  rw [map_mul, map_pow, map_ofNat, pow_add]
+  ring
+
+/-- **The quotient of a jet divisible by `2 ^ n` is divisible by `2 ^ n`**: the inverse power
+series of `E_t(t + α z)` is integral. -/
+private theorem inTwoPow_coeff_hermiteQuotient {B : Subring K}
+    (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {a u h n : ℕ} {t : ℤ} (ht : t ∈ recoveryNodes a)
+    {P : K[X]} (hP : ∀ j < taperMult u h t, InTwoPow B n (P.coeff j)) (j : ℕ) :
+    InTwoPow B n ((hermiteQuotient (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h)
+      (2 ^ (a + 1)) t P).coeff j) := by
+  obtain ⟨ψ, hψ⟩ := invOfUnit_hermiteBasis_comp_eq_map (K := K) a u h ht
+  rw [hermiteQuotient, hψ, PowerSeries.coeff_trunc]
+  split_ifs with hj
+  · rw [PowerSeries.coeff_mul]
+    refine inTwoPow_sum _ fun kl hkl => ?_
+    have hk : kl.1 < taperMult u h t := by
+      have := mem_antidiagonal.mp hkl
+      omega
+    rw [Polynomial.coeff_coe, PowerSeries.coeff_map]
+    exact (hP _ hk).mul_left (hB _ (PowerSeries.coeff kl.2 ψ).2)
+  · exact inTwoPow_zero B n
+
+/-- The value of `E_t(0)` in `K` is the image of the rational one. -/
+private theorem eval_zero_hermiteBasis_eq (a u h : ℕ) {t : ℤ} (ht : t ∈ recoveryNodes a) :
+    (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h) t).eval 0 =
+      algebraMap ℚ K
+        ((hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : ℚ)) (taperMult u h) t).eval 0) := by
+  have hv : (fun q : ℤ => algebraMap ℚ K (q : ℚ)) = fun q : ℤ => (q : K) :=
+    funext fun q => map_intCast _ q
+  rw [← hv, ← map_hermiteBasis _ (pairwise_isUnit_sub _) ht, eval_map,
+    ← map_zero (algebraMap ℚ K), eval₂_at_apply]
+
+/-- `E_t(0) ≠ 0`: its factors are `-q / (t - q)` with `q ≠ 0`. -/
+private theorem eval_zero_hermiteBasis_ne_zero (a u h : ℕ) {t : ℤ} :
+    (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : ℚ)) (taperMult u h) t).eval 0 ≠ 0 := by
+  rw [eval_hermiteBasis, prod_ne_zero_iff]
+  intro q hq
+  have hq0 : (q : ℚ) ≠ 0 := by exact_mod_cast ne_of_mem_erase (mem_of_mem_erase hq)
+  have hqt : ((t : ℚ) - q) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast (ne_of_mem_erase hq).symm)
+  rw [Ring.inverse_eq_inv']
+  exact pow_ne_zero _ (mul_ne_zero (inv_ne_zero hqt) (by rwa [zero_sub, neg_ne_zero]))
+
+/-- **Lemma D.5, precision** ([OpenAI2026ETH], §D.4.4, pp. 60–61). Let `B` be a subring of the
+`ℚ`-algebra `K` containing `ℤ_(2)`, and let `F ∈ K[T]` have degree below the total multiplicity
+`∑_t q_t`. Suppose that at every nonzero grid point `t` the polynomial `G t` agrees with
+`F(t + α z)` modulo `2 ^ p_t` below `z ^ q_t`, where `p + 6 h D_t + q_t (a + 1) ≤ p_t` and
+`D_t = 2 ^ (a - v₂ t)`. Then the recovered value agrees with `F(0)` modulo `2 ^ p`. -/
+theorem exists_taperedRecovery_eq_add (B : Subring K) (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B)
+    {a u h p : ℕ} (pt : ℤ → ℕ)
+    (hpt : ∀ t ∈ recoveryNodes a,
+      p + 6 * h * 2 ^ (a - padicValInt 2 t) + taperMult u h t * (a + 1) ≤ pt t)
+    {F : K[X]} (hF : F.degree < ↑(∑ t ∈ recoveryNodes a, taperMult u h t)) (G : ℤ → K[X])
+    (hG : ∀ t ∈ recoveryNodes a, ∀ j < taperMult u h t, ∃ b ∈ B,
+      (G t).coeff j = (F.comp (C (t : K) + C (2 ^ (a + 1)) * X)).coeff j + 2 ^ pt t * b) :
+    ∃ b ∈ B, taperedRecovery a u h G = F.eval 0 + 2 ^ p * b := by
+  suffices hsub : InTwoPow B p (taperedRecovery a u h G - F.eval 0) by
+    obtain ⟨b, hb, hb'⟩ := hsub
+    exact ⟨b, hb, by rw [← hb', add_sub_cancel]⟩
+  rw [eval_zero_eq_taperedRecovery hF, taperedRecovery, taperedRecovery, ← sum_sub_distrib]
+  refine inTwoPow_sum _ fun t ht => ?_
+  set F' := F.comp (C (t : K) + C (2 ^ (a + 1)) * X)
+  set J := taperMult u h t
+  set Q := hermiteQuotient (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h)
+    (2 ^ (a + 1)) t ((G t - F' : K[X]) : PowerSeries K)
+  have hQ : ∀ j, InTwoPow B (pt t) (Q.coeff j) := by
+    refine inTwoPow_coeff_hermiteQuotient hB ht (P := G t - F') (fun j hj => ?_)
+    obtain ⟨b, hb, hb'⟩ := hG t ht j hj
+    exact ⟨b, hb, by rw [coeff_sub, hb', add_sub_cancel_left]⟩
+  have hQsub : hermiteQuotient (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h)
+      (2 ^ (a + 1)) t (G t) - hermiteQuotient (recoveryNodes a) (fun q : ℤ => (q : K))
+      (taperMult u h) (2 ^ (a + 1)) t F' = Q := by
+    simp only [Q, hermiteQuotient, Polynomial.coe_sub, sub_mul, map_sub]
+  have hdeg : Q.natDegree < J + 1 := by
+    have := degree_hermiteQuotient_lt (recoveryNodes a) (fun q : ℤ => (q : K)) (taperMult u h)
+      (2 ^ (a + 1)) t ((G t - F' : K[X]) : PowerSeries K)
+    by_cases hQ0 : Q = 0
+    · rw [hQ0, natDegree_zero]; omega
+    · have := (natDegree_lt_iff_degree_lt hQ0).mpr this
+      omega
+  rw [← mul_sub, ← eval_sub, hQsub, eval_eq_sum_range' hdeg, mul_sum,
+    eval_zero_hermiteBasis_eq a u h ht]
+  refine inTwoPow_sum _ fun j hj => ?_
+  have hjJ : j ≤ J := Nat.lt_succ_iff.mp (mem_range.mp hj)
+  set E0 := (hermiteBasis (recoveryNodes a) (fun q : ℤ => (q : ℚ)) (taperMult u h) t).eval 0
+  have ht0 : (t : ℚ) ≠ 0 := by exact_mod_cast ne_of_mem_erase ht
+  have hx0 : (-(t : ℚ) / 2 ^ (a + 1)) ≠ 0 := div_ne_zero (neg_ne_zero.mpr ht0) (by positivity)
+  have hr : E0 * (-(t : ℚ) / 2 ^ (a + 1)) ^ j ≠ 0 :=
+    mul_ne_zero (eval_zero_hermiteBasis_ne_zero a u h) (pow_ne_zero _ hx0)
+  have hE0 : -(6 * (h : ℤ) * 2 ^ (a - padicValInt 2 t)) ≤ padicValRat 2 E0 := by
+    have := neg_le_padicValRat_eval_zero_hermiteBasis_taper (a := a) u h
+      (mem_of_mem_erase (by rw [← recoveryNodes_eq]; exact ht)) (ne_of_mem_erase ht)
+    rw [← recoveryNodes_eq] at this
+    exact this
+  have hxv : -((a : ℤ) + 1) ≤ padicValRat 2 (-(t : ℚ) / 2 ^ (a + 1)) := by
+    rw [padicValRat.div (neg_ne_zero.mpr ht0) (by positivity), padicValRat.neg,
+      padicValRat.of_int, padicValRat.pow, padicValRat_two]
+    push_cast
+    omega
+  have hval : -((pt t - p : ℕ) : ℤ) ≤ padicValRat 2 (E0 * (-(t : ℚ) / 2 ^ (a + 1)) ^ j) := by
+    rw [padicValRat.mul (eval_zero_hermiteBasis_ne_zero a u h) (pow_ne_zero _ hx0),
+      padicValRat.pow]
+    have hpt' := hpt t ht
+    have hJ : (j : ℤ) * padicValRat 2 (-(t : ℚ) / 2 ^ (a + 1)) ≥ -((J : ℤ) * ((a : ℤ) + 1)) := by
+      have : (j : ℤ) ≤ J := by exact_mod_cast hjJ
+      nlinarith
+    have : ((pt t - p : ℕ) : ℤ) = (pt t : ℤ) - p := by omega
+    push_cast [this]
+    have hpt'' : (p : ℤ) + 6 * h * 2 ^ (a - padicValInt 2 t) + (J : ℤ) * (a + 1) ≤ pt t := by
+      exact_mod_cast hpt'
+    linarith
+  have hk : p + (pt t - p) = pt t := by have := hpt t ht; omega
+  have hQj := hQ j
+  rw [← hk] at hQj
+  have := hQj.algebraMap_mul hB hr hval
+  rw [map_mul, map_pow] at this
+  convert this using 1
+  ring
+
+/-- **Lemma D.5 with the manuscript's parameters.** Let `1 ≤ u ≤ M`, let `h` satisfy
+`3 M ≤ h u ≤ 3 M + u` (as `h = ⌈3 M / u⌉` does), and let `F` have degree at most `M (2 L - 1)`,
+`L = 2 ^ a`. If the jets `G t` agree with `F(t + α z)` modulo `2 ^ p_t` below `z ^ q_t`, with
+`p_t = p + 8 h D_t + 8 M (a + 1)`, then the recovered value agrees with `F(0)` modulo `2 ^ p`. -/
+theorem exists_taperedRecovery_eq_add_of_params (B : Subring K)
+    (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {a u h p M : ℕ} (hu : 1 ≤ u) (huM : u ≤ M)
+    (hh : 3 * M ≤ h * u) (hh' : h * u ≤ 3 * M + u) {F : K[X]}
+    (hF : F.natDegree ≤ M * (2 * 2 ^ a - 1)) (G : ℤ → K[X])
+    (hG : ∀ t ∈ recoveryNodes a, ∀ j < taperMult u h t, ∃ b ∈ B,
+      (G t).coeff j = (F.comp (C (t : K) + C (2 ^ (a + 1)) * X)).coeff j +
+        2 ^ (p + 8 * h * 2 ^ (a - padicValInt 2 t) + 8 * M * (a + 1)) * b) :
+    ∃ b ∈ B, taperedRecovery a u h G = F.eval 0 + 2 ^ p * b := by
+  refine exists_taperedRecovery_eq_add B hB
+    (fun t => p + 8 * h * 2 ^ (a - padicValInt 2 t) + 8 * M * (a + 1)) (fun t _ => ?_) ?_ G hG
+  · have hJ := taperMult_le hh' huM t
+    have hD : 6 * h * 2 ^ (a - padicValInt 2 t) ≤ 8 * h * 2 ^ (a - padicValInt 2 t) :=
+      Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (by norm_num))
+    have hJa : taperMult u h t * (a + 1) ≤ 8 * M * (a + 1) :=
+      Nat.mul_le_mul_right _ (by omega)
+    omega
+  · refine (degree_le_natDegree).trans_lt ?_
+    have hsum := le_sum_taperMult a u h
+    have hM : 1 ≤ M := hu.trans huM
+    have h2a : 1 ≤ 2 ^ a := Nat.one_le_two_pow
+    have : M * (2 * 2 ^ a - 1) < 2 ^ a * (h * u) := by
+      have h3 : 2 ^ a * (3 * M) ≤ 2 ^ a * (h * u) := Nat.mul_le_mul_left _ hh
+      have : M * (2 * 2 ^ a - 1) < 2 ^ a * (3 * M) := by
+        rw [Nat.mul_sub, mul_one]
+        have : M * (2 * 2 ^ a) = 2 * (2 ^ a * M) := by ring
+        have : 2 ^ a * (3 * M) = 3 * (2 ^ a * M) := by ring
+        have : 1 ≤ 2 ^ a * M := Nat.one_le_iff_ne_zero.mpr (by positivity)
+        omega
+      omega
+    exact_mod_cast (hF.trans_lt (this.trans_le hsum))
+
+end Cslib.Circuits.Frontier
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkLocalDeformation.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkLocalDeformation.lean
new file mode 100644
index 0000000000..eea99015e2
--- /dev/null
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkLocalDeformation.lean
@@ -0,0 +1,68 @@
+/-
+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.LocalDeformation
+public import Complexity.Foundations.NumberTheory.Padics.RatValuation
+
+/-!
+# Tests for the deformed contraction in local coordinates
+
+The two-edge network of the Cauchy-mode tests, with tensors over `ℤ_(2)`: one packet of two
+slots (`a = 1`), at the grid point `t = 1`. Its local deformation is a polynomial over `ℤ_(2)` of
+degree at most `2 (2 * 2 - 1) = 6`; in `ℚ` it is `F(1 + 4 z)`, and modulo `4` its value at `ζ` is
+the deformed contraction along the Cauchy matrix at `T = 1 + 4 ζ`.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation
+
+open Cslib.Circuits.Frontier TensorNetwork Polynomial
+
+/-- The subring `ℤ_(2)` of rationals with odd denominator. -/
+local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
+
+/-- The two-edge network over `ℤ_(2)`, with tensor `(1, 2)` on the bit of the edge at each
+vertex. -/
+def net : TensorNetwork ℤ₍₂₎ Bool (Fin 4) (Fin 2) where
+  src e := ⟨e.val, by omega⟩
+  tgt e := ⟨e.val + 2, by omega⟩
+  tensor v x := if x ⟨v.val % 2, Nat.mod_lt _ (by decide)⟩ then 2 else 1
+  tensor_congr v x y h := by rw [h _ (by fin_cases v <;> decide)]
+
+/-- The rows `0, 1`. -/
+def side (v : Fin 4) : Bool := decide (v.val < 2)
+
+/-- Edge `e` sits in slot `e` of the single packet. -/
+def slot (e : Fin 2) : ℕ := e.val
+
+theorem hslot (e : Fin 2) : slot e < 2 ^ 1 := by fin_cases e <;> decide
+
+/-- The degree bound `M (2 L - 1)`. -/
+example : (net.localDeformation side (RingHom.id _) 1 1 (fun _ => ()) slot).natDegree ≤ 6 :=
+  natDegree_localDeformation_le net side (RingHom.id _) hslot (by decide)
+
+/-- In `ℚ`, the local deformation is `F(1 + 4 z)` for the deformed contraction `F(T)` along the
+Cauchy matrix. -/
+example : (net.localDeformation side (RingHom.id _) 1 1 (fun _ => ()) slot).map (ℤ₍₂₎).subtype =
+    (((net.map (ℤ₍₂₎).subtype).map C).deformedContraction side
+      ((cauchyMatrix (2 ^ 1) (fun _ => ()) slot).map (mapRingHom (algebraMap ℚ ℚ)))).comp
+        (C ((1 : ℤ) : ℚ) + C (2 ^ (1 + 1)) * X) :=
+  map_localDeformation net side (RingHom.id _) (ℤ₍₂₎).subtype rfl hslot (by decide)
+
+/-- Modulo `4`, its value at `ζ` is the deformed contraction along the Cauchy matrix at
+`T = 1 + 4 ζ`. -/
+example (ζ : ZMod (2 ^ 2)) :
+    (net.localDeformation side (RingHom.id _) 1 1 (fun _ => ()) slot).eval₂
+        (Rat.padicIntegerToZModPow 2 2) ζ =
+      (net.map (Rat.padicIntegerToZModPow 2 2)).deformedContraction side
+        (cauchyValueMatrix (Rat.padicIntegerToZModPow 2 2) ζ 1 1 (fun _ => ()) slot) :=
+  eval₂_localDeformation net side (RingHom.id _) _ ζ 1 1 _ slot
+
+end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTaperedRecovery.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTaperedRecovery.lean
new file mode 100644
index 0000000000..58cea84af6
--- /dev/null
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTaperedRecovery.lean
@@ -0,0 +1,50 @@
+/-
+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.TaperedRecovery
+
+/-!
+# Tests for tapered Hermite recovery with finite precision
+
+The grid of two slots (`a = 1`) has the nodes `-2, -1, 1`. With `u = 2` and `h = 3`, the odd nodes
+have multiplicity `6` and the node `-2`, of valuation one, has multiplicity `3`. The precision
+theorem applies over `K = ℚ` with `B = ℤ_(2)`: its hypotheses are met by exact jets.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery
+
+open Cslib.Circuits.Frontier Polynomial
+
+/-- The subring `ℤ_(2)` of rationals with odd denominator. -/
+local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
+
+example : recoveryNodes 1 = {-2, -1, 1} := by decide
+
+example : taperMult 2 3 1 = 6 ∧ taperMult 2 3 (-1) = 6 := by
+  simp [taperMult, padicValInt]
+
+example : taperMult 2 3 (-2) = 3 := by
+  simp [taperMult, padicValInt]
+
+/-- The total multiplicity of the two odd nodes alone is `2 * 6`. -/
+example : 2 ^ 1 * (3 * 2) ≤ ∑ t ∈ recoveryNodes 1, taperMult 2 3 t :=
+  le_sum_taperMult 1 2 3
+
+/-- **Non-vacuity.** For `F = X` (degree `1 = M (2 L - 1)` with `M = 1`, `L = 1`), `u = 1` and
+`h = 3`, exact jets recover `F(0)` modulo every `2 ^ p`. -/
+theorem exists_taperedRecovery_X (p : ℕ) :
+    ∃ b ∈ ℤ₍₂₎, taperedRecovery 0 1 3 (fun t => (X : ℚ[X]).comp (C (t : ℚ) + C (2 ^ (0 + 1)) * X)) =
+      (X : ℚ[X]).eval 0 + 2 ^ p * b :=
+  exists_taperedRecovery_eq_add_of_params (K := ℚ) (M := 1) ℤ₍₂₎ (fun c hc => hc) le_rfl le_rfl
+    (by norm_num) (by norm_num) (by rw [natDegree_X]; norm_num) _
+    (fun t _ j _ => ⟨0, zero_mem _, by rw [mul_zero, add_zero]⟩)
+
+end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery