dft_q3_equicardinal
plain-language theorem explainer
The theorem shows that DFT modes and recognition-cube vertices Q3 both have cardinality exactly 8. Cross-domain researchers in Recognition Science cite it to confirm that the 2^3 count appears uniformly in harmonic spectra and spatial recognition structures. The proof is a direct one-line application of the general equicardinality lemma for any two types that each satisfy the HasTwoCubeCount predicate.
Claim. Let $M$ be the type of discrete Fourier transform modes and $V$ the type of recognition-cube vertices. Then $|M| = |V|$.
background
The module establishes the structural identity 8 = 2^3 across Recognition Science domains for spatial dimension D = 3. HasTwoCubeCount is the predicate asserting that a finite type T satisfies Fintype.card T = 2^3. DFTMode is the inductive type with eight constructors m0 through m7; Q3Vertex is the inductive type with eight constructors v000 through v111. Upstream lemmas dft_has_2cube and q3_has_2cube each unfold the predicate and decide the equality by enumeration.
proof idea
The proof is a term-mode one-line wrapper. It applies the general lemma two_cube_equicardinal to the two upstream theorems dft_has_2cube and q3_has_2cube, which supply the HasTwoCubeCount hypotheses for each type.
why it matters
This declaration fills one instance of the C14 universality claim that the count 8 = 2^3 appears as the maximal periodic structure for D = 3. It directly supports the eight-tick octave (T7) and the recognition cube count. The result sits inside the cross-domain collection that also covers Pauli elements and tick phases; downstream work on wave-63 structures would invoke the shared cardinality to equate harmonic and geometric representations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.