HasTwoCubeCount
plain-language theorem explainer
A finite type has 2³-structure precisely when its cardinality equals 8. Cross-domain researchers in Recognition Science cite this definition to unify counts across DFT modes, Pauli elements, Q3 vertices, and tick phases under the D=3 recognition cube. The definition is a direct cardinality equality that serves as the shared predicate for equicardinality and product theorems.
Claim. A finite type $T$ has $2^3$-structure if and only if its cardinality satisfies $|T| = 8$.
background
The module collects instances of the count 8 = 2³ across Recognition Science domains as the maximal-periodic structure for spatial dimension D = 3. This includes DFT-8 modes for fundamental harmonic decomposition, the Q3 vertex count in the recognition cube, the eight elements of the single-qubit Pauli group, and the 8-tick fundamental period. The definition supplies the common predicate that all listed structures satisfy the same finite cardinality.
proof idea
This is a definition rather than a derived theorem. It directly equates the Fintype.card of the input type T to the constant 2^3.
why it matters
This definition anchors the cross-domain universality claim C14. It feeds the downstream results dft_has_2cube, pauli_has_2cube, q3_has_2cube, tick_has_2cube, two_cube_equicardinal, and two_cube_pair_64. It realizes the T7 eight-tick octave and D = 3 spatial dimensions by showing that multiple physical and mathematical structures share the count of 8 for three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.