pith. machine review for the scientific record. sign in
def definition def or abbrev

piInPhysics

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 259def piInPhysics : List String := [

proof body

Definition body.

 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). -/

depends on (15)

Lean names referenced from this declaration's body.