q3Vertices
plain-language theorem explainer
The declaration sets the vertex count of the recognition lattice Q₃ to 2 raised to the third power. Researchers working on graph properties extracted from Recognition Science cite this when fixing the size of the 3-dimensional hypercube before deriving edge counts or Euler characteristics. The definition is a direct assignment with no computation or lemmas applied.
Claim. The vertex count of the recognition lattice Q₃ is $2^3$.
background
The module presents graph theory extracted from Recognition Science, taking the recognition lattice Q₃ = {0,1}³ as the prototypical graph. This lattice has 8 vertices equal to 2^D where D equals 3, 12 edges, is bipartite, and has chromatic number 2. The upstream result in GraphTheoryDepthFromRS records the Euler relation V - E + F = 8 - 12 + 6 = 2 and supplies the numerical value 8 for the same vertex count.
proof idea
This is a direct definition that assigns the natural number 2^3 to the vertex count. The equality q3Vertices_eq later confirms the value equals 8 by decision.
why it matters
The definition supplies the vertex count required by the GraphTheoryCert structure, which records vertices_8 : q3Vertices = 8 together with the edge and chromatic facts. It supports the Euler characteristic computation in q3EulerChar and matches the T8 step that forces D = 3 spatial dimensions with 2^D vertices on the recognition lattice. It closes one link in the chain from the recognition composition law to concrete graph invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.