graphTheoremCount
plain-language theorem explainer
The theorem states that the inductive type enumerating canonical graph theorems for the recognition lattice has exactly five elements. A researcher deriving graph invariants from the three-cube lattice would cite this count to fix the configuration dimension. The proof is a direct decision procedure on the finite type.
Claim. The set of canonical graph theorems has cardinality $5$.
background
The module treats Q₃, the three-dimensional cube graph, as the canonical recognition lattice with eight vertices, twelve edges, and six faces. The inductive type GraphTheorem enumerates the five theorems handshaking, Euler, Kuratowski, fourColor, and ramsey. Upstream results supply the vertex count V(D) = 2^D and edge count E(D) = D × 2^{D-1} for D = 3, which together with the face count yield the Euler characteristic 2.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute Fintype.card on the inductive type GraphTheorem.
why it matters
This supplies the five_theorems field of graphTheoryDepthCert. It realizes the framework identification of five graph theorems with configuration dimension D = 3, consistent with the eight-tick octave and the topological identification of Q₃ with the sphere via Euler characteristic 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.