Pith. sign in
module module high

IndisputableMonolith.Constants.AlphaGenesis.SpectralForcing

show as:
view Lean formalization →

Closes the trigonometric identity behind eight-tick spectral weights: the squared modulus of each cyclic-shift eigenvalue minus one equals four times the squared half-angle sine. Anyone deriving the geometric gap weights or the fine-structure seed from the w₈ projection cites this. The argument is elementary complex arithmetic on eighth roots of unity, then factorization into the spectral times measure form of the geometric weight.

claimFor the primitive eighth root of unity $\omega_8 = e^{2\pi i/8}$ and mode index $k$, $|\omega_8^k - 1|^2 = 4\sin^2(k\pi/8)$. The eight-tick difference energy of mode $k$ equals that quantity. The geometric weight on the ladder factors as this spectral factor times the T9 measure weight.

background

Alpha Genesis derives the fine-structure constant forward from Recognition structure rather than fitting a display formula. The eight-tick octave (T7) makes the cyclic shift on period $2^3$ the natural discrete time operator. Its eigenvalues are the powers $\omega_8^k$.

GapWeight.Projection already states the design intent: geometric weights carry a $\sin^2(\pi k/8)$ factor because that is the spectral weight of the discrete derivative (Laplacian) on the 8-tick cycle, forced by shift-diagonalization in DFT language. PatternForcing supplies the companion fact that the ladder pattern consumed by the $w_8$ projection is exactly $\varphi^t$, and that the decay envelope $\varphi^{-k}$ is the T9 forced measure term by term.

This module supplies the missing trig identity that turns the complex eigenvalue gap into the real $\sin^2$ weight used in those formulas.

proof idea

The core identity is proved by writing $\omega_8^k = e^{i k \pi/4}$, expanding $|z-1|^2 = (z-1)(\bar z-1)$ on the unit circle, and reducing to $2-2\cos\theta = 4\sin^2(\theta/2)$ with $\theta = k\pi/4$. A companion lemma equates the eight-tick difference-energy of mode $k$ to the same $4\sin^2(k\pi/8)$ expression. The geometric-weight equality then multiplies that spectral factor by the T9 measure weight, matching the canonical gap-weight formula. A certificate aggregates the equalities for downstream import.

why it matters in Recognition Science

Without the trig closure, the $\sin^2(\pi k/8)$ factor in the geometric weights would remain an ansatz. This module discharges that step so AlphaGenesis can assemble $\alpha^{-1}$ from seed times continuum weight on $w_8$ without an ad hoc spectral kernel.

It sits between GapWeight.Projection (which names the spectral origin of the sine factor) and the AlphaGenesis aggregator (forward $\alpha$ derivation, mirror of the mass program). Upstream PatternForcing and MeasureForcing (T9) fix the $\varphi$-ladder and the measure envelope; this module only closes the eigenvalue-to-sine bridge on the eight-tick circle. Framework landmarks in play: T6 ($\varphi$), T7 (eight-tick octave), and T9 (forced measure).

scope and limits

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (4)