TwoCubeUniversalityCert
plain-language theorem explainer
The TwoCubeUniversalityCert structure records that DFTMode, Q3Vertex, PauliElement and TickPhase each have cardinality exactly 8, that any two finite types with this property are equicardinal, and that the product of two such types has cardinality 64 satisfying both 8*8 and 2^6. Cross-domain researchers would cite it to unify the 2^3 count across harmonic, geometric, algebraic and temporal instances in D=3. The definition assembles the four HasTwoCubeCount facts with the equicardinality lemma and the arithmetic identities.
Claim. Let $HasTwoCubeCount(T)$ denote that a finite type $T$ satisfies $|T|=8$. The structure TwoCubeUniversalityCert asserts $HasTwoCubeCount(DFTMode)$, $HasTwoCubeCount(Q_3Vertex)$, $HasTwoCubeCount(PauliElement)$, $HasTwoCubeCount(TickPhase)$, the equicardinality law that any two finite types satisfying the predicate have equal cardinality, the equality $|DFTMode × Q_3Vertex|=64$, and the identities $64=8×8 ∧ 64=2^6$.
background
In Recognition Science the count $2^3=8$ is the maximal periodic structure for spatial dimension $D=3$, appearing as the eight-tick octave. The predicate HasTwoCubeCount(T) holds precisely when a finite type T has cardinality 8. The module assembles four canonical instances: the eight DFT modes for harmonic decomposition, the eight vertices of the recognition cube Q3, the eight Pauli group elements, and the eight phases of the tick cycle. Upstream results supply the inductive definitions of these types, each equipped with Fintype instances of cardinality 8.
proof idea
The structure is introduced by direct construction, supplying the four HasTwoCubeCount certificates for each domain type, the equicardinality lemma two_cube_equicardinal, and the arithmetic facts on 64. No tactics intervene; the definition simply packages the component lemmas already established for the individual instances.
why it matters
This definition packages the evidence for the 2^3 universality that feeds the parent theorem twoCubeUniversalityCert. It fills the C14 claim by exhibiting the shared count across DFT, Q3, Pauli and tick domains. In the framework it instantiates the eight-tick octave (T7) and the emergence of D=3 (T8), supplying concrete types that realize the recognition cube cardinality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.