phi_irrational_information
plain-language theorem explainer
The theorem establishes that the golden ratio φ is irrational, so φ-encoded information in the RS ledger cannot be captured exactly by rational arithmetic. Researchers on the information-ledger equivalence cite it to show that the fundamental constant introduces irreducible transcendence. The proof is a direct one-line reference to the upstream irrationality result for φ in the constants module.
Claim. The golden ratio $φ = (1 + √5)/2$ is irrational.
background
The module InformationIsLedger treats information as the physical ledger: every recognition event is a ratio x > 0 carrying J-cost J(x) = (x + 1/x)/2 − 1, with J(x) = 0 precisely when x = 1 (balanced state, zero information). The module derives eight core statements, including non-negativity of J-cost, symmetry J(x) = J(1/x), and the identification of Shannon entropy with expected J-cost. Upstream, phi_irrational states that φ is irrational (degree 2 algebraic, not rational) because it equals Mathlib's goldenRatio, whose irrationality follows from that of √5.
proof idea
This is a one-line term-mode wrapper that applies the theorem phi_irrational from IndisputableMonolith.Constants, which itself reduces the claim to Real.goldenRatio_irrational via the equality phi = Real.goldenRatio.
why it matters
The result supplies IC-001.19 inside the Information Is Ledger module and is referenced by the ic001_certificate that assembles the full derived status of the ledger claim. It anchors the framework landmark that φ is the self-similar fixed point forced at T6 of the unified forcing chain and appears in the phi-ladder mass formula and the alpha band (137.030, 137.039). The irrationality prevents any rational truncation of the ledger constant and thereby closes one route to rationalizing the entire RS structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.