functionalGroup_count
plain-language theorem explainer
The theorem asserts that the finite type FunctionalGroup has cardinality exactly five, matching the configuration dimension D=5 for major organic groups in Recognition Science chemistry. Chemists classifying molecular structures under the phi-ladder would cite this count to certify the canonical list. The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression.
Claim. The cardinality of the set of canonical organic functional groups is five: $|FunctionalGroup| = 5$, where the set consists of hydroxyl, carbonyl, carboxyl, amino, and thiol/sulfide.
background
The module derives the five major organic functional groups directly from configDim with D=5. The inductive type FunctionalGroup enumerates the classes hydroxyl (alcohols/phenols), carbonyl (aldehyde/ketone), carboxyl (acids/esters), amino (amine/amide), and thiol/sulfide, each equipped with DecidableEq and Fintype instances. This count supplies the five_groups field in the downstream FunctionalGroupsCert definition within the same module.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on Fintype.card FunctionalGroup. The tactic succeeds because the inductive type has exactly five constructors and derives the required decidable instances.
why it matters
This theorem populates the five_groups field of FunctionalGroupsCert, completing the certification of the five-group classification. It implements the module claim that configDim D=5 yields these canonical groups, connecting to the Recognition Science forcing chain (T5 J-uniqueness through T8 D=3) where dimensions emerge from the J-function and phi fixed point. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.