phi_sq
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1 as its defining algebraic relation once self-similar ledger closure is imposed. Researchers closing the meta-principle derivation to constants would cite this identity. The proof unfolds the explicit definition of φ, verifies (√5)² = 5, and reduces the equation via ring normalization.
Claim. Let φ = (1 + √5)/2. Then φ² = φ + 1.
background
The Meta-Principle asserts that empty recognition is impossible, forcing a ledger whose self-similar closure selects φ. In this module φ is introduced as the positive root of the quadratic that encodes fixed-point self-similarity. Upstream results on magnitude-of-mismatch and simplicial edge lengths supply the comparison operators that make the ledger well-defined before φ appears.
proof idea
Unfold the definition of φ. Introduce the auxiliary fact that (√5)² = 5 via Real.sq_sqrt. Apply ring_nf to expand, rewrite with the auxiliary fact, and close with the ring tactic.
why it matters
The identity confirms the algebraic property of the self-similar fixed point that the meta-principle forces after ledger construction. It supplies the relation used to obtain RS-native constants (c = 1, ħ = φ^{-5}, G = φ^5/π) and the eight-tick octave. No downstream uses are recorded yet, but the result sits between self_similarity_forces_phi and the constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.