w8_projected
plain-language theorem explainer
The projected eight-tick gap weight is the φ-pattern DFT energy fraction scaled by the fundamental cell cardinality, turning a dimensionless spectral ratio into a per-cell integrated weight. Anyone citing the explicit normalization of the gap weight (versus the historically implicit form) uses this constant. The body is a one-line product of the cell scale with the ratio of weighted neutral DFT energy to total φ DFT energy.
Claim. Define the projected eight-tick weight by $w_8^{\mathrm{proj}} = N_{\mathrm{cell}}\cdot(E_{\mathrm{weighted}}/E_{\mathrm{total}})$, where $N_{\mathrm{cell}}$ is the cardinality of the fundamental RS interface cell, $E_{\mathrm{weighted}}$ is the sum over nonzero modes of $\phi$-DFT amplitude times geometric weight, and $E_{\mathrm{total}}$ is the total $\phi$-DFT energy (Parseval denominator).
background
The GapWeight.Projection module closes a historical ambiguity in the Recognition Science gap-weight construction by making two choices explicit: the spectral factor $\sin^2(\pi k/8)$, forced as the eigenvalue weight of the discrete derivative (Laplacian) on the 8-tick cyclic shift, and the normalization $64=8\times 8$, the cardinality of the fundamental interface cell (eight ticks of the octave clock times eight vertices of the $Q_3$ cell).
Upstream, the DFT candidate weight sums, over nonzero modes $k$, the product of the $\phi$-pattern DFT amplitude and that geometric weight; the module notes this candidate is not yet identified with the certified eight-tick weight used by the $\alpha$ pipeline. The total DFT energy is the sum of $\phi$-DFT amplitudes over all eight modes and serves as the Parseval denominator. The projection scale is simply $N_{\mathrm{cell}}$.
The present definition packages those pieces into one real: scale times (weighted energy over total energy), so operator and measure choices are no longer hidden degrees of freedom.
proof idea
Definitional, not a proved statement. The body multiplies the projection scale $N_{\mathrm{cell}}$ by the ratio of the DFT candidate weight to the total $\phi$-DFT energy. No tactics or lemmas are applied; the expression is the definition.
why it matters
This constant is the explicit projected eight-tick weight that the Projection module introduces to remove hidden normalization freedom. Downstream, nonnegativity follows at once from nonnegativity of the scale, the candidate numerator, and the total-energy denominator (with a zero-energy edge case that collapses the ratio to zero). It is the object compared in the projection-equality closure that aims to match this construction against the certified gap weight feeding the $\alpha$ pipeline.
In the broader framework it sits under the eight-tick octave (T7 forcing) and the constants layer that supplies the gap factor on the $\phi$-ladder mass formula. By fixing the cell measure $N_{\mathrm{cell}}=64$ and the spectral weights in the open, it is claim hygiene rather than new physics: the same numerical weight, now with an auditable operator and measure story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.