phi_sq
plain-language theorem explainer
The golden ratio satisfies its defining quadratic equation. Interval arithmetic workers in Recognition Science cite this identity when establishing monotonicity and bounds on the phi ladder for mass and coupling calculations. The proof is a direct term-mode invocation of the matching Mathlib fact followed by simplification on the definition.
Claim. Let $φ$ be the golden ratio. Then $φ^2 = φ + 1$.
background
The Numerics.IntervalProofs module supplies minimal helpers that convert small numerical inequalities into Lean proofs while avoiding heavy dependencies; it relies on norm_num together with monotonicity and interval tactics. This lemma supplies a rewrite convenience for the golden-ratio identity that appears repeatedly in phi-bound arguments. It sits downstream of the meta-realization structure in UniversalForcingSelfReference, whose doc-comment records the structural properties required by self-reference axioms.
proof idea
One-line wrapper that applies the Mathlib fact Real.goldenRatio_mul_goldenRatio and simplifies using the definitions of goldenRatio and pow_two.
why it matters
The lemma anchors the algebraic properties of phi used throughout the numerics layer that supports the phi-ladder mass formula and the alpha band. It directly instantiates the self-similar fixed point required by T6 of the forcing chain. No downstream theorems are recorded yet, so the result remains a local convenience rather than a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.