geometricWeight_eq_sin_mul_forced_measure
plain-language theorem explainer
For every nonzero eight-tick mode k, the geometric gap weight equals sin²(kπ/8) times the T9 forced lattice measure. Anyone deriving α from the w₈ spectral projection cites this envelope identity. The φ^{-k} decay inside the weight is not an α-specific choice; it is the unique forced recognition measure. The proof unfolds the geometric-weight definition and matches the decay factor to the reciprocal lattice weight by elementary power algebra.
Claim. For every mode $k \in \{1,\ldots,7\}$ on the eight-tick carrier, the geometric gap weight equals $\sin^2(k\pi/8)$ times the forced lattice measure at $k$: $w_{\mathrm{geom}}(k) = \sin^2(k\pi/8)\,\mu_{\mathrm{lat}}(k)$.
background
Alpha Genesis M2 (Pattern Forcing) shows that the φ-pattern consumed by the w₈ spectral projection is forced, not chosen. Any eight-tick ladder with unit base, constant positive step ratio, and self-similar ratio $r^2 = r + 1$ (the T6 equation on the T7 carrier) is exactly $\varphi^t$. The conjugate decay envelope $\varphi^{-k}$ inside the spectral weight is the unique T9 forced measure from Foundation.MeasureForcing.
Geometric weight on a nonzero mode is defined as $\sin^2(k\pi/8)\cdot\varphi^{-k}$. Lattice weight is that forced measure, term for term. The module's reciprocity structure records that the time-domain pattern $\varphi^t$ and the spectral envelope $\varphi^{-k}$ are reciprocal displays of one object (pattern · forcedMeasure = 1 tick by tick), reflecting the ledger J-symmetry $J(x)=J(1/x)$. Neither display is an independent input. Status target: theorem, zero sorry, no CODATA.
proof idea
Term proof. Unfold geometricWeight and kill the zero-mode branch with the hypothesis $k\neq 0$, leaving $\sin^2(k\pi/8)\cdot\varphi^{-k}$ on the left-hand side. The goal is then equality of the two decay factors $\varphi^{-(k:\mathbb{Z})}$ and $(1/\varphi)^k$ after the common $\sin^2$ factor. One congr 1 isolates that factor; zpow_neg, zpow_natCast, one_div, and inv_pow identify the integer negative power of $\varphi$ with the natural power of its reciprocal. No external lemmas beyond the definition and these power rewrites.
why it matters
This is the envelope identity of M2: the $\varphi^{-k}$ inside $w_8$ is the unique T9 recognition weight, not an α-specific fit. It is clause 4 of PatternForcingCert ("the spectral decay envelope is the forced measure") and clause 3 of the top-level AlphaGenesisCert ("the spectral envelope is the forced measure (M2)"). The spectral-forcing sibling geometricWeight_eq_spectrum_mul_measure rewrites through this identity, then replaces $\sin^2$ by the difference-operator spectrum over 4, so both factors of the mode weight become theorems. Together with pattern forcing (T6 on the T7 eight-tick octave) and pattern–measure reciprocity, it removes discrete choice (ii) from the no-fit proposition in the fine-structure derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.