diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeRecovery.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeRecovery.lean
index daa823e54c..48f1349891 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeRecovery.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeRecovery.lean
@@ -74,6 +74,8 @@ recovery is polynomial-time with the precision, the shift, the parameters and `2
 * `Cslib.Circuits.Frontier.NativeRecovery.recip`: the truncated reciprocal of `E_t(t + α z)`.
 * `Cslib.Circuits.Frontier.NativeRecovery.coeffMult`: the multipliers.
 * `Cslib.Circuits.Frontier.NativeRecovery.recover`: native tapered recovery.
+* `Cslib.Circuits.Frontier.NativeRecovery.storeValue`: storing a value in the table that `recover`
+  reads, the accumulator update of a recursive call.
 * `Cslib.Circuits.Frontier.NativeRecovery.recipSeries`,
   `Cslib.Circuits.Frontier.NativeRecovery.gamma`: the reciprocal and the multipliers over
   `ℤ_(2)`.
@@ -103,6 +105,9 @@ recovery is polynomial-time with the precision, the shift, the parameters and `2
   mathematical recovery modulo `2 ^ p`.
 * `Cslib.Circuits.Frontier.NativeRecovery.computableInPolyTime_recover`: native recovery is
   polynomial-time.
+* `Cslib.Circuits.Frontier.NativeRecovery.getD_foldl_storeValue`,
+  `Cslib.Circuits.Frontier.NativeRecovery.computableInPolyTime_storeValue`: storing a sequence of
+  values gives each node index its values in order, in polynomial time.
 
 ## References
 
@@ -238,6 +243,39 @@ def recover (p Δ : ℕ) (fl : List ℕ) (a u h : ℕ) (ζ : List (List ℕ)) (W
     if k = 2 ^ a then S else add (p + Δ) fl S (nodeTerm (p + Δ) fl a u h Δ ζ k (W.getD k [])))
     (zero fl))
 
