graphTheoryCert
plain-language theorem explainer
graphTheoryCert assembles four equality theorems into a single GraphTheoryCert record for the Q3 lattice. A researcher modeling discrete space from recognition principles would cite this certificate to invoke the vertex count, edge count, chromatic number, and edge factorization without separate proofs. The definition is a direct record literal that references the four upstream equality results.
Claim. Let $Q_3$ be the recognition lattice on vertex set $2^3$. The certificate certifies that $Q_3$ has exactly 8 vertices, exactly 12 edges, chromatic number 2, and that the edge count equals $3$ times $4$.
background
The module defines graph properties of the recognition lattice $Q_3 = {0,1}^3$, the prototypical graph in Recognition Science. This lattice has 8 vertices equal to $2^D$ and 12 edges equal to $D$ times $2^{D-1}$ for $D=3$, is bipartite, and therefore has chromatic number 2. The structure GraphTheoryCert packages these four facts as a single record whose fields are the equalities vertices_8, edges_12, chromatic_2, and edges_factored.
proof idea
The definition constructs the GraphTheoryCert record by direct field assignment: vertices_8 receives q3Vertices_eq, edges_12 receives q3Edges_eq, chromatic_2 receives q3Chromatic_eq, and edges_factored receives q3Edges_factored. Each of the four referenced theorems is proved by decide or rfl, so the certificate is assembled by record construction alone.
why it matters
The certificate supplies a verified bundle for the 8-vertex, 12-edge, 2-chromatic properties of $Q_3$, which realizes the eight-tick octave and $D=3$ spatial dimensions inside the Recognition Science framework. It closes the basic graph-theory scaffolding for the recognition lattice and stands ready for use in any later development that invokes the discrete geometry of $Q_3$. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.