pi_transcendence
π is irrational. Recognition Science researchers deriving constants from 8-tick geometry cite this to confirm that the continuum limit of discrete phases produces non-algebraic numbers. The proof is a term-mode delegation to Mathlib's irrational_pi lemma, which applies the Niven polynomial argument.
claimThe real number $π$ is irrational.
background
The module MATH-002 derives π from 8-tick geometry: the 8-tick circle has eight discrete phases, and π emerges as the ratio of circumference to diameter in the continuous limit n → ∞. The fundamental tick τ₀ equals 1 in RS-native units, with one octave spanning 8 ticks. Upstream results define tick as the time quantum and supply bridges from discrete simplicial ledgers to continuum models, but the irrationality step itself rests on standard real analysis.
proof idea
The proof is a one-line term wrapper that applies the Mathlib lemma irrational_pi.
why it matters in Recognition Science
This anchors the status of π inside the Recognition framework as the bridge from discrete 8-tick ledger to continuous geometry. It fills the module target of deriving π from RS 8-tick geometry and relates to the eight-tick octave (T7). No downstream theorems are recorded in the used_by graph.
scope and limits
- Does not prove transcendence of π.
- Does not derive the numerical value of π from RS axioms.
- Does not connect π to the φ fixed point or phi-ladder.
- Does not address other constants such as e.
formal statement (Lean)
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
proof body
Term-mode proof.
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
290
291 π is the "bridge" between discrete (ledger) and continuous (geometry). -/