pi_transcendence
plain-language theorem explainer
π 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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.