ratio_eq_phi
plain-language theorem explainer
Any eight-tick ladder has constant step ratio equal to φ. Cited when discharging the discrete choice of the canonical φ-pattern on the T7 carrier. The proof is a one-line application of uniqueness of the positive root of the T6 self-similarity equation.
Claim. Let $L$ be an eight-tick ladder: a sequence with unit base, constant positive step ratio $r$, and self-similarity $r^2=r+1$. Then $r=\varphi$, where $\varphi$ is the golden ratio.
background
An eight-tick ladder is a real sequence $u:\mathbb{N}\to\mathbb{R}$ with unit base $u_0=1$, a single positive constant step ratio $r$, the recurrence $u_{n+1}=r,u_n$, and the T6 self-similarity constraint $r^2=r+1$. The carrier is the T7 eight-tick window (indexed by $\mathbb{N}$, consumed at $\mathrm{Fin},8$).
The module Alpha Genesis M2 (Pattern Forcing) shows that the time-domain pattern $u_t=\varphi^t$ used by the $w_8$ spectral projection is not a free choice: any such ladder is exactly the $\varphi$-pattern, and its conjugate decay envelope is the T9 forced measure.
Upstream, pos_root_eq_phi states that the unique positive root of $x^2=x+1$ is $\varphi$ (the T6 forcing equation, self-contained).
proof idea
One-line term proof. Apply pos_root_eq_phi to the ladder fields ratio_pos ($0<r$) and self_similar ($r^2=r+1$). That lemma already identifies the unique positive root of the T6 equation with $\varphi$, so the ladder ratio is forced.
why it matters
Feeds pattern_forced, which concludes by induction that every ladder value equals $\varphi^n$. Together they discharge discrete choice (ii) of the no-fit proposition: the canonical $\varphi$-pattern is forced by T6 self-similarity on the T7 eight-tick carrier, not chosen. The module then pairs this growth display with the reciprocal spectral envelope $\varphi^{-k}$ (the T9 forced measure), so pattern and weight are conjugate under J-symmetry rather than independent inputs. Landmark links: T6 ($\varphi$ as self-similar fixed point) and T7 (eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.