FunctionalGroup
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not enumerate functional groups outside the five canonical classes tied to configDim = 5.
- Does not provide chemical reaction mechanisms or bonding details for the groups.
- Does not connect to specific molecular formulas or mass calculations from the phi-ladder.
- Does not address inorganic or other non-organic functional groups.
formal statement (Lean)
16inductive FunctionalGroup where
17 | hydroxyl
18 | carbonyl
19 | carboxyl
20 | amino
21 | thiolSulfide
22 deriving DecidableEq, Repr, BEq, Fintype
23