graphInvariant_count
plain-language theorem explainer
The theorem establishes that exactly five graph invariants arise from the configuration dimension in Recognition Science. Combinatorial researchers verifying the framework's discrete structure would cite this count to confirm completeness of the invariant set. The proof is a direct decision procedure on the finite inductive type.
Claim. The set of canonical graph invariants has cardinality five: $|$chromatic number, clique number, independence number, genus, treewidth$| = 5$.
background
The module defines five canonical graph invariants corresponding to configDim D = 5: chromatic number, clique number, independence number, genus, and treewidth. Each serves as a distinct complexity measure of an undirected graph. The inductive type enumerates these five cases and derives DecidableEq and Fintype instances to support cardinality computation. This setup supplies the combinatorial depth for the Recognition Science framework with zero sorry or axiom.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the cardinality of the finite type defined by the five-constructor inductive.
why it matters
This supplies the five_invariants field for the GraphInvariantsCert definition, certifying the invariant count. It aligns with the configDim D=5 requirement in the Recognition framework, supporting derivation of physics from graph structures consistent with the forcing chain and eight-tick octave. The result closes the enumeration without open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.