GraphTheorem
plain-language theorem explainer
This inductive type enumerates five canonical graph theorems (handshaking lemma, Euler formula, Kuratowski planarity criterion, four-color theorem, Ramsey theory) as the complete set tied to the 3-cube graph in Recognition Science. Discrete geometers or researchers modeling topological lattices would cite it when counting graph-theoretic content at configuration dimension 5. The declaration is a direct inductive enumeration that automatically derives decidable equality and finite-type structure.
Claim. Let $T$ be the inductive type whose five constructors are the handshaking lemma, Euler's formula, Kuratowski's theorem, the four-color theorem, and Ramsey theory. Then $T$ is a finite type with exactly five elements.
background
The module treats the 3-cube graph $Q_3$ (8 vertices, 12 edges, 6 faces) as the canonical recognition lattice. It identifies five classical graph theorems whose count equals configuration dimension 5. The Euler characteristic of $Q_3$ is stated as $V-E+F=2$, matching the topology of the 2-sphere.
proof idea
This is an inductive definition that lists the five theorems as constructors. No lemmas or tactics are invoked; the type is generated directly and the deriving clause supplies DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
The definition supplies the enumeration consumed by graphTheoremCount (which proves the cardinality is 5) and by GraphTheoryDepthCert (which records five_theorems, euler_q3=2, chromatic_q3=2). It realizes the configDim D=5 landmark for the $Q_3$ lattice inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.