Pith. sign in
module module moderate

IndisputableMonolith.Constants.GapWeight.Projection

show as:
view Lean formalization →

Defines the geometric projection that turns the canonical φ-pattern gap weight into an eight-tick DFT energy scale. Introduces tick, vertex, and cell counts for the fundamental octave, the projection scale, the total φ-DFT energy, and the nonnegativity of the projected eight-mode weight. Cited by the spectral-forcing argument that identifies the sin²(kπ/8) factor with the difference-operator spectrum on the cycle. Mostly equalities and nonnegativity lemmas over fixed combinatorial constants.

claimOn the eight-tick recognition cycle fix $N_{\mathrm{ticks}}=8$, together with vertex and cell counts $N_{\mathrm{vertices}}$, $N_{\mathrm{cell}}$. The projection scale converts the canonical $\varphi$-pattern gap weight into a DFT-8 energy $E_{\varphi}^{\mathrm{DFT}}\ge 0$, yielding a projected eight-mode weight $w_8^{\mathrm{proj}}\ge 0$.

background

Recognition Science takes the fundamental time quantum as one tick ($\tau_0=1$) and forces an eight-tick octave (period $2^3$) as the closed recognition cycle. The DFT-8 module supplies the unitary eigenbasis for that cycle, with primitive root $\omega=e^{-2\pi i/8}$.

The GapWeight.Formula layer packages the canonical $\varphi$-pattern: mode weights built from powers of the golden ratio $\varphi$ on the eight-tick ladder. Projection sits between that combinatorial weight and the spectral picture: it records how many ticks, vertices, and cells enter the fundamental cell, then rescales the $\varphi$-pattern into a total DFT energy and a projected eight-mode weight.

Notation is RS-native and dimensionless. Equalities such as $N_{\mathrm{ticks}}=8$ are definitional anchors, not dynamical claims; nonnegativity of the projected energy and weight is the only analytic content needed downstream.

proof idea

Definition module with thin equational and positivity lemmas. Combinatorial counts ($N_{\mathrm{ticks}}$, $N_{\mathrm{vertices}}$, $N_{\mathrm{cell}}$) are closed by rfl or direct numeral equalities. The projection scale and $\varphi$-DFT total energy are abbreviations or one-line unfoldings of the Formula and DFT8 imports. Nonnegativity of phiDFTEnergyTotal and w8_projected follows from nonnegativity of the underlying $\varphi$-weights and squared spectral factors, without a long tactic script.

why it matters in Recognition Science

Feeds Constants.AlphaGenesis.SpectralForcing, whose doc-comment states the theorem: the oscillation factor $\sin^2(k\pi/8)$ inside the gap-weight mode weights is not a modeling choice but one quarter of the spectrum of the one-step difference operator on the eight-tick cycle, read in the DFT-8 eigenbasis.

Without a clean projection scale and a nonnegative projected weight $w_8^{\mathrm{proj}}$, that forcing chain has nothing to evaluate. The module therefore closes the constants side of the link between the canonical $\varphi$-pattern (GapWeight.Formula) and the eight-tick spectral backbone (DFT8), in service of the $\alpha$-genesis program. It sits on the T7 eight-tick octave landmark and prepares the ground for identifying geometric gap weights with derivative spectra.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)