geometricWeight
plain-language theorem explainer
For each eight-tick Fourier mode k, the geometric weight vanishes at the DC mode and otherwise equals sin²(kπ/8)·φ^{-k}. Anyone reconstructing α from the eight-tick spectral envelope cites this as the mode-wise building block of the gap-weight decomposition. The body is a direct closed-form product of the oscillation factor and the φ-decay envelope; no lemmas are required.
Claim. For each mode $k \in \{0,\ldots,7\}$, define the geometric weight by $w(k)=0$ if $k=0$, and $w(k)=\sin^2(k\pi/8)\,\varphi^{-k}$ otherwise.
background
The module develops the canonical φ-pattern on the eight-tick register. Modes are indexed by Fin 8, matching the T7 eight-tick octave (period $2^3$). The constant φ is the self-similar fixed point forced at T6 of the unified forcing chain.
The geometric weight packages two factors that later theorems identify independently: the squared-sine oscillation $\sin^2(k\pi/8)$, which equals one quarter of the difference-operator spectrum of DFT mode $k$, and the decay $\varphi^{-k}$, which pattern-forcing identifies with the T9 forced lattice measure. Upstream, the certified scalar gap weight $w_8$ is the normalized projection of the gap onto the fundamental 8-tick basis (closed form involving $\sqrt{2}$ and φ, numerically $\approx 2.49057\ldots$). Mode weights of the present form feed the spectral reconstruction used by the α pipeline.
proof idea
Plain definition by cases on the mode index. The zero mode is set to $0$. For nonzero $k$ one forms the frequency $k\pi/8$, takes the squared sine as the oscillation factor, multiplies by $\varphi$ raised to the integer power $-k$, and returns the product. No upstream lemmas are applied; the body is a closed expression in Real.sin and the global constant φ.
why it matters
This is the mode-wise object that the Alpha Genesis spectral and pattern certificates factor. Downstream, the envelope identity proves the decay factor is exactly the forced lattice measure, and the spectral-forcing theorem rewrites the oscillation as $\mathrm{diffEnergy}_8(\mathrm{mode},k)/4$. Both feed PatternForcingCert and SpectralForcingCert, which bundle into AlphaGenesisCert for the forward derivation of α (channel budget $4\pi\cdot 11$, forced φ-ladder, forced spectral measure, dressing $e^{-\varepsilon}$).
The eight-tick structure (T7) and φ (T6) appear explicitly; the construction sits in the constants domain targeting the $\alpha^{-1}$ band near 137. A nearby DFT candidate for the scalar $w_8$ is explicitly not yet proven equal to the certified eight-tick projection; the present definition supplies the spectral factors used in the forcing identities rather than that closed scalar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.