GraphInvariant
plain-language theorem explainer
The inductive type enumerates five canonical graph invariants tied to configuration dimension 5 in the Recognition Science framework: chromatic number, clique number, independence number, genus, and treewidth. Combinatorial researchers working on graph complexity measures within the theory would cite the enumeration when confirming that exactly these five are tracked. The definition introduces the five constructors and derives the supporting typeclass instances for decidability and finiteness.
Claim. Let $G$ be the inductive type whose constructors are the chromatic number, clique number, independence number, genus, and treewidth of an undirected graph.
background
The module identifies five canonical graph invariants for the case where the configuration dimension equals 5. These comprise the chromatic number (fewest colors for a proper vertex coloring), clique number (order of a largest complete subgraph), independence number (order of a largest independent set), genus (lowest surface genus permitting a crossing-free embedding), and treewidth (minimum width over all tree decompositions). Each serves as a distinct complexity measure of an undirected graph, with the formalization free of axioms or sorry placeholders.
proof idea
The declaration is an inductive definition that directly lists the five constructors. It then derives the instances DecidableEq, Repr, BEq, and Fintype in a single step to equip the type with equality testing, representation, boolean equality, and finite cardinality.
why it matters
The definition supplies the enumeration required by the downstream theorem graphInvariant_count establishing cardinality 5 and by the structure GraphInvariantsCert. It realizes the combinatorial layer for configuration dimension 5, consistent with the framework's selection of five distinct measures to support the forcing chain and recognition composition law. No open questions appear in the supplied documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.