goldenScalar_forces_phi
plain-language theorem explainer
Any positive real λ with λ² = λ + 1 equals the RS golden ratio φ. Cited wherever a golden-operator eigenvalue or characteristic root must be identified with φ rather than left algebraic. The proof excludes λ = 1, rewrites the equation as the ledger-closure identity 1 + λ = λ², and hands off to the complete phi-forcing theorem.
Claim. If $\lambda \in \mathbb{R}$ satisfies $\lambda > 0$ and $\lambda^2 = \lambda + 1$, then $\lambda = \varphi$, where $\varphi$ is the Recognition Science golden ratio (the unique positive self-similar fixed point of the scale ladder).
background
This module is the algebraic core of the paper on golden and metallic structures on Hessian manifolds. From a normalized projector $P$ one builds the almost-product operator $F = 2P - I$ (with $F^2 = I$) and the golden operator $G = \varphi P + (1-\varphi)(I-P)$, which is required to satisfy $G^2 = G + I$. The scalar characteristic equation of that operator is exactly $\lambda^2 = \lambda + 1$.
The Recognition Science constant $\varphi$ is forced earlier in the stack as the unique positive ratio of a geometric scale sequence closed under additive ledger composition. The complete forcing theorem states: for $r > 0$, $r \neq 1$, the closure identity $1 + r = r^2$ implies $r = \varphi$. That is the T6 landmark (phi forced as the self-similar fixed point).
Here the only extra work is to match the golden-operator equation to that closure hypothesis and rule out the degenerate root $r = 1$.
proof idea
Tactic proof in three short steps. First, $\lambda \neq 1$: substituting $\lambda = 1$ into $\lambda^2 = \lambda + 1$ yields $1 = 2$, contradiction by norm_num. Second, rearrange by linarith to the closure form $1 + \lambda = \lambda^2$. Third, apply PhiForcingDerived.phi_forcing_complete with the positivity hypothesis, the inequality $\lambda \neq 1$, and the rearranged closure identity. No further algebraic work; the uniqueness of $\varphi$ is entirely upstream.
why it matters
Closes the scalar identification step in the projector-to-golden package. Downstream, projector_golden_certificate packages the almost-product and golden-operator square identities together with the normalized-projector facts; this theorem supplies the reason the golden eigenvalue is literally $\varphi$, not an unnamed metallic root.
It is re-exported as JHessianGoldenMulti.goldenScalar_forces_phi and feeds jHessianGoldenMultiCertificate, which discharges the golden-structure $\varphi$-forcing hypotheses for the multi-coordinate RS J-Hessian in arbitrary dimension. In the forcing chain this is the concrete algebraic link from the cost-induced projector geometry back to T6 (phi uniqueness). Status is fully proved: zero sorry, zero new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.