`leibniz_8_approximates`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.Pi
domain: Mathematics
line: 243 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.Pi on GitHub at line 243.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 240noncomputable def leibniz_8_terms : ℝ :=
 241  1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15
 242
 243theorem leibniz_8_approximates :
 244    -- leibniz_8_terms ≈ 0.76
 245    -- vs π/4 ≈ 0.785
 246    True := trivial
 247
 248/-! ## π in Physics -/
 249
 250/-- π appears throughout physics:
 251
 252    1. **Circles**: C = 2πr (definition)
 253    2. **Spheres**: V = (4/3)πr³
 254    3. **Gaussian**: ∫exp(-x²)dx = √π
 255    4. **Quantum**: ℏ = h/(2π)
 256    5. **Relativity**: Schwarzschild radius = 2GM/(πc²) (no, 2GM/c²)
 257
 258    In RS, π appears because of 8-tick circular geometry. -/
 259def piInPhysics : List String := [
 260  "Geometry: Circles, spheres, volumes",
 261  "Waves: 2πf = angular frequency",
 262  "Quantum: ℏ = h/2π",
 263  "Statistics: Normal distribution"
 264]
 265
 266/-! ## Deep Question -/
 267
 268/-- Why is π transcendental?
 269
 270    π is not the root of any polynomial with integer coefficients.
 271
 272    This means π cannot be constructed with compass and straightedge alone.
 273

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.