GraphInvariantsCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that the five listed invariants are independent or minimal for arbitrary graphs.
- Does not compute the numerical value of any invariant on a concrete graph.
- Does not relate the invariants to the forcing chain T0-T8 or to constants such as phi or alpha.
- Does not address directed graphs, infinite graphs, or additional graph properties.
formal statement (Lean)
28structure GraphInvariantsCert where
29 five_invariants : Fintype.card GraphInvariant = 5
30