Certified numeric facts for the Chudnovsky formula (Phase D1) #
Sorried stubs for the certified numeric bounds consumed by Phase D
(Coefficients.lean, ch. 10 of Milla, arXiv:1809.00533v6): high-precision bounds
for π, √163, and the nome magnitude e^{-π√163} = ‖q τ₁₆₃‖, together with the
exact evaluation q τ₁₆₃ = -e^{-π√163} (a negative real number, since
e^{2πi·(1/2)} = -1).
Per PLAN.md (D1), these will eventually be proved by a small ℚ-interval-arithmetic
layer (directed-rounding add/mul/div, Real.exp_bound Taylor remainders, rational
square-root approximation + nlinarith), extending the machinery of
Mathlib.Analysis.Real.Pi.Bounds for the π bounds.
Every digit string below has been verified by exact rational arithmetic
(80-digit Decimal computation of π via Machin's formula, √163, and
exp (-π·√163), then interval checks with fractions.Fraction):
π = 3.14159265358979323846 26433832795028841971693993751…√163 = 12.7671453348037046617 10952009780892347382363780301…(checked by squaring the rational endpoints:lo² < 163 < hi²)e^{-π√163} = 3.80898093700765233822623151647 80054376196293193806…e-18
Bounds for π #
π = 3.14159265358979323846264338327950288419716939937510…
High-precision lower bound for π (21 significant digits).
To be proved by the Mathlib.Analysis.Real.Pi.Bounds machinery (PLAN D1).
High-precision upper bound for π (21 significant digits).
To be proved by the Mathlib.Analysis.Real.Pi.Bounds machinery (PLAN D1).
Bounds for √163 #
√163 = 12.7671453348037046617109520097808923473823637803013…;
the endpoint rationals below satisfy lo² < 163 < hi² (verified exactly).
Lower bound for √163 (21 significant digits). To be proved from
lo² < 163 via Real.lt_sqrt / nlinarith (PLAN D1).
Upper bound for √163 (21 significant digits). To be proved from
163 < hi² via Real.sqrt_lt' / nlinarith (PLAN D1).
High-precision internal bounds (Phase D1 certificates) #
The two theorems on e^{-π√163} need π and √163 to far more than the 21 digits
of pi_gt_high_precision. We certify π and √163 to 38 decimal places internally,
using Mathlib's pi_lower_bound/pi_upper_bound witness machinery (the certificate
rationals were generated by exact-arithmetic directed rounding) and rational squaring.
All arithmetic is checked by the kernel via norm_num.
Bounds for e^{-π√163} #
e^{-π√163} = 3.808980937007652338226231516478005437619629319381…e-18
(30 significant digits certified below). This is ‖q τ₁₆₃‖, the quantity all
the truncation-error estimates of ch. 5/10 are evaluated at.
Lower bound for e^{-π√163} (30 significant digits), i.e.
380898093700765233822623151647 / 10^47 < e^{-π√163}.
To be proved by ℚ-interval arithmetic + Real.exp_bound (PLAN D1).
Upper bound for e^{-π√163} (30 significant digits), i.e.
e^{-π√163} < 380898093700765233822623151648 / 10^47.
To be proved by ℚ-interval arithmetic + Real.exp_bound (PLAN D1).