phi_satisfies_fixed_point
plain-language theorem explainer
The golden ratio satisfies the quadratic fixed-point equation φ² = φ + 1 required by the Recognition cost function. Ledger-uniqueness arguments cite this identity to anchor the specific choice of φ inside the discrete conservative system. The term-mode proof unfolds the explicit definition of φ and reduces the equation by squaring the square root of 5, followed by ring normalization and linear arithmetic.
Claim. Let φ = (1 + √5)/2. Then φ² = φ + 1.
background
The Ledger Uniqueness module resolves the objection that other discrete structures could satisfy discreteness and conservation by proving each component is the unique solution to its forcing constraint. For φ the constraint is the cost-function fixed point J(x) = J(1/x) with minimal curvature; the positive solution is the golden ratio. This sits inside the forcing chain where T6 identifies φ as the self-similar fixed point of the Recognition Composition Law.
proof idea
The proof is a short term-mode calculation. It unfolds the definition of phi, records the auxiliary equality (√5)² = 5, applies ring normalization to expand the left-hand side, and closes the goal with linear arithmetic on the resulting polynomial identity.
why it matters
This supplies the algebraic verification that φ meets the fixed-point equation demanded by the cost function. It supports the module's main claim that any discrete conservative system is isomorphic to the RS ledger built from φ, Q₃ and the 8-tick cycle. The result directly instantiates the T6 step of the forcing chain; the companion theorem phi_unique_fixed_point then proves uniqueness of this solution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.