From c86c11902b0258ce4f207d122528361b22e17253 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 31 Aug 2026 12:57:21 +0000 Subject: [PATCH] feat(truncated-series): expose bounded log agreement --- HexTruncatedSeries/ExpLog.lean | 66 +++++++++++-------- HexTruncatedSeries/ModuleBoundaryTests.lean | 16 +++++ .../SPEC/hex-truncated-series.md | 2 + 3 files changed, 55 insertions(+), 29 deletions(-) diff --git a/HexTruncatedSeries/ExpLog.lean b/HexTruncatedSeries/ExpLog.lean index 9dfc6505c..9a704d058 100644 --- a/HexTruncatedSeries/ExpLog.lean +++ b/HexTruncatedSeries/ExpLog.lean @@ -340,34 +340,42 @@ private theorem log_one_add [Lean.Grind.CommRing R] · intro i hi hip omega -private theorem logUpTo_agree [Lean.Grind.CommRing R] +/-- Bounded logarithm agrees with the full logarithm throughout the requested +prefix. -/ +theorem logUpTo_agree [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (m : Nat) (a : TSeries R n) - (ha : a.coeff 0 = 1) : Agree m (logUpTo m a) (log a) := by - intro i hi him - have hau : a.coeff 0 * 1 = 1 := by rw [ha]; grind - unfold log logUpTo - rw [coeff_ofFn _ i hi, if_pos him, coeff_ofFn _ i hi, if_pos hi, - coeff_truncate _ _ i hi, coeff_truncate _ _ i hi] - cases i with - | zero => - rw [coeff_integrate _ 0 (by omega), coeff_integrate _ 0 (by omega)] - simp - | succ i => - rw [coeff_integrate _ (i + 1) (by omega), - coeff_integrate _ (i + 1) (by omega)] - simp only [show i + 1 ≠ 0 by omega, if_false, Nat.add_sub_cancel] - rw [coeff_mulUpTo (m - 1) _ _ i (by omega), if_pos (by omega), - coeff_mulUpTo (n - 1) _ _ i (by omega), if_pos (by omega), - coeff_mul _ _ i (by omega), coeff_mul _ _ i (by omega)] - congr 1 - unfold convCoeff - apply List.foldl_add_congr - intro j hj - have hj' : j < i + 1 := List.mem_range.mp hj - rw [coeff_truncate _ _ (i - j) (by omega), - coeff_truncate _ _ (i - j) (by omega), - coeff_invUpTo m a 1 hau (i - j) (by omega), if_pos (by omega), - coeff_invUpTo n a 1 hau (i - j) (by omega), if_pos (by omega)] + (ha : (a - 1).coeff 0 = 0) : Agree m (logUpTo m a) (log a) := by + by_cases hn : 0 < n + · have ha0 : a.coeff 0 = 1 := by + rw [coeff_sub a 1 0 hn, coeff_one 0 hn] at ha + grind + intro i hi him + have hau : a.coeff 0 * 1 = 1 := by rw [ha0]; grind + unfold log logUpTo + rw [coeff_ofFn _ i hi, if_pos him, coeff_ofFn _ i hi, if_pos hi, + coeff_truncate _ _ i hi, coeff_truncate _ _ i hi] + cases i with + | zero => + rw [coeff_integrate _ 0 (by omega), coeff_integrate _ 0 (by omega)] + simp + | succ i => + rw [coeff_integrate _ (i + 1) (by omega), + coeff_integrate _ (i + 1) (by omega)] + simp only [show i + 1 ≠ 0 by omega, if_false, Nat.add_sub_cancel] + rw [coeff_mulUpTo (m - 1) _ _ i (by omega), if_pos (by omega), + coeff_mulUpTo (n - 1) _ _ i (by omega), if_pos (by omega), + coeff_mul _ _ i (by omega), coeff_mul _ _ i (by omega)] + congr 1 + unfold convCoeff + apply List.foldl_add_congr + intro j hj + have hj' : j < i + 1 := List.mem_range.mp hj + rw [coeff_truncate _ _ (i - j) (by omega), + coeff_truncate _ _ (i - j) (by omega), + coeff_invUpTo m a 1 hau (i - j) (by omega), if_pos (by omega), + coeff_invUpTo n a 1 hau (i - j) (by omega), if_pos (by omega)] + · intro i hi _ + omega private theorem log_agree [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (p : Nat) (hp : 0 < p) (a b : TSeries R n) @@ -445,7 +453,7 @@ private theorem expStep_correct [Lean.Grind.CommRing R] have hfactor : Agree m factor (1 + e) := by have h := Agree.sub (Agree.add (Agree.refl m (C 1)) (Agree.refl m a)) - (logUpTo_agree m y hy) + (logUpTo_agree m y (logArg y hy)) have halg : C 1 + a - log y = 1 + e := by dsimp only [e] rw [C_one] @@ -493,7 +501,7 @@ private theorem expStep_stable [Lean.Grind.CommRing R] have hfactor : Agree m factor (1 + e) := by have h := Agree.sub (Agree.add (Agree.refl m (C 1)) (Agree.refl m a)) - (logUpTo_agree m y hy) + (logUpTo_agree m y (logArg y hy)) have halg : C 1 + a - log y = 1 + e := by dsimp only [e] rw [C_one] diff --git a/HexTruncatedSeries/ModuleBoundaryTests.lean b/HexTruncatedSeries/ModuleBoundaryTests.lean index 92e6d2710..2f1dd8151 100644 --- a/HexTruncatedSeries/ModuleBoundaryTests.lean +++ b/HexTruncatedSeries/ModuleBoundaryTests.lean @@ -74,6 +74,22 @@ example (c : TSeries Int 8) (k : Nat) : k < 8 ∧ c.coeff k ≠ 0 ∧ ∀ i, i < k → c.coeff i = 0 := by exact valuation?_eq_some_iff c k +/-- Bounded square-root lifting exposes its prefix contract downstream. -/ +example (c : TSeries Rat 8) (r v : Rat) + (hr : r * r = c.coeff 0) (hv : ((1 + 1) * r) * v = 1) : + Agree 5 (sqrtUpTo 5 c r v) (sqrtOfRoot c r v) := by + exact sqrtUpTo_agree 5 c r v hr hv + +/-- Bounded logarithm exposes its prefix contract downstream. -/ +example (c : TSeries Rat 8) (h0 : (c - 1).coeff 0 = 0) : + Agree 5 (logUpTo 5 c) (log c) := by + exact logUpTo_agree 5 c h0 + +/-- Bounded exponential exposes its prefix contract downstream. -/ +example (c : TSeries Rat 8) (h0 : c.coeff 0 = 0) : + Agree 5 (expUpTo 5 c) (exp c) := by + exact expUpTo_agree 5 c h0 + /-- Bounded reversion agrees with the full Newton result throughout the requested prefix. -/ example (c : TSeries Int 8) (v : Int) diff --git a/HexTruncatedSeries/SPEC/hex-truncated-series.md b/HexTruncatedSeries/SPEC/hex-truncated-series.md index a1d4f89ca..7ac12c84a 100644 --- a/HexTruncatedSeries/SPEC/hex-truncated-series.md +++ b/HexTruncatedSeries/SPEC/hex-truncated-series.md @@ -656,6 +656,8 @@ def Agree (p : Nat) (a b : TSeries R n) : Prop := theorem sqrtUpTo_agree (m : Nat) (hr : r * r = a.coeff 0) (hv : ((1 + 1) * r) * v = 1) : Agree m (sqrtUpTo m a r v) (sqrtOfRoot a r v) +theorem logUpTo_agree (m : Nat) (ha : (a - 1).coeff 0 = 0) : + Agree m (logUpTo m a) (log a) theorem expUpTo_agree (m : Nat) (ha : a.coeff 0 = 0) : Agree m (expUpTo m a) (exp a) theorem revUpTo_agree (m : Nat) (h0 : b.coeff 0 = 0)