Q3Vertex
plain-language theorem explainer
The declaration enumerates the eight vertices of the 3-cube over GF(2) as an inductive type with derived decidable equality and finite-type structure. Cross-domain universality arguments in Recognition Science cite it as the canonical model for the 2^3 count in spatial dimension D=3. The definition is a direct inductive enumeration of the binary triples with automatic typeclass derivation.
Claim. Let $Q_3$ be the finite set of all points with coordinates in the field with two elements raised to the third power, i.e., all triples $(x,y,z)$ where each coordinate lies in $F_2$.
background
The module establishes that the integer 8 appears uniformly as the maximal periodic structure for three spatial dimensions, matching the eight-tick octave and the recognition cube. It lists concrete realizations including DFT-8 modes, Pauli group elements, tick phases, and the vertices of the recognition cube. Q3Vertex supplies the explicit model for the last of these. HasTwoCubeCount is the typeclass asserting that a type has cardinality exactly eight; the downstream theorems q3_has_2cube and TwoCubeUniversalityCert invoke it directly on this definition.
proof idea
The declaration is a primitive inductive definition that lists the eight constructors v000 through v111. Derivation of DecidableEq, Repr, BEq, and Fintype is performed automatically by the compiler; no lemmas or tactics are applied.
why it matters
Q3Vertex supplies the concrete type used by dft_q3_equicardinal and dft_q3_product to prove that DFT modes and Q3 vertices are equinumerous and that their Cartesian product has cardinality 64. It realizes one of the eight instances listed in the C14 universality claim, directly supporting the structural identity |T|=2^3 for D=3. The definition closes the recognition-cube slot in the cross-domain collection and feeds the TwoCubeUniversalityCert structure that aggregates all 2^3 instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.