phi_irrational
plain-language theorem explainer
Phi, the golden ratio fixed point forced in the Recognition Science chain, is irrational. Framework developers working on information ledgers and computation bounds cite the result to establish that phi-based structures admit no exact rational representation. The proof is a term reduction that equates the local definition to Mathlib's goldenRatio and invokes the library fact on the irrationality of sqrt(5).
Claim. The golden ratio $phi = (1 + sqrt(5))/2$, the unique positive root of $x^2 - x - 1 = 0$, is irrational.
background
The Constants module introduces the core numerical constants of Recognition Science, with phi as the self-similar fixed point obtained from the forcing chain at step T6. It satisfies the quadratic $phi^2 = phi + 1$ and enters the J-cost function, the phi-ladder for masses, and the eight-tick octave. The module also fixes the fundamental time quantum tau_0 equal to one tick in RS-native units. Upstream results supply the identity event at zero J-cost and the primitive distinction axioms that generate the structural conditions under which phi appears.
proof idea
This is a term-mode proof. It first records the definitional equality between the local phi and Real.goldenRatio by reflexivity, rewrites the goal, and applies the library lemma Real.goldenRatio_irrational, whose own justification rests on the irrationality of sqrt(5) for prime 5.
why it matters
The result is invoked by the computation-limits structure (IC-002.5) and the information-is-ledger theorem (IC-001.19) to conclude that phi cannot be captured exactly by rational arithmetic. It completes the T6 forcing step that installs phi as the self-similar fixed point and supports the subsequent claims for the eight-tick octave and D = 3. It leaves open the precise interface between this algebraic irrationality and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.