Pith. sign in
module module moderate

IndisputableMonolith.Constants.GapWeight.Projection

show as:
view Lean formalization →

Defines the discrete projection data that turns the canonical φ-pattern gap weights into eight-tick mode weights: tick/vertex/cell counts, a projection scale, total φ-DFT energy, and the nonnegativity of the projected weights w₈. Cited by anyone deriving the spectral factor in α-genesis. Mostly equalities and nonnegativity lemmas over the DFT-8 backbone.

claimOn the eight-tick octave fix $N_{\mathrm{ticks}}=8$ (and companion vertex/cell counts). Define a projection scale, the total $\varphi$-DFT energy $E_{\varphi}^{\mathrm{DFT}}\ge 0$, and projected mode weights $w_8$ obtained by projecting the canonical $\varphi$-pattern gap-weight formula onto the DFT-8 basis, with $w_8\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 recognition cycle. The DFT-8 module supplies the canonical unitary basis for that cycle: the primitive eighth root $\omega=e^{-2\pi i/8}$ and the associated 8-point transform.

Upstream, GapWeight.Formula packages the canonical $\varphi$-pattern whose mode content must be read in that basis. This Projection module sits between those two layers: it records the discrete geometry of the octave (ticks, vertices, cells), a projection scale that normalizes the map from the $\varphi$-pattern into DFT space, and the total $\varphi$-DFT energy against which projected weights are measured.

The local objects are therefore bookkeeping constants plus the projected weight vector $w_8$, not a new dynamical law.

proof idea

Definition module with short equality and nonnegativity lemmas. Counts such as $N_{\mathrm{ticks}}$ are closed by rfl-style equations to the octave size 8. projectionScale and phiDFTEnergyTotal are defined from the Formula and DFT-8 imports; nonnegativity of total energy and of $w_8$ follows from nonnegativity built into the $\varphi$-pattern and the unitary DFT-8 energy identity. No deep tactic proof lives here; the module assembles the projected data SpectralForcing will interpret.

why it matters in Recognition Science

Feeds Constants.AlphaGenesis.SpectralForcing, whose doc-comment states the target 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 on the DFT-8 eigenbasis.

Without projected weights and the projection scale, that spectral identification has nothing concrete to act on. In the broader chain this is the constants-side hinge between the canonical $\varphi$-pattern (GapWeight.Formula), the eight-tick octave (T7), and the α-genesis forcing argument that pins the fine-structure sector. It does not itself prove the sin² identification; it supplies the projected $w_8$ data that argument consumes.

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)