dft_has_2cube
plain-language theorem explainer
The finite set of DFT modes has cardinality exactly 8. Cross-domain universality arguments cite this to equate the harmonic decomposition with the recognition cube Q3 and the Pauli group. The proof is a one-line wrapper that unfolds the cardinality predicate and invokes the decide tactic on the derived Fintype instance.
Claim. The finite set of DFT modes has cardinality $2^3$.
background
Module C14 collects instances of the count 8 = 2³ across RS domains as the maximal-periodic structure for spatial dimension D = 3. HasTwoCubeCount T is the proposition that a finite type T satisfies Fintype.card T = 2^3. DFTMode is the inductive type with eight constructors m0 through m7, each a distinct harmonic mode index. Upstream, the same name appears as an abbreviation for Fin 8 in the DFTHarmonicSpectrum module, confirming the count aligns with the eight-tick period.
proof idea
The proof is a one-line wrapper. It unfolds HasTwoCubeCount to the equality Fintype.card DFTMode = 2 ^ 3. The decide tactic then resolves the statement using the Fintype instance derived from the inductive definition.
why it matters
This theorem supplies the DFT instance to dft_q3_equicardinal and dft_q3_product, which establish equicardinality and the 64-element product with Q3 vertices. It also populates twoCubeUniversalityCert, the certificate collecting all 2³ instances. In the framework it realizes the eight-tick octave and D = 3 as the common cardinality |F₂³| = 8 across harmonic, vertex, and group structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.