geometricWeight_nonneg
plain-language theorem explainer
Each of the eight DFT mode geometric weights is nonnegative. Anyone proving positivity of the DFT-based gap-weight candidate cites this. The proof unfolds the piecewise definition: the zero mode is identically zero, and every other mode is a product of a squared sine and a nonnegative integer power of φ.
Claim. For every mode index $k \in \{0,\ldots,7\}$, the geometric weight attached to $k$ is nonnegative: $0 \le w^{\mathrm{geom}}(k)$. Explicitly, $w^{\mathrm{geom}}(0)=0$ and for $k\neq 0$ one has $w^{\mathrm{geom}}(k)=\sin^2(k\pi/8)\,\varphi^{-k}\ge 0$.
background
The module fixes the canonical φ-pattern on the eight-tick register. Modes are indexed by Fin 8, matching the T7 octave (period $2^3$). The geometric weight of mode $k$ is defined piecewise: it is zero on the DC mode $k=0$, and otherwise the product of an oscillatory factor $\sin^2(k\pi/8)$ with a φ-decay $\varphi^{-k}$.
Here $\varphi$ is the golden ratio forced as the self-similar fixed point (T6), known positive. Squared sines are nonnegative on $\mathbb{R}$, and integer powers of a positive base remain nonnegative. The construction sits inside the Constants/GapWeight layer that builds DFT-side candidates for the mass-gap weight from this φ-pattern.
proof idea
Unfold the piecewise definition and case-split on whether the mode index is zero. On the zero branch the claim is $0\le 0$, discharged by reflexivity of $\le$. On the nonzero branch the weight is a product; apply nonnegativity of multiplication, then nonnegativity of squares for the sine factor and nonnegativity of integer powers of a nonnegative base (using $\varphi>0$) for the decay factor.
why it matters
This is the nonnegativity half of the geometric-weight calculus on the eight-tick DFT. Downstream, w8_dft_candidate_pos sums filtered mode contributions and needs each summand nonnegative (via mul_nonneg on this lemma) before concluding the DFT candidate weight is strictly positive. That candidate is the Constants-layer stand-in for a gap weight built from the canonical φ-pattern, tying T6 (φ) and T7 (eight-tick octave) into the mass-gap bookkeeping. Without nonnegativity, the Finset positivity argument for the candidate cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.