w8_projected_nonneg
plain-language theorem explainer
The DFT-normalized eight-tick projection weight is nonnegative. Anyone using the explicit projection-scale form of the gap weight (rather than the closed algebraic constant) cites this bound. The proof unfolds the ratio definition, records nonnegativity of scale, numerator, and Parseval energy, then splits on whether the energy vanishes.
Claim. Let $w_8^{\mathrm{proj}}$ be the projected eight-tick gap weight, defined as the product of the cell projection scale with the ratio of the DFT candidate weight to the total $\varphi$-pattern DFT energy. Then $0 \le w_8^{\mathrm{proj}}$.
background
This module closes an ambiguity in the gap-weight story: it makes explicit both the spectral factor $\sin^2(\pi k/8)$ (eigenvalue weight of the discrete one-step difference on the 8-tick cycle) and the normalization by $64=8\times 8$ (eight ticks times the eight vertices of the $Q_3$ cell). The result is a scale-invariant fraction converted into a per-cell integrated weight.
The projected weight is built from three pieces already in scope. The DFT candidate $w_8^{\mathrm{dft}}$ sums, over nonzero modes $k\in\mathrm{Fin},8$, the product of $\varphi$-DFT amplitudes with geometric weights; it is known strictly positive. The Parseval denominator is the total $\varphi$-DFT energy $\sum_k$ amplitude. The projection scale is the nonnegative $8\times 8$ cell factor. Upstream, the certified pipeline constant $w_8$ is the closed form $(348+210\sqrt{2}-(204+130\sqrt{2})\varphi)/7\approx 2.49057$, not yet identified with this projection operator inside Lean.
proof idea
Unfold the definition of the projected weight (scale times candidate over total energy). Record three nonnegativity facts: the projection scale by simplification of its definition; the DFT candidate by le_of_lt on the existing positivity theorem; the total energy by the dedicated nonnegativity lemma.
Case-split on whether the total energy is zero. If it is, the ratio collapses and the whole expression is zero (hence nonnegative) by simplification with the nonnegative numerator and scale. If not, the energy is strictly positive, so div_nonneg gives a nonnegative ratio, and mul_nonneg with the scale finishes.
why it matters
In Recognition Science the eight-tick octave (forcing step T7) supplies the fundamental evolution period; gap weights on that clock enter the $\alpha$ and mass pipelines. Historically the projection measure and the $64$-normalization were implicit. This lemma is claim hygiene: once the operator is written as an explicit normalized DFT projection, its nonnegativity is immediate and machine-checked.
No downstream theorems currently depend on it (used_by is empty). The module note flags the real open step: proving the projected operator equals the certified closed form w8_from_eight_tick. That equality is a tractable algebraic/trigonometric reduction, tracked as follow-up. Until then, this bound certifies that the definition-level closure is at least a legitimate nonnegative weight, consistent with the positive closed-form constant used by the $\alpha$ pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.