q3Vertices_eq
plain-language theorem explainer
The theorem equates the two definitions of the vertex count for the recognition lattice Q₃, confirming it equals 8. Researchers deriving graph properties from the Recognition Science forcing chain cite this when verifying the 2^D structure for D=3. The proof is a direct decision procedure that confirms numerical identity between the exponential and constant definitions.
Claim. The recognition lattice $Q_3 = {0,1}^3$ has vertex count exactly 8.
background
The module defines the recognition lattice Q₃ as the 3-dimensional hypercube graph whose vertices are the points of {0,1}³. One sibling definition sets the vertex count to 2^3 while the depth module sets it directly to 8; the Euler characteristic identity V - E + F = 8 - 12 + 6 = 2 is recorded upstream. The local setting is the extraction of elementary graph invariants (vertex count, edge count, chromatic number) from the Recognition Science lattice before they are bundled into a single certificate.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the numerical equality between the two definitions of q3Vertices.
why it matters
The equality supplies the vertices_8 field of graphTheoryCert, which certifies that Q₃ has 8 vertices, 12 edges and chromatic number 2. It directly instantiates the framework landmark that Q₃ realizes 2^D vertices for D=3 spatial dimensions and closes the verification step that precedes any appeal to the Recognition Composition Law or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.