GraphInvariantsCert
plain-language theorem explainer
GraphInvariantsCert is the structure recording that the set of graph invariants has cardinality exactly five. Combinatorial researchers in Recognition Science cite it to fix the configuration dimension at five for the listed complexity measures. The definition is a direct record whose single field is the cardinality equality supplied by the Fintype instance on the five-constructor inductive type.
Claim. Let $I$ be the finite set whose elements are the chromatic number, clique number, independence number, genus, and treewidth of an undirected graph. The structure $C$ is the record type containing the single assertion that the cardinality of $I$ equals 5.
background
The module treats graph invariants as combinatorial objects derived from configuration dimension, fixed at five. It enumerates five canonical measures of undirected-graph complexity: chromatic number, clique number, independence number, genus, and treewidth. The upstream inductive definition lists precisely these five cases and equips the type with a Fintype instance, so that its cardinality is immediately five.
proof idea
The declaration is a structure definition whose sole field is the equality Fintype.card of the inductive type equals five. No lemmas are invoked; the equality follows at once from the automatic Fintype derivation for an inductive type with five constructors.
why it matters
The structure supplies the type instantiated by the downstream certificate that confirms five invariants at configuration dimension five. It realizes the module statement that these five measures fix the combinatorial dimension and feeds further invariant calculations in the Recognition framework, where dimensions are forced from the J-function and phi-ladder. No open questions remain at this enumeration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.