dft_q3_product
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.