piInPhysics

formal source

 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
 274    In RS terms: π emerges from the INFINITE limit of 8-tick geometry.
 275    The discreteness (algebraic) gives way to continuity (transcendental). -/
 276theorem pi_transcendence :
 277    -- π is irrational (Lindemann 1882 proved it is actually transcendental,
 278    -- but irrationality was shown earlier by Lambert in 1761)
 279    -- Mathlib proves irrationality via the Niven polynomial argument.
 280    Irrational Real.pi := irrational_pi
 281
 282/-! ## RS Perspective -/
 283
 284/-- RS perspective on π:
 285
 286    1. **8-tick discreteness**: Finite approximation
 287    2. **Continuum limit**: π emerges as n → ∞
 288    3. **φ connections**: cos(π/5) = φ/2, etc.
 289    4. **Transcendence**: From discrete → continuous