two_cube_equicardinal
plain-language theorem explainer
Any two 2³-cube domains have equal finite cardinality. Cross-domain proofs in Recognition Science cite this to equate DFT modes with Q3 vertices and Pauli elements with tick phases. The proof is a one-line rewrite that substitutes the two defining cardinality equalities.
Claim. Let $A$ and $B$ be finite types. If $|A| = 2^3$ and $|B| = 2^3$, then the cardinality of $A$ equals the cardinality of $B$.
background
The module collects instances of the 2³ = 8 structure across domains and proves they share the same count. HasTwoCubeCount is the proposition that a finite type T satisfies Fintype.card T = 2^3 = 8; this encodes the recognition cube count for D = 3. The module lists canonical cases including DFT-8 modes, Q3 vertices, Pauli group elements, and 8-tick periods, all with cardinality exactly 8.
proof idea
The proof is a one-line wrapper that rewrites the two hypotheses hA and hB. Each hypothesis is the defining equality of HasTwoCubeCount, so substitution immediately yields the desired cardinality equality.
why it matters
This result feeds dft_q3_equicardinal, pauli_tick_equicardinal, and the TwoCubeUniversalityCert definition. It realizes the C14 claim that 2³ = 8 appears uniformly as the maximal-periodic structure for spatial dimension D = 3, consistent with the eight-tick octave and the recognition cube. The module reports zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.