proofs
Provedmandalic-clockfine-structurecodata-2022conditional-comparison

Mandalic clock: exact CODATA error, ppm bounds, and conditional separation

(0.000304598878<π+π2+4⋅π3−137.035999177∧π+π2+4⋅π3−137.035999177<0.000304598879)∧(2.22276540<π+π2+4⋅π3−137.035999177137.035999177⋅1000000∧π+π2+4⋅π3−137.035999177137.035999177⋅1000000<2.22276542)∧(∀a∈R,∣a−137.035999177∣≤0.000000021  ⟹  14000⋅0.000000021<π+π2+4⋅π3−a∧π+π2+4⋅π3≠a)\begin{aligned} & \left(\right. \htmlData{mx=2}{0.000304598878} \mathrel{\htmlData{mx=12}{<}} \htmlData{mx=11}{\htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=3}{\pi} + \htmlData{mx=5}{\htmlData{mx=4}{\pi}^{2}}} + \htmlData{mx=9}{4 \cdot \htmlData{mx=8}{\htmlData{mx=7}{\pi}^{3}}}} - 137.035999177} \\ & \htmlData{mx=1}{\land} \htmlData{mx=21}{\htmlData{mx=20}{\htmlData{mx=16}{\htmlData{mx=13}{\pi} + \htmlData{mx=15}{\htmlData{mx=14}{\pi}^{2}}} + \htmlData{mx=19}{4 \cdot \htmlData{mx=18}{\htmlData{mx=17}{\pi}^{3}}}} - 137.035999177} \mathrel{\htmlData{mx=23}{<}} \htmlData{mx=22}{0.000304598879} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=26}{2.22276540} \\ & \quad \htmlData{mx=25}{<} \htmlData{mx=37}{\htmlData{mx=36}{\frac{\htmlData{mx=35}{\htmlData{mx=34}{\htmlData{mx=30}{\htmlData{mx=27}{\pi} + \htmlData{mx=29}{\htmlData{mx=28}{\pi}^{2}}} + \htmlData{mx=33}{4 \cdot \htmlData{mx=32}{\htmlData{mx=31}{\pi}^{3}}}} - 137.035999177}}{137.035999177}} \cdot 1000000} \\ & \htmlData{mx=24}{\land} \htmlData{mx=49}{\htmlData{mx=48}{\frac{\htmlData{mx=47}{\htmlData{mx=46}{\htmlData{mx=42}{\htmlData{mx=39}{\pi} + \htmlData{mx=41}{\htmlData{mx=40}{\pi}^{2}}} + \htmlData{mx=45}{4 \cdot \htmlData{mx=44}{\htmlData{mx=43}{\pi}^{3}}}} - 137.035999177}}{137.035999177}} \cdot 1000000} \\ & \quad \htmlData{mx=38}{<} \htmlData{mx=50}{2.22276542} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=51}{\forall} a \in \htmlData{mx=52}{\mathbb{R}}, \\ & \quad \htmlData{mx=56}{\left\lvert \htmlData{mx=55}{\htmlData{mx=54}{a} - 137.035999177} \right\rvert} \mathrel{\htmlData{mx=57}{\leq}} 0.000000021 \\ & \quad \htmlData{mx=53}{\implies} \htmlData{mx=60}{14000 \cdot \htmlData{mx=59}{0.000000021}} \mathrel{\htmlData{mx=71}{<}} \htmlData{mx=70}{\htmlData{mx=68}{\htmlData{mx=64}{\htmlData{mx=61}{\pi} + \htmlData{mx=63}{\htmlData{mx=62}{\pi}^{2}}} + \htmlData{mx=67}{4 \cdot \htmlData{mx=66}{\htmlData{mx=65}{\pi}^{3}}}} - \htmlData{mx=69}{a}} \\ & \quad \htmlData{mx=58}{\land} \htmlData{mx=79}{\htmlData{mx=75}{\htmlData{mx=72}{\pi} + \htmlData{mx=74}{\htmlData{mx=73}{\pi}^{2}}} + \htmlData{mx=78}{4 \cdot \htmlData{mx=77}{\htmlData{mx=76}{\pi}^{3}}}} \mathrel{\htmlData{mx=81}{\neq}} \htmlData{mx=80}{a} \left.\right) \end{aligned}
What the notation means · or point at any symbol
(x : T)As real numbers
0.000304598878 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((0.000304598878 : ℝ))
<Less than
0.000304598878 is strictly smaller than π + π^2 + 4 · π^3 − 137.035999177. ((0.000304598878 : ℝ) < Real.pi + Real.p…)
∧And
Both hold: 0.000304598878 < π + π^2 + 4 · π^3 − 137.035999177, and π + π^2 + 4 · π^3 − 137.035999177 < 0.000304598879. ((0.000304598878 : ℝ) < Real.pi + Real.p…)
πPi
The ratio of a circle's circumference to its diameter, ≈ 3.14159. (Real.pi)
+Addition
π plus π^2. (Real.pi + Real.pi ^ 2)
-Subtraction
π + π^2 + 4 · π^3 minus 137.035999177. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (Real.pi + Real.pi ^ 2 + 4 * Real.pi ^ 3…)
aᵇPower
π raised to the power 2. (Real.pi ^ 2)
·Multiplication
4 times π^3. (4 * Real.pi ^ 3)
a/bDivision
π + π^2 + 4 · π^3 − 137.035999177 divided by 137.035999177. In Lean, dividing by 0 gives 0. ((Real.pi + Real.pi ^ 2 + 4 * Real.pi ^ …)
∀For all
The statement after the comma holds for every a. (∀ a : ℝ, |a - 137.035999177| ≤ 0.000000…)
RReal numbers
The real numbers: every point on the number line. (ℝ)
|x|Absolute value
The size of a − 137.035999177 without its sign. (|a - 137.035999177|)
≤At most
|a − 137.035999177| is less than or equal to 0.000000021. (|a - 137.035999177| ≤ 0.000000021)
⟹Implies
If |a − 137.035999177| ≤ 0.000000021, then 14000 · 0.000000021 < π + π^2 + 4 · π^3 − a ∧ π + π^2 + 4 …. (Between types, A → B is the type of functions from A to B.) (|a - 137.035999177| ≤ 0.000000021 → 140…)
≠Not equal
π + π^2 + 4 · π^3 and a are different. (Real.pi + Real.pi ^ 2 + 4 * Real.pi ^ 3…)

Use fixed rational data C=137.035999177 and standard uncertainty u=0.000000021 from NIST CODATA 2022. Bound P-C and its relative error in ppm. Prove that any real a satisfying the explicitly assumed interval |a-C| <= u lies more than 14000u below P. No assertion is made that the actual constant is guaranteed to lie in a one-standard-uncertainty interval; this is a conditional arithmetic result.

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
60 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements