geometricWeight_pos
plain-language theorem explainer
For every nonzero eight-tick mode index k, the geometric weight (sin² of the mode frequency times a negative power of φ) is strictly positive. Gap-weight and DFT-candidate constructions cite this to keep mode sums strictly above zero. The proof unfolds the piecewise definition, drops the zero branch, and factors positivity into a positive sine-square on (0,π) and a positive φ-power.
Claim. Let $k\in\{0,\ldots,7\}$ with $k\neq 0$. Write $\mathrm{freq}=k\pi/8$ and $\phi$ for the golden ratio. Then the geometric weight $\sin^2(\mathrm{freq})\cdot\phi^{-k}$ is strictly positive.
background
The module fixes the canonical φ-pattern on the eight-tick circle (the T7 octave). Modes are indexed by Fin 8. The geometric weight of mode $k$ is defined piecewise: it is $0$ at the DC mode $k=0$, and otherwise the product of an oscillatory factor $\sin^2(k\pi/8)$ with a φ-decay $\phi^{-k}$.
That product is the real amplitude used when assembling DFT-style gap weights from the φ-pattern. Sibling facts already record nonnegativity of the amplitude and of the geometric weight; the present lemma upgrades the nonzero-mode case to strict positivity.
The eight-tick setting is the discrete period $2^3$ forced in the Recognition chain; φ is the self-similar fixed point from T6. The frequency $k\pi/8$ places every nonzero residue strictly inside $(0,\pi)$, so the sine factor cannot vanish.
proof idea
Unfold the geometric-weight definition and simplify with $k\neq 0$ to discard the zero branch, leaving $\sin^2(k\pi/8)\cdot\phi^{-k}$.
Apply product positivity. The square is positive once $\sin(k\pi/8)>0$, which follows from $\mathrm{Real.sin_pos_of_pos_of_lt_pi}$: the argument is positive because $k\ge 1$, and strictly less than $\pi$ because $k\le 7$ forces $k\pi/8\le 7\pi/8<\pi$ (via nlinarith and $\pi>0$).
The second factor is positive by zpow_pos from $\phi>0$.
why it matters
Strict positivity of nonzero-mode geometric weights is the local positivity engine for the DFT-based candidate weight. Downstream, w8_dft_candidate_pos sums positive contributions over the filtered nonzero modes and needs each summand nonnegative with at least one strictly positive; this lemma supplies the strict half.
In the Recognition constants layer, gap weights sit on the eight-tick octave (T7) with φ-ladder decay (T6). Keeping every neutral mode weight positive prevents accidental cancellation to zero when the candidate is later compared against gauge-volume or quotient weights elsewhere in the SevenGaps stack.
The lemma is fully proved (no sorry). It does not itself identify the physical gap spectrum; it only certifies that the geometric building block used by the DFT candidate is a positive real on the nonzero residue classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.