phi_fixed_point'
plain-language theorem explainer
The golden ratio satisfies the fixed-point relation φ = 1 + φ^{-1}. Researchers deriving self-similar structures from the Recognition Science forcing chain cite this algebraic identity as T6. The proof reduces the squared relation φ² = φ + 1 by division after confirming positivity of φ.
Claim. $φ = 1 + φ^{-1}$ where $φ = (1 + √5)/2$ is the golden ratio satisfying the defining relation $φ^2 = φ + 1$.
background
The module PhiSupport supplies supporting identities for the golden ratio under the Recognition Science framework. The upstream theorem phi_squared states that φ² = φ + 1, proved by unfolding the explicit definition φ = (1 + √5)/2 and applying ring normalization. MODULE_DOC records the same squared relation as the defining equation of the golden ratio. The primer identifies T6 as the step that forces phi as the self-similar fixed point of the forcing chain T0–T8.
proof idea
One-line wrapper that invokes phi_squared, establishes positivity via phi_pos, then applies field_simp followed by linarith to obtain the fixed-point form.
why it matters
This identity supplies the explicit fixed-point equation required by T6 in the forcing chain. It sits inside the phi-ladder constructions that later yield the mass formula and the eight-tick octave. No downstream declarations are recorded, indicating it functions as a basic algebraic building block rather than a terminal result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.