DFTMode
DFTMode enumerates the eight discrete Fourier transform modes via an inductive type with constructors m0 to m7. Cross-domain universality arguments in Recognition Science cite it to instantiate the 2³ count for harmonic decomposition. The definition is a direct inductive enumeration that derives DecidableEq, Repr, BEq and Fintype to guarantee cardinality 8.
claimThe type DFTMode is the inductive type generated by eight constructors m0,…,m7 and equipped with instances of decidable equality, representation, boolean equality and finite type structure.
background
The CrossDomain.TwoCubeUniversality module establishes that the count 8=2³ appears as the maximal-periodic structure for spatial dimension D=3 across RS domains. HasTwoCubeCount asserts that a finite type T satisfies Fintype.card T = 2^3. DFTMode supplies the DFT-8 modes instance for fundamental harmonic decomposition. The upstream abbrev DFTMode : Type := Fin 8 from DFTHarmonicSpectrum supplies the mode index used in frequency definitions.
proof idea
This is a direct inductive definition declaring eight constructors m0 through m7 and deriving the Fintype instance. No lemmas are invoked; the structure itself encodes the required cardinality.
why it matters in Recognition Science
The declaration supplies the DFT-8 modes entry in the C14 2³=8 universality list. It is referenced by DFTHarmonicSpectrumCert (modes_eight field) and by dft_has_2cube. It connects the DFT domain to the eight-tick octave and the D=3 recognition cube count.
scope and limits
- Does not prove HasTwoCubeCount for Q3 vertices or Pauli elements.
- Does not derive any harmonic frequency formulas or carrier bounds.
- Does not establish equivalence between this inductive type and the Fin 8 abbreviation.
formal statement (Lean)
32inductive DFTMode where
33 | m0 | m1 | m2 | m3 | m4 | m5 | m6 | m7
34 deriving DecidableEq, Repr, BEq, Fintype
35