dft_q3_product
The Cartesian product of the eight DFT modes and the eight Q3 vertices has cardinality exactly 64. Cross-domain researchers cite this to confirm that both the harmonic decomposition and the recognition cube realize the same 2^3 count. The proof is a direct one-line application of the general product lemma for any two types satisfying the 2^3 cardinality property.
claimLet DFTMode denote the finite set of eight discrete Fourier transform modes and Q₃Vertex the finite set of eight vertices of the recognition cube. Then the cardinality of their Cartesian product equals 64.
background
The module establishes the structural identity 2³ = 8 across domains for spatial dimension D = 3. HasTwoCubeCount (T : Type) [Fintype T] is the proposition 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, dft_has_2cube proves HasTwoCubeCount DFTMode by unfolding and deciding; q3_has_2cube does the same for Q3Vertex. The key supporting lemma states: for types A and B each satisfying HasTwoCubeCount, Fintype.card (A × B) = 64.
proof idea
The proof is a one-line term that applies the general lemma two_cube_pair_64 to the two facts dft_has_2cube and q3_has_2cube.
why it matters in Recognition Science
This theorem supplies one concrete instance for the TwoCubeUniversalityCert definition, which assembles the 2^3 property across DFT, Q3, Pauli, and tick domains. It directly supports the module's claim that the D = 3 recognition cube count 8 appears uniformly, consistent with the eight-tick octave and the forcing of three spatial dimensions. The result closes a small gap in the cross-domain universality certificate without introducing new hypotheses.
scope and limits
- Does not assign physical interpretations to the DFT modes or Q3 vertices.
- Does not prove the 2^3 property for any domain outside the listed siblings.
- Does not address non-finite types or structures with cardinality other than 8.
- Does not derive the product identity from the Recognition Composition Law.
formal statement (Lean)
92theorem dft_q3_product :
93 Fintype.card (DFTMode × Q3Vertex) = 64 :=
proof body
Term-mode proof.
94 two_cube_pair_64 dft_has_2cube q3_has_2cube
95
96/-- 64 = 8² and 64 = 2^6. Both identities. -/