dft_q3_equicardinal
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the 2^3 count for domains outside the listed instances.
- Does not supply a physical interpretation or dynamics for the modes or vertices.
- Does not prove uniqueness of the representation up to isomorphism.
- Does not address continuous limits or infinite extensions of the structures.
formal statement (Lean)
82theorem dft_q3_equicardinal :
83 Fintype.card DFTMode = Fintype.card Q3Vertex :=
proof body
Term-mode proof.
84 two_cube_equicardinal dft_has_2cube q3_has_2cube
85
86/-- Pauli group and tick phases are equinumerous (both 8 = 2³). -/