feat(circuit/frontier): native tapered recovery computes recoverFromValues mod 2^p (Lemma D.5)

Complexity.lean

@@ -893,6 +893,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCo
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.KernelProduct
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeRecovery
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEntry
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Recursion
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Reindex
@@ -2043,6 +2044,7 @@ public import Complexity.Computability.PolyTime.CommonCountingAccum
 public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck
 public import Complexity.Computability.PolyTime.GaloisRingArithmetic
 public import Complexity.Computability.PolyTime.GaloisRingInterpolation
+public import Complexity.Computability.PolyTime.GaloisRingSeries
 public import Complexity.Computability.PolyTime.GaloisRingUnits
 public import Complexity.Computability.PolyTime.GreedyLabelSchedule
 public import Complexity.Computability.PolyTime.GreedySlotScore

Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean

@@ -133,6 +133,12 @@ noncomputable def recoverFromValues (B : Subring K) (a u h : ℕ) {n : ℕ} (ζ
     (v : ℤ → Fin n → B) : K :=
   taperedRecovery a u h fun t => (Lagrange.ringInterpolate univ ζ (v t)).map B.subtype
 
+theorem recoverFromValues_def (B : Subring K) (a u h : ℕ) {n : ℕ} (ζ : Fin n → B)
+    (v : ℤ → Fin n → B) :
+    recoverFromValues B a u h ζ v =
+      taperedRecovery a u h fun t => (Lagrange.ringInterpolate univ ζ (v t)).map B.subtype := by
+  rw [recoverFromValues]
+
 /-- 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