Skip to content

feat(truncated-series): expose bounded log agreement #9873

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kim-em merged 1 commit into from
Aug 31, 2026
Merged

feat(truncated-series): expose bounded log agreement #9873

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
66 changes: 37 additions & 29 deletions HexTruncatedSeries/ExpLog.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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]
Expand Down
16 changes: 16 additions & 0 deletions HexTruncatedSeries/ModuleBoundaryTests.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 2 additions & 0 deletions HexTruncatedSeries/SPEC/hex-truncated-series.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Loading