pos_root_eq_phi
plain-language theorem explainer
Any positive real solving the self-similarity equation r² = r + 1 equals the golden ratio φ. Pattern-forcing and eight-tick ladder arguments cite this to pin the constant step ratio. The proof is elementary real algebra: complete the square to identify √5, then match the closed form of φ.
Claim. If $r \in \mathbb{R}$ satisfies $r > 0$ and $r^2 = r + 1$, then $r = \varphi$, where $\varphi = (1 + \sqrt{5})/2$ is the golden ratio.
background
In Recognition Science the T6 forcing step selects the unique self-similar scale factor of the ledger: the positive root of $x^2 = x + 1$. That root is the golden ratio $\varphi$, written in closed form as $(1 + \sqrt{5})/2$. The same equation appears as the constant step-ratio condition on an eight-tick ladder pattern (unit base, positive ratio, self-similar ratio) consumed by the $w_8$ spectral projection.
This module (Alpha Genesis M2: Pattern Forcing) shows that any such ladder is exactly the geometric sequence $\varphi^t$, and that the conjugate decay envelope $\varphi^{-k}$ is the T9 forced measure. The present lemma is the pure real-analysis kernel of that identification: positivity plus the quadratic forces $r = \varphi$, with no appeal to CODATA or external constants.
Upstream scaffolding supplies only the ambient RS tick and primitive calculus infrastructure; the argument itself is self-contained real arithmetic.
proof idea
From $r^2 = r + 1$, rearrange to $(2r - 1)^2 = 5$ by nlinarith. Nonnegativity of $2r - 1$ is proved by contradiction: if $2r - 1 < 0$, the identity $(2r)(2 - 2r) = 1 - (2r - 1)^2$ together with positivity of both factors would force $0 < 1 - 5$, absurd. Thus $\sqrt{5} = 2r - 1$ by Real.sqrt_sq. Unfold the definitional equality $\varphi = (1 + \sqrt{5})/2$, substitute, and finish by ring.
why it matters
This is the T6 self-similarity pin used throughout Alpha Genesis pattern forcing. Downstream, ratio_eq_phi applies it directly: every EightTickLadder has ratio equal to $\varphi$, which then yields the full pattern-forcing theorem (every eight-tick ladder is the $\varphi$-pattern $\varphi^t$). That discharges discrete choice (ii) of the no-fit proposition: the canonical $\varphi$-pattern is forced by T6 given the T7 eight-tick carrier, rather than chosen.
Together with the reciprocal identity that pattern times forced measure equals 1 tick-by-tick, it closes the ledger J-symmetry link between the growth display $\varphi^t$ and the spectral weight $\varphi^{-k}$. No open scaffolding remains on this lemma; it is a proved, zero-sorry real identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.