perf(Zeta5Irrational): share rational certificate arithmetic

LeanPool/Zeta5Irrational/Table/RationalSeries.lean

@@ -6,12 +6,16 @@ Authors: Lean Pool contributors
 module
 
 public import LeanPool.Zeta5Irrational.TableCheck
+import Mathlib.Analysis.Complex.ExponentialBounds
+import Mathlib.Tactic.Linarith
 
 /-!
 # Rational certificates for finite analytic series
 
 The table bounds use only rational inputs. Check their finite sums in `ℚ`, then transport
 one inequality to `ℝ`, avoiding a separate normalization proof for every real operation.
+Binary range reduction also checks its rational rounding bound before using the shared
+lower bound on `Real.log 2`.
 -/
 
 public section
@@ -62,4 +66,24 @@ lemma arctan_le_of_series_rat {z U : ℚ} (k : ℕ)
   simpa only [Rat.cast_add, Rat.cast_mul, Rat.cast_sum, Rat.cast_div, Rat.cast_pow,
     Rat.cast_sub, Rat.cast_one, Rat.cast_ofNat, Rat.cast_natCast, Rat.cast_neg] using h
 
+/-- Check binary range reduction and its final logarithm bound in the rationals. -/
+lemma log_le_of_split_neg_rational {r r' U U' : ℚ} (power m : ℕ)
+    (certificate : 1 ≤ r' ∧
+      2 * ∑ k ∈ range m, (1 / (2 * (k : ℚ) + 1)) * ((r' - 1) / (r' + 1)) ^ (2 * k + 1) +
+          2 * ((r' - 1) / (r' + 1)) ^ (2 * m + 1) /
+            ((2 * m + 1) * (1 - ((r' - 1) / (r' + 1)) ^ 2)) ≤ U')
+    (reduction : r = r' / 2 ^ power ∧ U' - power * (6931471803 / 10000000000) ≤ U) :
+    Real.log (r : ℝ) ≤ (U : ℝ) := by
+  have hr : (r : ℝ) = (r' : ℝ) / 2 ^ power := by exact_mod_cast reduction.1
+  have hr' : (0 : ℝ) < r' := by
+    exact_mod_cast (lt_of_lt_of_le (by decide : (0 : ℚ) < 1) certificate.1)
+  have h := log_le_of_split_neg power hr hr' (log_le_of_ge_one_rat m certificate)
+  have hround : (U' : ℝ) - power * (6931471803 / 10000000000) ≤ U := by
+    simpa only [Rat.cast_sub, Rat.cast_mul, Rat.cast_natCast, Rat.cast_div,
+      Rat.cast_ofNat] using (Rat.cast_le (K := ℝ)).2 reduction.2
+  have hlog : (6931471803 / 10000000000 : ℝ) ≤ Real.log 2 := by
+    linarith only [Real.log_two_gt_d9]
+  have hmul := mul_le_mul_of_nonneg_left hlog (Nat.cast_nonneg (α := ℝ) power)
+  exact h.trans ((sub_le_sub_left hmul _).trans hround)
+
 end Zeta5Irrational

LeanPool/Zeta5Irrational/Table/UpperCertificate.lean

@@ -10,7 +10,11 @@ public import LeanPool.Zeta5Irrational.Table.Common
 public import LeanPool.Zeta5Irrational.Certificates
 public import Mathlib.Analysis.Complex.ExponentialBounds
 
-/-! # Reusable upper certificates for arcsine potentials -/
+/-! # Reusable upper certificates for arcsine potentials
+
+The rational versions read endpoints from the existing table and transfer their closed
+arithmetic certificates to the real analytic lemmas once.
+-/
 
 @[expose] public section
 
@@ -36,4 +40,54 @@ lemma Uω_le_right_certificate {a b t s q U : ℝ} (hab : a < b) (ht : b ≤ t)
   apply (Real.log_le_log (by linarith) ?_).trans hlog
   linarith
 
+/-- The left endpoint of an arcsine interval, evaluated in the rationals. -/
+def rationalLeftEndpoint (j : ℕ) : ℚ :=
+  ((table1.getD (j - 1) (0, 0, 0)).1 : ℚ) / 10 ^ 12
+
+/-- The right endpoint of an arcsine interval, evaluated in the rationals. -/
+def rationalRightEndpoint (j : ℕ) : ℚ :=
+  ((table1.getD (j - 1) (0, 0, 0)).2.1 : ℚ) / 10 ^ 12
+
+lemma aρ_eq_rationalLeftEndpoint (j : ℕ) : aρ j = (rationalLeftEndpoint j : ℝ) := by
+  simp only [aρ, rationalLeftEndpoint, Rat.cast_div, Rat.cast_natCast,
+    Rat.cast_pow, Rat.cast_ofNat]
+
+lemma bρ_eq_rationalRightEndpoint (j : ℕ) : bρ j = (rationalRightEndpoint j : ℝ) := by
+  simp only [bρ, rationalRightEndpoint, Rat.cast_div, Rat.cast_natCast,
+    Rat.cast_pow, Rat.cast_ofNat]
+
+/-- A rational certificate to the left of a tabulated arcsine interval. -/
+lemma Uω_le_left_certificate_rational {j : ℕ} {t s q U : ℚ}
+    (certificate : rationalLeftEndpoint j < rationalRightEndpoint j ∧
+      t ≤ rationalLeftEndpoint j ∧ 0 ≤ s ∧
+      (t - rationalLeftEndpoint j) * (t - rationalRightEndpoint j) ≤ s ^ 2 ∧
+      ((rationalLeftEndpoint j + rationalRightEndpoint j) / 2 - t + s) / 2 ≤ q)
+    (hlog : Real.log (q : ℝ) ≤ (U : ℝ)) :
+    Uω (aρ j) (bρ j) (t : ℝ) ≤ (U : ℝ) := by
+  rw [aρ_eq_rationalLeftEndpoint, bρ_eq_rationalRightEndpoint]
+  apply Uω_le_left_certificate (s := (s : ℝ)) (q := (q : ℝ))
+  · exact_mod_cast certificate.1
+  · exact_mod_cast certificate.2.1
+  · exact_mod_cast certificate.2.2.1
+  · exact_mod_cast certificate.2.2.2.1
+  · exact_mod_cast certificate.2.2.2.2
+  · exact hlog
+
+/-- A rational certificate to the right of a tabulated arcsine interval. -/
+lemma Uω_le_right_certificate_rational {j : ℕ} {t s q U : ℚ}
+    (certificate : rationalLeftEndpoint j < rationalRightEndpoint j ∧
+      rationalRightEndpoint j ≤ t ∧ 0 ≤ s ∧
+      (t - rationalLeftEndpoint j) * (t - rationalRightEndpoint j) ≤ s ^ 2 ∧
+      (t - (rationalLeftEndpoint j + rationalRightEndpoint j) / 2 + s) / 2 ≤ q)
+    (hlog : Real.log (q : ℝ) ≤ (U : ℝ)) :
+    Uω (aρ j) (bρ j) (t : ℝ) ≤ (U : ℝ) := by
+  rw [aρ_eq_rationalLeftEndpoint, bρ_eq_rationalRightEndpoint]
+  apply Uω_le_right_certificate (s := (s : ℝ)) (q := (q : ℝ))
+  · exact_mod_cast certificate.1
+  · exact_mod_cast certificate.2.1
+  · exact_mod_cast certificate.2.2.1
+  · exact_mod_cast certificate.2.2.2.1
+  · exact_mod_cast certificate.2.2.2.2
+  · exact hlog
+
 end Zeta5Irrational