GraphInvariantsCert
plain-language theorem explainer
GraphInvariantsCert is a structure that packages the assertion that exactly five graph invariants exist, matching configDim D = 5. Combinatorialists and Recognition Science researchers linking graph complexity to dimensional parameters would cite the certificate when counting canonical measures. The declaration is a bare structure definition whose single field records the Fintype cardinality equality.
Claim. The structure GraphInvariantsCert consists of the field asserting that the cardinality of the finite type of graph invariants equals 5, where the invariants are the chromatic number, clique number, independence number, genus, and treewidth.
background
The module identifies five canonical graph invariants for undirected graphs and equates their count to configDim D = 5. The inductive type GraphInvariant enumerates them explicitly as chromaticNumber, cliqueNumber, independenceNumber, genus, and treewidth, each a distinct complexity measure, and derives DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The declaration is a structure definition with no proof body or tactics. It directly introduces the type whose single field five_invariants records the equality Fintype.card GraphInvariant = 5.
why it matters
The structure supplies the type for the downstream definition graphInvariantsCert, which constructs an explicit instance via graphInvariant_count. It fixes the combinatorial count at five to match configDim D = 5, thereby connecting graph invariants to the dimensional parameters of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.