phiPattern_is_forced
plain-language theorem explainer
On any admissible eight-tick ladder, the GapWeight φ-pattern at tick t equals the ladder value at that index. Citers of the Alpha Genesis M2 pattern-forcing certificate need this: the spectral machinery's canonical pattern is the forced ladder on Fin 8, not an extra choice. Proof is a one-line rewrite through global pattern forcing, then reflexivity.
Claim. For every eight-tick ladder $L$ (unit base, constant positive step ratio $r$ with $r^2=r+1$) and every tick $t\in\{0,\ldots,7\}$, the canonical GapWeight pattern equals the ladder value: $\varphi^{t}=u_L(t)$.
background
Alpha Genesis M2 shows the φ-pattern consumed by the $w_8$ spectral projection is forced, not chosen. An eight-tick ladder is a sequence $u:\mathbb{N}\to\mathbb{R}$ with unit base $u(0)=1$, constant positive step ratio $r$, and self-similarity $r^2=r+1$ (the T6 equation). The carrier is the T7 eight-tick window, sampled at $\mathrm{Fin},8$.
Upstream, pattern_forced proves every such ladder equals $\varphi^n$ at every $n$, by induction from the base and the ratio identification with $\varphi$. GapWeight defines the canonical pattern as $\varphi^{t}$ on $\mathrm{Fin},8$. The module's reciprocity pairs this growth display with the T9 forced measure (decay $\varphi^{-k}$), conjugate under $J$-symmetry.
proof idea
One-line term proof. Rewrite via pattern_forced on $L$, which yields $u_L(n)=\varphi^n$ for all $n$, so $u_L(t)=\varphi^{t}$. That is definitionally the GapWeight pattern at $t$, and reflexivity closes.
why it matters
Feeds PatternForcingCert, the M2 closure: clause 2 asserts the GapWeight pattern is exactly the forced ladder on $\mathrm{Fin},8$. With global pattern forcing, pattern-measure reciprocity, and the spectral-envelope identification, this discharges discrete choice (ii) of the no-fit proposition: the "canonical φ-pattern" is forced by T6 self-similarity on the T7 carrier, not fitted. Ties forcing-chain landmarks T6 ($\varphi$ as self-similar fixed point) and T7 (eight-tick octave). Status is pure theorem; no CODATA.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.