Provedalphabaguettebaguette-zv2
An int32 grid of 2⁻³⁰ rounds a typical second moment 10⁻¹² to zero; a 2⁻⁶⁰ grid keeps it at ≥ 10⁶ ulps
What the notation means · or point at any symbol
- ⌊x⌋Floor
- The largest integer not above 1/10^12 · 2^30. (
⌊(1 / 10 ^ 12 : ℝ) * 2 ^ 30⌋) - =Equality
- ⌊1/10^12 · 2^30⌋ and 0 are the same. (
⌊(1 / 10 ^ 12 : ℝ) * 2 ^ 30⌋ = 0) - ∧And
- Both hold: ⌊1/10^12 · 2^30⌋ = 0, and 10^6 ≤ 1/10^12 · 2^60. (
⌊(1 / 10 ^ 12 : ℝ) * 2 ^ 30⌋ = 0 ∧ (10 …) - (x : T)As real numbers
- 1/10^12 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 / 10 ^ 12 : ℝ)) - ·Multiplication
- 1/10^12 times 2^30. (
(1 / 10 ^ 12 : ℝ) * 2 ^ 30) - a/bDivision
- 1 divided by 10^12. In Lean, dividing by 0 gives 0. (
1 / 10 ^ 12) - aᵇPower
- 10 raised to the power 12. (
10 ^ 12) - ≤At most
- 10^6 is less than or equal to 1/10^12 · 2^60. (
(10 ^ 6 : ℝ) ≤ (1 / 10 ^ 12 : ℝ) * 2 ^ …)
theorem bz2-int32-moment-underflow :
⌊(1 / 10 ^ 12 : ℝ) * 2 ^ 30⌋ = 0 ∧ (10 ^ 6 : ℝ) ≤ (1 / 10 ^ 12 : ℝ) * 2 ^ 60Formal record of review S6: ⌊10⁻¹²·2³⁰⌋ = 0 (the v1 plan's moment format would have zeroed v and made Adam's direction m/ε explode), while 10⁻¹²·2⁶⁰ ≥ 10⁶ (relative precision ≤ 10⁻⁶ by bz2-moment-resolution). Part of 'Baguette-Z v2' (revision after the hostile review).
How it was proved
- Proved
- 3 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- 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
- 15 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.