+/-! ### Storing the values -/
+
+/-- Store the value `y` at node index `k`, after the values already stored there. This is the
+accumulator update of a recursive call once the value at an interpolation point is complete;
+`NativeRecovery.recover` reads the table. -/
+def storeValue (W : List (List (List ℕ))) (k : ℕ) (y : List ℕ) : List (List (List ℕ)) :=
+  (List.range (max W.length (k + 1))).map fun k' =>
+    if k' = k then W.getD k' [] ++ [y] else W.getD k' []
+
+theorem getD_storeValue (W : List (List (List ℕ))) (k : ℕ) (y : List ℕ) (k' : ℕ) :
+    (storeValue W k y).getD k' [] = if k' = k then W.getD k [] ++ [y] else W.getD k' [] := by
+  unfold storeValue
+  by_cases hk' : k' < max W.length (k + 1)
+  · rw [List.getD_eq_getElem _ _ (by simpa using hk'), List.getElem_map, List.getElem_range]
+    split_ifs with h
+    · rw [h]
+    · rfl
+  · have hne : k' ≠ k := by omega
+    rw [List.getD_eq_default _ _ (by rw [List.length_map, List.length_range]; omega),
+      ite_eq_right_of_eq_false _ _ (eq_false hne), List.getD_eq_default _ _ (by omega)]
+
+/-- **Storing a sequence of values**: each node index receives its values in order. -/
+theorem getD_foldl_storeValue (W : List (List (List ℕ))) (l : List (ℕ × List ℕ)) (k : ℕ) :
+    (l.foldl (fun W e => storeValue W e.1 e.2) W).getD k [] =
+      W.getD k [] ++ (l.filter fun e => e.1 = k).map Prod.snd := by
+  induction l generalizing W with
+  | nil => simp
+  | cons e l ih =>
+    rw [List.foldl_cons, ih, getD_storeValue, List.filter_cons]
+    by_cases h : e.1 = k
+    · simp [h]
+    · simp [h, Ne.symm h]
+
 /-! ### Correctness of the constants -/
 
 variable {N : ℕ} {fl : List ℕ}
@@ -1008,6 +1046,12 @@ private theorem singletonPolyTime {n : α → ℕ} (hn : ComputableInPolyTime n
     ComputableInPolyTime (fun x => [n x]) encIn (encList encNat) :=
   ComputableInPolyTime.cons' hn (ComputableInPolyTime.const [])
 
+/-- A coefficient list as a one-element list. -/
+private theorem singletonPolyTime' {c : α → List ℕ}
+    (hc : ComputableInPolyTime c encIn (encList encNat)) :
+    ComputableInPolyTime (fun x => [c x]) encIn (encList (encList encNat)) :=
+  ComputableInPolyTime.cons' hc (ComputableInPolyTime.const [])
+
 private theorem polyBounded_unary {n : α → ℕ} (hn : ComputableInPolyTime n encIn encUnary) :
     PolyBounded (fun x => (encIn x).length) n := by
   simpa using ComputableInPolyTime.polyBounded_length hn
@@ -1380,6 +1424,32 @@ theorem computableInPolyTime_recover {p Δ a u h : α → ℕ} {fl : α → List
   refine (computableInPolyTime_shiftDown hΔ hfold).of_enc_eq fun x => ?_
   simp only [recover, beq_iff_eq, Function.comp_apply]
 
+/-- **Storing a value is polynomial-time**, with the node index in unary. -/
+@[fun_prop]
+theorem computableInPolyTime_storeValue {W : α → List (List (List ℕ))} {k : α → ℕ}
+    {y : α → List ℕ}
+    (hW : ComputableInPolyTime W encIn (encList (encList (encList encNat))))
+    (hk : ComputableInPolyTime k encIn encUnary)
+    (hy : ComputableInPolyTime y encIn (encList encNat)) :
+    ComputableInPolyTime (fun x => storeValue (W x) (k x) (y x)) encIn
+      (encList (encList (encList encNat))) := by
+  have h1 := ComputableInPolyTime.fst encIn encUnary
+  have h2 := ComputableInPolyTime.snd encIn encUnary
+  have hrow := (ComputableInPolyTime.listGetD (encA := encList (encList encNat)) []).comp
+    ((hW.comp h1).prod h2)
+  have hlen := lengthPolyTime hW
+  have hmax : ComputableInPolyTime (fun x => max (W x).length (k x + 1)) encIn encUnary :=
+    (ComputableInPolyTime.unary_add' hlen (ComputableInPolyTime.unary_sub'
+      (ComputableInPolyTime.unary_add' hk (ComputableInPolyTime.const 1)) hlen)).of_enc_eq
+      fun x => by congr 1; omega
+  refine (ComputableInPolyTime.mapWithInput
+    (f := fun x k' => if (k' == k x) = true then (W x).getD k' [] ++ [y x] else (W x).getD k' [])
+    (ComputableInPolyTime.range.comp hmax)
+    (ComputableInPolyTime.ite (ComputableInPolyTime.beq h2 (hk.comp h1))
+      (ComputableInPolyTime.listAppend' hrow (singletonPolyTime' (hy.comp h1))) hrow)).of_enc_eq
+    fun x => ?_
+  simp only [storeValue, beq_iff_eq, Function.comp_apply]
+
 end PolyTime
 
 end Cslib.Circuits.Frontier.NativeRecovery
diff --git a/Complexity/Computability/PolyTime/GaloisRingSeries.lean b/Complexity/Computability/PolyTime/GaloisRingSeries.lean
index 455838f145..082432783f 100644
--- a/Complexity/Computability/PolyTime/GaloisRingSeries.lean
+++ b/Complexity/Computability/PolyTime/GaloisRingSeries.lean
@@ -31,7 +31,8 @@ the contraction algorithm of [OpenAI2026ETH] (Appendix D.4.4, pp. 60–61).
   determined modulo `2 ^ p` (`GaloisRingArith.mod_eq_of_val_eq`), and every element is the value
   of a reduced coefficient list (`GaloisRingArith.exists_val_eq`).
 * **Precision.** Reduction `A_N → A_n` for `n ≤ N` (`GaloisRingArith.reduce`) keeps the
-  coordinates (`GaloisRingArith.reduce_val`). Dividing the coordinates of `2 ^ Δ y` by `2 ^ Δ`
+  coordinates (`GaloisRingArith.reduce_val`), and its kernel is `2 ^ n A_N`
+  (`GaloisRingArith.exists_eq_add_of_reduce_eq`). Dividing the coordinates of `2 ^ Δ y` by `2 ^ Δ`
   gives `y` modulo `2 ^ (N - Δ)` (`GaloisRingArith.val_shiftDown`): this is how a sum that is
   known to be divisible by `2 ^ Δ` loses its common power of two.
 * **Truncated products** (`GaloisRingArith.tmul`) of polynomials in `z` over `A_p`: the first
@@ -51,6 +52,8 @@ length and the shift in unary (`GaloisRingArith.computableInPolyTime_tmul`,
 
 * `Cslib.GaloisRingArith.mod_eq_of_val_eq`, `Cslib.GaloisRingArith.exists_val_eq`: coordinates.
 * `Cslib.GaloisRingArith.val_shiftDown`: cancelling a common power of two.
+* `Cslib.GaloisRingArith.exists_eq_add_of_reduce_eq`,
+  `Cslib.GaloisRingArith.exists_val_eq_add_of_val_eq`: the kernel of reduction is `2 ^ n A_N`.
 * `Cslib.GaloisRingArith.val_tmul`: truncated products are correct.
 * `Cslib.GaloisRingArith.computableInPolyTime_tmul`,
   `Cslib.GaloisRingArith.computableInPolyTime_shiftDown`: polynomial time.
@@ -178,6 +181,27 @@ theorem reduce_val {n N : ℕ} (h : n ≤ N) (c : List ℕ) :
     reduce h fl (val N fl c) = val n fl c := by
   simp only [reduce, val, map_sum, map_mul, map_pow, map_natCast, AdjoinRoot.map_root]
 
+/-- **Equal reductions differ by a multiple of `2 ^ n`**: the kernel of reduction
+`A_N → A_n` is `2 ^ n A_N`. -/
+theorem exists_eq_add_of_reduce_eq {n N : ℕ} (h : n ≤ N) {x y : Ring N fl}
+    (hxy : reduce h fl x = reduce h fl y) : ∃ c, x = y + 2 ^ n * c := by
+  obtain ⟨r, -, -, rfl⟩ := exists_val_eq x
+  obtain ⟨s, -, -, rfl⟩ := exists_val_eq y
+  rw [reduce_val, reduce_val] at hxy
+  choose! q hq using fun i (hi : i < fl.length) => Nat.modEq_iff_dvd.mp (mod_eq_of_val_eq hxy hi)
+  refine ⟨-∑ i ∈ range fl.length, ((q i : ℤ) : Ring N fl) * AdjoinRoot.root _ ^ i, ?_⟩
+  rw [val, val, mul_neg, mul_sum, ← sub_eq_add_neg, ← sum_sub_distrib]
+  refine sum_congr rfl fun i hi => ?_
+  have hi' := congrArg (Int.cast : ℤ → Ring N fl) (hq i (mem_range.mp hi))
+  push_cast at hi'
+  linear_combination (-(AdjoinRoot.root _ ^ i : Ring N fl)) * hi'
+
+/-- **A value at a lower precision lifts with an error divisible by `2 ^ n`**: a coefficient list
+whose value in `A_n` is the reduction of `y ∈ A_N` has value `y + 2 ^ n c` in `A_N`. -/
+theorem exists_val_eq_add_of_val_eq {n N : ℕ} (h : n ≤ N) {w : List ℕ} {y : Ring N fl}
+    (hw : val n fl w = reduce h fl y) : ∃ c, val N fl w = y + 2 ^ n * c :=
+  exists_eq_add_of_reduce_eq h (by rw [reduce_val, hw])
+
 /-- Division of each coordinate by `2 ^ Δ`. -/
 def shiftDown (Δ : ℕ) (c : List ℕ) : List ℕ := c.map (· / 2 ^ Δ)
 
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeRecovery.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeRecovery.lean
index 35cced1e54..f0afe5bb95 100644
--- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeRecovery.lean
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeRecovery.lean
@@ -39,6 +39,11 @@ example : (mult 1 1 1 1, mult 1 1 1 3, mult 1 1 1 0) = (1, 1, 0) := by decide
 `E_{-1}(0) F(-1) + E_1(0) F(1) = (4 + 6) / 2 = 5` modulo `8`, computing modulo `2 ^ (3 + 2)`. -/
 example : recover 3 2 [1, 1] 1 1 1 [[0, 0]] [[], [[4, 0]], [], [[6, 0]]] = [5, 0] := by decide
 
+/-- The value table of that recovery, built by storing `F(-1)` at node index `1` and `F(1)` at
+node index `3`. -/
+example : storeValue (storeValue [] 1 [4, 0]) 3 [6, 0] = [[], [[4, 0]], [], [[6, 0]]] := by
+  decide
+
 /-- The same recovery with `Δ = (a + 1) ∑_t q_t = 4`, the shift that `val_recover` assumes. -/
 example : recover 3 4 [1, 1] 1 1 1 [[0, 0]] [[], [[4, 0]], [], [[6, 0]]] = [5, 0] := by decide
 
@@ -61,4 +66,9 @@ example : Turing.MultiTapeTM.ComputableInPolyTime (fun n : ℕ => twoVal n n)
   computableInPolyTime_twoVal Turing.MultiTapeTM.ComputableInPolyTime.id'
     Turing.MultiTapeTM.ComputableInPolyTime.id'
 
+/-- A value computed at precision `3` lifts to precision `5` with an error divisible by `2 ^ 3`. -/
+example (y : Ring 5 [1, 1]) (hw : val 3 [1, 1] [5, 0] = reduce (by norm_num) [1, 1] y) :
+    ∃ c, val 5 [1, 1] [5, 0] = y + 2 ^ 3 * c :=
+  exists_val_eq_add_of_val_eq _ hw
+
 end ComplexityTests.TensorNetworkNativeRecovery