phi_sq_identity
plain-language theorem explainer
The golden ratio satisfies the algebraic relation φ² = φ + 1. Number theorists cataloguing RS identities and linguists constructing lexicon ratio certificates cite this fact directly. The proof is a one-line wrapper that reuses the phi_sq_eq lemma from the constants module.
Claim. The golden ratio φ satisfies φ² = φ + 1.
background
The Number Theory from RS module catalogues five canonical identities, the second of which is the algebraic property of the golden ratio. This identity originates from the quadratic equation x² - x - 1 = 0 whose positive root defines φ. Upstream lemmas in Constants and PhiLadderLattice establish the same relation by explicit computation with the square root of five.
proof idea
The declaration is a one-line wrapper that applies the phi_sq_eq lemma imported from IndisputableMonolith.Constants.
why it matters
This identity is the second of the five canonical RS number-theoretic identities listed in the module documentation. It supplies the phi_sq field in numberTheoryCert and the phi_sq_identity clause in the LexiconRatioCert structure. In the Recognition framework it encodes the self-similar fixed point of the J-function on the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.