phi_sq
The theorem states that the golden ratio phi satisfies phi squared equals phi plus one. Researchers deriving self-similar fixed points in J-cost geometry cite this identity when constructing the phi-ladder for mass formulas. The proof unfolds the definition of phi and reduces the equation by invoking the square identity for the square root of five followed by nonlinear arithmetic.
claim$phi^2 = phi + 1$ where $phi = (1 + sqrt(5))/2$ is the positive root of the quadratic $x^2 - x - 1 = 0$.
background
The module JCostGeometry develops log-domain identities for the canonical reciprocal cost J(x) = 1/2 (x + x^{-1}) - 1. It extends the core definitions imported from JcostCore and supplies the algebraic facts required by the F1 foundation paper on simultaneous versus sequential descent. Phi enters as the self-similar fixed point of the J-cost recurrence, consistent with the forcing chain step that selects the unique positive solution to x^2 = x + 1.
proof idea
The tactic proof unfolds the definition of phi, asserts that zero is at most five, records that the square of the square root of five equals five, and closes the goal with nonlinear arithmetic.
why it matters in Recognition Science
This identity anchors the phi-ladder used in mass formulas and the eight-tick octave of the forcing chain. It supplies the algebraic relation needed for geometric-mean optimality results in the same module and for downstream claims on total J-cost minimization. The result closes a basic algebraic prerequisite for the F1 paper propositions on J-cost geometry.
scope and limits
- Does not prove that phi is the unique positive solution.
- Does not derive the J-cost functional equation.
- Does not connect phi to physical constants such as alpha or G.
- Does not address positivity or ordering properties of phi.
formal statement (Lean)
202theorem phi_sq : phi ^ 2 = phi + 1 := by
proof body
Tactic-mode proof.
203 unfold phi
204 have h5 : (0 : ℝ) ≤ 5 := by norm_num
205 have hsq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
206 nlinarith [hsq]
207
208/-- phi > 0 -/