phi_fixed_point
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1. Anyone citing the self-similarity fixed point, the reciprocal-shift uniqueness argument, or the φ self-similarity certificate needs this algebraic identity. The proof unfolds the closed form (1+√5)/2, normalizes by ring, and closes with (√5)² = 5 plus linear arithmetic.
Claim. Let $\varphi = \frac{1 + \sqrt{5}}{2}$. Then $\varphi^{2} = \varphi + 1$.
background
The module Verification.Dimension proves that RSCounting together with 45-gap synchronization forces spatial dimension $D = 3$, with the iff form RSCounting_Gap45_Absolute $D \leftrightarrow D = 3$. Beside those rigidity results it records elementary facts about the golden ratio used by self-similarity certificates.
In Recognition Science, $\varphi$ is the unique self-similar fixed point forced at T6 of the forcing chain. Its closed form is the positive root of $x^{2} - x - 1 = 0$, written $\varphi = (1+\sqrt{5})/2$. The squared identity $\varphi^{2} = \varphi + 1$ is the polynomial form of that equation; the reciprocal form $\varphi = 1 + 1/\varphi$ is the algebraic corollary used by the reciprocal-generator lemmas upstream in PhiSupport.
Locally, $\varphi$ is the same constant appearing next to the Hopf-linking penalty $\ln\varphi$ and the $D=3$ witnesses in this file.
proof idea
Unfold $\varphi$ to its closed form $(1+\sqrt{5})/2$. Apply ring normalization to the target equality. Insert the elementary fact $(\sqrt{5})^{2} = 5$, obtained from Real.sq_sqrt with nonnegativity of 5 by norm_num. Finish by linear arithmetic on the normalized identity.
why it matters
This identity is the algebraic base of T6: $\varphi$ forced as the self-similar fixed point. Downstream, ReciprocalGenerator uses it (via the PhiSupport corollary) to prove that $\varphi$ is a fixed point of the $\iota$-shift and the unique such fixed point among reals $> 1$. PhiSelfSimilarityCert packages the reciprocal form $\varphi = 1 + 1/\varphi$ as a verification predicate certifying "the defining recursive structure of the golden ratio."
Within this module the lemma sits beside the $D=3$ rigidity chain (T8) and the Hopf-linking penalty $\ln\varphi$, so dimension counting and the $\varphi$-ladder share a common algebraic seed. It does not itself force $\varphi$ from the Recognition Composition Law; it only discharges the closed-form identity once $\varphi$ is defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.