phi_sq_eq'
plain-language theorem explainer
Local private restatement of the golden-ratio quadratic: φ² = φ + 1. Cosmology proofs that expand φ-powers via Fibonacci coefficients cite it (or its Constants parent). The body is a one-line term alias of the global identity lemma.
Claim. The golden ratio satisfies $\varphi^2 = \varphi + 1$, equivalently the root equation $x^2 - x - 1 = 0$.
background
In Recognition Science, $\varphi$ is the unique positive self-similar fixed point forced by the J-cost uniqueness step (T5–T6): it solves $x^2 = x + 1$. The Constants module records this as the key algebraic identity $\varphi^2 = \varphi + 1$, proved from the closed form $(\sqrt{5}+1)/2$ by clearing the square root and ring normalization.
This module certifies the baryon-to-photon interval prediction $\varphi^{-44}\in(5.5,7.5)\times 10^{-10}$, with Planck 2018 $\eta_B$ inside the band. The structural integer 44 factors as flip-count times torsion gap, the same 44 that appears in the $\alpha^{-1}$ formula. Bounding $\varphi^{\pm 44}$ uses the Fibonacci–φ recurrence, which rests on the quadratic relation at every inductive step.
proof idea
One-line term wrapper: the goal is definitionally the statement of Constants.phi_sq_eq, so the proof is just that lemma (no tactics, no extra hypotheses). Sibling cosmology modules re-export the same fact the same way.
why it matters
Without $\varphi^2=\varphi+1$, the Fibonacci identity $\varphi^{n+1}=F_{n+1}\varphi+F_n$ does not close, and the concrete decimal bounds on $\varphi^{44}$ and $\varphi^{-44}$ cannot be discharged. Those bounds are the arithmetic spine of eta_B_interval and the master EtaBCert certificate in this module. Framework-wise this is the T6 fixed-point algebra reused in cosmology: the same φ that sets the mass ladder and the eight-tick structure supplies the exponent that places $\eta_B$ next to the observed $6.1\times 10^{-10}$. The “44 connection” ties this asymmetry certificate to the electromagnetic coupling through one structural integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.