q3_has_2cube
plain-language theorem explainer
The theorem shows that the Q3Vertex inductive type, enumerating the eight vertices of the recognition cube, satisfies the 2³-structure by having cardinality exactly 8. Cross-domain researchers in Recognition Science cite it when equating counts across DFT modes, Pauli groups, and tick phases to establish shared universality. The proof is a one-line wrapper that unfolds the cardinality predicate and lets the decision tactic confirm the equality.
Claim. $|Q_3| = 2^3$, where $Q_3$ is the finite set of vertices with binary coordinates in three dimensions.
background
The CrossDomain.TwoCubeUniversality module collects instances of the structural claim that the count 8 = 2³ = |F₂³| appears as the maximal-periodic structure for spatial dimension D = 3. HasTwoCubeCount T is the proposition that a finite type T satisfies Fintype.card T = 2 ^ 3. Q3Vertex is the inductive type with exactly eight constructors v000 through v111, each a binary triple, and it derives Fintype, DecidableEq, and related instances so the cardinality is computable by decision procedures.
proof idea
The proof is a one-line wrapper that unfolds HasTwoCubeCount to the goal Fintype.card Q3Vertex = 2 ^ 3 and then applies the decide tactic, which succeeds because Q3Vertex has eight constructors and derives the necessary Fintype instance.
why it matters
This supplies the Q3Vertex instance of the 2³-property and is invoked by dft_q3_equicardinal to equate it with DFTMode cardinality, by dft_q3_product to obtain the 64-element product, and by twoCubeUniversalityCert to certify the full collection. It instantiates the T8 step of the forcing chain that forces D = 3 and the eight-tick octave, confirming that the recognition cube count matches the Boolean algebra atoms on three variables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.