FunctionalGroupsCert
The structure FunctionalGroupsCert certifies that the finite type enumerating major organic functional groups has cardinality exactly five. Chemists working in the Recognition Science framework cite it to anchor the count of canonical classes (hydroxyl, carbonyl, carboxyl, amino, thiol/sulfide) to the five-dimensional configuration space. The definition is a direct structure wrapper packaging the Fintype.card equality with no additional lemmas or reductions.
claimLet $F$ be the inductive type with constructors hydroxyl, carbonyl, carboxyl, amino, thiolSulfide. The structure FunctionalGroupsCert consists of the single field asserting that the cardinality of the finite type $F$ equals 5.
background
The module identifies five canonical functional-group classes arising from configuration dimension equal to five: hydroxyl (alcohols/phenols), carbonyl (aldehydes/ketones), carboxyl (acids/esters), amino (amines/amides), and thiol/sulfide. The sibling inductive type FunctionalGroup enumerates precisely these five constructors and derives DecidableEq, Repr, BEq, and Fintype instances. This supplies the local theoretical setting in which the Recognition Science chemistry depth is tied directly to configDim = 5.
proof idea
The declaration is a structure definition whose sole field is the proposition Fintype.card FunctionalGroup = 5. No lemmas are applied and no tactics are used; the structure directly packages the cardinality statement for downstream instantiation.
why it matters in Recognition Science
This supplies the type for the concrete certificate functionalGroupsCert, which populates the field via the enumerated count. It realizes the module claim that exactly five canonical classes arise at configDim = 5. In the framework it extends the forcing-chain landmarks by fixing a chemistry-specific count without reference to the spatial dimension D = 3 or the phi-ladder.
scope and limits
- Does not derive chemical reactivity or bonding rules for any group.
- Does not connect the groups to the phi-ladder mass formula or constants.
- Does not prove these five exhaust all possible organic functional groups.
- Does not address Berry creation threshold or Z_cf values.
formal statement (Lean)
26structure FunctionalGroupsCert where
27 five_groups : Fintype.card FunctionalGroup = 5
28