DFTMode
plain-language theorem explainer
The eight-mode inductive type for discrete Fourier transform supplies the cardinality-eight structure required by the cross-domain universality argument. Researchers on harmonic spectra in Recognition Science cite this to confirm the 2³ count for the DFT domain. The definition enumerates eight constructors and automatically derives the finite type instance.
Claim. Let $M$ be the type inductively generated by eight constructors $m_0$ to $m_7$, equipped with instances of decidable equality, representation, boolean equality, and finite type.
background
The module collects domains realizing 2³-structure, where HasTwoCubeCount $T$ means Fintype.card $T$ equals 8. The local setting is the structural claim that the count 8 equals 2³ equals |F₂³| appears as the maximal-periodic structure for spatial dimension D=3 across RS domains, with DFT-8 modes listed as one instance. Upstream, the harmonic spectrum module defines the mode index as the abbreviation Fin 8, whose cardinality equals 8 by direct decision.
proof idea
The declaration is the inductive definition that introduces the eight constructors together with the derived typeclass instances for decidable equality, representation, boolean equality and finite type. No lemmas are invoked; the inductive structure itself yields the Fintype instance of cardinality 8.
why it matters
This supplies the mode type used by DFTHarmonicSpectrumCert to certify spectrum properties including the eight-mode count and by dftMode_count to record the cardinality. It fills the DFT instance among the canonical 2³ domains in the module documentation. The construction supports the framework landmark of the eight-tick octave and D=3 yielding the recognition cube count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.