phi_sq
plain-language theorem explainer
The golden ratio satisfies the quadratic relation φ² = φ + 1. Researchers applying the Fibonacci-phi reduction to bound powers in cross-domain Recognition Science calculations would cite this as the base identity. The proof is a one-line wrapper referencing the established lemma in Constants.
Claim. The golden ratio satisfies $φ^2 = φ + 1$.
background
The Fibonacci-Phi Identity Universality module collects already-proved relations that reduce any power φ^n to the linear form F(n)·φ + F(n-1), where F is the Fibonacci sequence with F(0)=0 and F(1)=1. This supplies the arithmetic engine behind per-domain bounds such as φ^8 > 46. The upstream Constants.phi_sq_eq lemma derives the base case directly from the quadratic equation x² - x - 1 = 0 by algebraic simplification and linear combination.
proof idea
One-line wrapper that applies the phi_sq_eq lemma from Constants.
why it matters
This supplies the base case for all higher phi-power identities in the module, which in turn support cross-domain bounds on telomere halving and baryon asymmetry. It instantiates the self-similar fixed-point property of φ from the forcing chain (T5-T6). No open questions remain as the identity is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.