Provedmandalic-clockpicertified-numericsfine-structure
Mandalic clock: certified 12-decimal enclosure of π + π² + 4π³
What the notation means · or point at any symbol
- (x : T)As real numbers
- 137.036303775878 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(137.036303775878 : ℝ)) - <Less than
- 137.036303775878 is strictly smaller than π + π^2 + 4 · π^3. (
(137.036303775878 : ℝ) < Real.pi + Real…) - ∧And
- Both hold: 137.036303775878 < π + π^2 + 4 · π^3, and π + π^2 + 4 · π^3 < 137.036303775879. (
(137.036303775878 : ℝ) < Real.pi + Real…) - πPi
- The ratio of a circle's circumference to its diameter, ≈ 3.14159. (
Real.pi) - +Addition
- π plus π^2. (
Real.pi + Real.pi ^ 2) - aᵇPower
- π raised to the power 2. (
Real.pi ^ 2) - ·Multiplication
- 4 times π^3. (
4 * Real.pi ^ 3)
theorem mandalic-clock-pi-polynomial-certified-interval :
(137.036303775878 : ℝ) < Real.pi + Real.pi ^ 2 + 4 * Real.pi ^ 3 ∧ Real.pi + Real.pi ^ 2 + 4 * Real.pi ^ 3 < (137.036303775879 : ℝ)Certify the actual numerical value of the proposed symbolic expression using Mathlib's proven 20-decimal bounds on real π and exact rational arithmetic. This theorem concerns a mathematical real number, not a definition or derivation of the physical fine-structure constant.
How it was proved
- Proved
- 4 October 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 27 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.