FunctionalGroup
plain-language theorem explainer
The inductive definition enumerates five canonical organic functional groups tied to configDim equal to 5. Chemists or Recognition Science modelers would cite it when counting or certifying functional groups in molecular structures derived from configuration dimension. The definition lists the five constructors explicitly and derives decidable equality, representation, boolean equality, and finite type structure automatically.
Claim. Define the inductive type of functional groups as the disjoint union of five classes: hydroxyl (alcohols and phenols), carbonyl (aldehydes and ketones), carboxyl (acids and esters), amino (amines and amides), and thiol/sulfide.
background
The module on organic functional groups from configDim states that five canonical classes arise when configDim D equals 5. These classes are hydroxyl for alcohols and phenols, carbonyl for aldehydes and ketones, carboxyl for acids and esters, amino for amines and amides, and thiol/sulfide. The module records zero sorry or axiom in the Lean formalization of this enumeration.
proof idea
This is a direct inductive definition with five explicit constructors, one per functional group class. The deriving clauses for DecidableEq, Repr, BEq, and Fintype are generated automatically with no additional proof steps required.
why it matters
This definition supplies the enumeration used by the theorem functionalGroup_count to prove Fintype.card equals 5 and by the structure FunctionalGroupsCert to certify the count. It fills the chemistry depth section by linking configDim = 5 to the standard organic functional groups listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.