pattern_mul_forced_measure
plain-language theorem explainer
At every tick of the eight-tick register, the canonical golden-ratio pattern multiplies the T9 forced lattice measure to one. Anyone citing Alpha Genesis M2 reciprocity (pattern and weight as conjugate displays of one object) needs this identity. The proof is a short algebraic reduction: φ^t times (1/φ)^t cancels to 1 once φ is known nonzero.
Claim. For every tick $t\in\{0,\ldots,7\}$, the product of the canonical golden-ratio pattern $\varphi^{t}$ and the forced lattice weight $w(t)$ equals one: $\varphi^{t}\cdot w(t)=1$.
background
Alpha Genesis M2 forces the discrete φ-pattern consumed by the w₈ spectral projection. Any eight-tick ladder with unit base, constant positive step ratio, and self-similar ratio $r^{2}=r+1$ (the T6 equation) is exactly $\varphi^{t}$. The same module identifies the decay envelope $\varphi^{-k}$ inside the spectral weight with the unique T9 forced measure from Foundation.MeasureForcing.
The w₈ machinery therefore uses two reciprocal φ-displays: the time-domain growth pattern $\varphi^{t}$ and the spectral weight $\varphi^{-k}$. Their product is identically one tick by tick. Module text frames this as the ledger J-symmetry $J(x)=J(1/x)$: cost-side and weight-side displays are conjugates, neither an independent input.
Here phiPattern is the sample $t\mapsto\varphi^{t}$ on Fin 8. latticeWeight is the forced measure on that carrier; the proof unfolds it as $(1/\varphi)^{t}$. Upstream phi_ne_zero supplies the cancellation hypothesis.
proof idea
Term proof by unfolding. Both factors reduce to powers of φ: the goal becomes $\varphi^{t}\cdot(1/\varphi)^{t}=1$. Rewrite $1/\varphi$ as the multiplicative inverse, pull the product inside the power (mul_pow), cancel via mul_inv_cancel₀ using phi_ne_zero, and finish with one_pow. No induction and no spectral analysis.
why it matters
Clause 3 of PatternForcingCert: pattern and forced measure are reciprocal displays. With pattern_forced, phiPattern_is_forced, and the sibling envelope identity geometricWeight = sin²(kπ/8)·latticeWeight, this closes M2 of Alpha Genesis and discharges discrete choice (ii) of the no-fit proposition (the "canonical φ-pattern" is forced, not chosen). The reciprocity is discrete J-symmetry from T5 (J(x)=J(1/x)); the envelope that follows is the unique T9 recognition weight, not an α-specific ansatz. Sits on the T7 eight-tick octave and the forced measure of MeasureForcing. No CODATA enters the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.