phi_sq_identity
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of φ from the forcing chain.
- Does not prove Fibonacci relations for higher powers such as φ^5.
- Does not connect the identity to physical constants or spatial dimensions.
- Does not address uniqueness of the positive root of the quadratic.
formal statement (Lean)
31theorem phi_sq_identity : phi ^ 2 = phi + 1 := phi_sq_eq
proof body
Term-mode proof.
32
33/-- φ^5 = 5φ+3 (Fibonacci). -/