graphInvariant_count
plain-language theorem explainer
The theorem establishes that the inductive type enumerating five canonical graph invariants has cardinality exactly five. Combinatorial researchers formalizing Recognition Science would cite the result to certify the size of the invariant set linked to configDim. The proof is a one-line decision procedure on the finite type.
Claim. The finite set consisting of the chromatic number, clique number, independence number, genus, and treewidth has cardinality five.
background
The module sets out five canonical graph invariants for configuration dimension equal to 5. These are the chromatic number, clique number, independence number, genus, and treewidth, each a distinct complexity measure of an undirected graph. The local setting is the combinatorics layer of Recognition Science, where the count is fixed by the configDim parameter.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable equality Fintype.card GraphInvariant = 5, which follows immediately from the five constructors of the inductive type.
why it matters
The result populates the five_invariants field of graphInvariantsCert, which certifies completeness of the invariant collection. It directly realizes the module statement that five invariants correspond to configDim D = 5. In the framework this combinatorial count stands apart from the spatial dimension D = 3 derived in the forcing chain (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.