module module high

`IndisputableMonolith.Spectral.DFT8`

Defines the 8-point DFT toolkit for the Recognition eight-tick cycle: the primitive root ω = e^{-πi/4}, DFT-8 matrix entries, cyclic shift, and elementary power/modulus identities. Downstream spectral weights, complex-structure forcing, Clifford/Bott bridge, and the Schrödinger derivation all import it. Structure is definitional plus short algebraic lemmas on powers of ω.

claimModule objects: the primitive eighth root $\omega_8 = e^{-2\pi i/8} = e^{-\pi i/4}$; DFT-8 entries $F_{jk} \propto \omega_8^{jk}$; the cyclic shift $T$ on $\mathbb{C}^8$ and its matrix; identities $\omega_8^8 = 1$, $\omega_8^4 = -1$, $|\omega_8| = 1$, and non-triviality $\omega_8^k \neq 1$ for $0 < k < 8$.

background

Recognition Science forces an eight-tick recognition period (T7): with spatial dimension $D = 3$ the minimal closed ledger cycle has length $2^D = 8$. Ledger states on one octave are therefore 8-component signals; the discrete time step is the cyclic shift operator $T$ on that octuple.

Spectral analysis of $T$ is the length-8 discrete Fourier transform. The primitive root $\omega_8 = e^{-2\pi i/8}$ is the eigenvalue generator: $T$ is diagonalized by the DFT-8 matrix with entries built from powers of $\omega_8$. Downstream gap-weight work identifies the Laplacian/derivative weights on this cycle with factors $\sin^2(\pi k/8)$ coming from those eigenvalues.

The module sits in the Spectral domain and imports only Mathlib; it supplies the concrete complex arithmetic that later foundation modules treat as the forced 8-tick signal space.

proof idea

Definition-first module, not a single theorem. It introduces omega8 as $e^{-\pi i/4}$, records omega8_pow_8, omega8_pow_4, and omega8_abs, then builds dft8_entry / dft8_matrix / dft8_mode and the cyclic_shift / shift_matrix pair. Remaining lemmas are short power and symmetry identities; one non-degeneracy fact appears as an explicit axiom (omega8_pow_ne_one_axiom) rather than a derived Mathlib closed form. No deep analytic argument: pure finite cyclic-group arithmetic on the eighth roots.

why it matters in Recognition Science

This is the concrete spectral substrate for T7. GapWeight.Projection imports it to justify the $\sin^2(\pi k/8)$ factor as the eigenvalue weight of the discrete derivative on the 8-tick shift ("forced by shift-diagonalization"). ComplexStructureForcing uses the same shift: $T$ is not diagonalizable over $\mathbb{R}$, so complexification is algebraically forced. CliffordBridge ties the 8-tick package to Bott periodicity $\mathrm{Cl}_{n+8}\cong\mathrm{Cl}_n\otimes\mathrm{Cl}_8$. SchrodingerDerivation starts from T7 → Signal8 and needs this DFT/shift language to reach $i\hbar\partial_t\psi=\hat H\psi$. GapWeight.Formula (canonical $\varphi$-pattern) also depends on the module. Without a pinned DFT-8, the octave spectral weights and the complex structure step remain informal.

scope and limits

Does not derive T7 or $D=3$; assumes the eight-tick period as given.
Does not prove the Schrödinger equation or Bott periodicity; only supplies DFT-8 primitives.
Does not fix normalization conventions for gap weights beyond matrix/entry definitions.
Does not claim uniqueness of $\omega_8$ orientation beyond the stated primitive root.
Non-degeneracy of intermediate powers may rest on an explicit axiom, not a closed Mathlib proof.

used by (5)

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

IndisputableMonolith.Constants.GapWeight.Formula module_import
IndisputableMonolith.Constants.GapWeight.Projection module_import
IndisputableMonolith.Foundation.CliffordBridge module_import
IndisputableMonolith.Foundation.ComplexStructureForcing module_import
IndisputableMonolith.Foundation.SchrodingerDerivation module_import

declarations in this module (46)

def omega8 L41
theorem omega8_pow_8 L44
theorem omega8_pow_4 L53
theorem omega8_abs L62
def dft8_entry L72
lemma dft8_entry_sym L76
def dft8_matrix L82
def dft8_mode L86
def cyclic_shift L90
def shift_matrix L94
theorem omega8_pow_ne_one L102
theorem omega8_pow_ne_one_axiom L143
lemma star_omega8 L149
lemma star_omega8_pow L161
lemma omega8_mul_inv L165
lemma star_omega8_mul_self L170
lemma star_omega8_pow_mul_self L176
lemma omega8_inv_eq_pow7 L180
lemma star_omega8_pow_mul_pow L193
lemma sum_star_omega8_pow_prod L200
theorem roots_of_unity_sum L211
lemma roots_of_unity_sum_zero L242
lemma star_dft8_entry_mul L247
lemma star_omega8_pow_mul_same L258
theorem dft8_column_orthonormal L267
theorem dft8_unitary L339
theorem dft8_row_orthonormal L349
def shift_eigenvalue L363
lemma mod8_mul_eq L366
theorem dft8_shift_eigenvector L385
lemma shift_mul_dft8_entry L396
lemma conjTranspose_shift_mul L424
theorem dft8_diagonalizes_shift L444
lemma dft8_mode_zero_constant L457
lemma dft8_mode_neutral L464
def dft_coefficients L485
lemma dft_coeff_zero L489
lemma dft_coeff_zero_of_neutral L506
lemma inverse_dft_expansion L513
theorem dft8_neutral_subspace L541
def dft8_neutral_subspace_hypothesis L570
theorem dft8_neutral_subspace_hypothesis_holds L576
def dft8_unique_up_to_phase_hypothesis L592
structure EightTickBasis L607
def standardDFT8Basis L620
def standardDFT8Basis_canonical_hypothesis L630