GraphTheoryCert
plain-language theorem explainer
GraphTheoryCert packages the vertex count, edge count, chromatic number, and edge factorization of the Q3 recognition lattice into one record. Researchers deriving discrete geometry or lattice models from Recognition Science cite it to access the 8 vertices, 12 edges, and bipartiteness invariants uniformly. The declaration is a plain structure whose four fields are direct equalities to the precomputed constants supplied by the module's q3* definitions.
Claim. The structure GraphTheoryCert asserts the following properties of the graph $Q_3$: $|V(Q_3)|=8$, $|E(Q_3)|=12$, chromatic number $2$, and $|E(Q_3)|=3*4$.
background
The module defines the recognition lattice $Q_3={0,1}^3$ as the basic graph arising from the Recognition Science derivation of spatial structure. Module documentation states that $Q_3$ has 8 vertices equal to $2^D$ for $D=3$, 12 edges equal to $32^{D-1}$, is bipartite, and therefore has chromatic number 2. Upstream definitions in both GraphTheoryDepthFromRS and the local module fix q3Vertices to 8, q3Edges to 12 (equivalently $32^(3-1)$), and q3ChromaticNumber to 2, supplying the concrete values referenced by the certificate fields.
proof idea
The declaration is a structure definition with no proof body. It consists of four field declarations that simply record the equalities vertices_8, edges_12, chromatic_2, and edges_factored to the values already supplied by the sibling definitions q3Vertices, q3Edges, and q3ChromaticNumber.
why it matters
GraphTheoryCert supplies the bundled invariants that the downstream graphTheoryCert construction instantiates via equality lemmas. It directly encodes the T7 eight-tick octave and T8 derivation of three spatial dimensions by packaging the $2^3$ vertex count and the three-axis edge structure of the recognition lattice. The certificate closes the elementary graph layer before results on Hamiltonian cycles or further Recognition Composition Law applications are derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.