q3Vertices
plain-language theorem explainer
q3Vertices defines the vertex count of the 3-cube graph Q₃ as exactly 8. Recognition Science researchers cite this constant when computing the Euler characteristic of the canonical recognition lattice or populating graph theory certificates. It is a direct constant definition that hardcodes the value to match the 2^3 hypercube construction from the base module.
Claim. The number of vertices in the three-dimensional hypercube graph $Q_3$ is $8$.
background
Q₃ is the 3-cube graph, presented in the module as the canonical recognition lattice with 8 vertices, 12 edges, and 6 faces. The local setting states that its Euler characteristic equals 2, matching χ(S²), and that five canonical graph theorems hold for configDim D = 5. The upstream definition in GraphTheoryFromRS sets the same quantity to 2^3, confirming the count via the binary hypercube structure.
proof idea
This is a one-line definition that directly assigns the constant 8. It does not apply any lemmas or tactics but aligns with the upstream result q3Vertices = 2^3 and the theorem q3Vertices_eq that verifies equality to 8.
why it matters
The definition supplies the vertex count required by q3EulerChar (which computes V - E + F) and by the GraphTheoryCert structure that asserts vertices_8 : q3Vertices = 8. It anchors the claim that Q₃ realizes the five graph theorems for D = 5 and confirms topological equivalence to the sphere via χ = 2. The placement closes the numerical foundation for the Recognition Science graph theory depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.