functionalGroup_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not enumerate functional groups outside the five canonical classes.
- Does not derive the groups from J-cost or Recognition Composition Law equations.
- Does not address stereochemistry, reactivity, or higher-order molecular interactions.
Lean usage
theorem groups_certified : functionalGroupsCert.five_groups = 5 := by rw [functionalGroup_count]formal statement (Lean)
24theorem functionalGroup_count : Fintype.card FunctionalGroup = 5 := by decide
proof body
25