phi_not_rational
plain-language theorem explainer
The theorem shows that the golden ratio φ cannot equal any rational number when viewed in the reals. Researchers on computation limits in Recognition Science cite it to establish that φ-based states cannot be captured exactly by finite rational arithmetic. The term-mode proof reduces the universal claim to the known irrationality of φ by exhibiting any assumed rational witness as a range member.
Claim. $∀ q ∈ ℚ, (q : ℝ) ≠ φ$, where φ denotes the golden ratio.
background
Module IC-002 derives fundamental computation limits from temporal discreteness, irrational constants, and thermodynamic costs. One source is the irrationality of φ: φ-based states cannot be represented exactly with finite rational arithmetic, forcing any exact simulation of RS dynamics to use transcendental precision. Upstream, phi_irrational establishes that φ equals Mathlib's goldenRatio and is therefore irrational via the irrationality of √5.
proof idea
Term-mode proof. It introduces an arbitrary rational q and an equality hypothesis, then applies the phi_irrational theorem by constructing a witness that places q in the range of the rational-to-real embedding, yielding an immediate contradiction.
why it matters
This supplies IC-002.5 inside the computation-limits structure, closing the argument that irrational constants block exact finite algorithms for RS dynamics. It supports the module's claim that maximum bit rate and precision floors arise directly from the tick and from φ's irrationality, without feeding any downstream declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.