IndisputableMonolith.Constants.GapWeight.Formula
Defines the canonical eight-tick φ-power samples and the DFT amplitudes that become geometric gap weights. Anyone working the α-genesis or gap-weight projection chain cites these formulas as the explicit ladder input. The module packages u_t = φ^t on Fin 8, complex DFT coefficients, amplitudes, and nonnegativity of the resulting weights.
claimOn the eight-tick cycle, the canonical pattern is $u_t = \varphi^t$ for $t \in \{0,\ldots,7\}$. The module defines its DFT-8 coefficients $\hat u_k$, amplitudes $|\hat u_k|$, and geometric weights built from those amplitudes (with the spectral $\sin^2(k\pi/8)$ factor supplied by the projection layer).
background
Recognition Science fixes an eight-tick recognition cycle (T7) and the golden ratio $\varphi$ as the self-similar fixed point of the T6 equation $r^2 = r + 1$. The natural ladder samples on that cycle are therefore the geometric sequence $\varphi^t$ at the eight discrete ticks.
The DFT-8 backbone supplies the unitary eigenbasis for the cyclic shift: the primitive root $\omega = e^{-2\pi i/8}$ and the standard eight-point transform. Gap weights are read off as spectral amplitudes of the $\varphi$-pattern in that basis, later multiplied by the discrete-derivative spectrum.
This module sits under Constants and only constructs those samples and amplitudes; forcing that the pattern must be $\varphi^t$, and that the $\sin^2$ factor is the difference-operator spectrum, are proved downstream.
proof idea
Definition module, not a theorem package. It introduces the real and complex $\varphi$-patterns on Fin 8, their DFT-8 coefficients and amplitudes, the geometric weight and the $w_8$ DFT candidate, then records elementary nonnegativity and positivity lemmas for those quantities. No forcing or uniqueness argument lives here.
why it matters in Recognition Science
Supplies the explicit ladder input consumed by the α-genesis and gap-weight stack. PatternForcing cites it as the $\varphi$-pattern $u_t = \varphi^t$ whose uniqueness under unit base, constant step ratio, and the T6 self-similarity equation is the M2 theorem. SpectralForcing and GapWeight.Projection take the same amplitudes and close the historical ambiguity about why geometric weights carry a $\sin^2(k\pi/8)$ factor: that factor is the eigenvalue weight of the one-step difference operator on the eight-tick cycle. Without these formulas the spectral projection has nothing concrete to normalize.
scope and limits
- Does not prove that $u_t = \varphi^t$ is the unique admissible eight-tick ladder pattern.
- Does not derive the $\sin^2(k\pi/8)$ spectral factor; that is Projection/SpectralForcing.
- Does not evaluate or bound the fine-structure constant $\alpha$.
- Does not normalize gap weights into a probability measure; only defines raw amplitudes and candidates.
- Does not address continuous-time or non-octave (non-8) sampling.