functionalGroupsCert
Recognition Science chemistry derives five major organic functional groups from the configuration dimension. The definition packages this count into a certified structure for use in downstream derivations. It is realized by a direct assignment from the decidable cardinality result.
claimLet $FG$ denote the finite type of canonical organic functional groups. The definition constructs a certificate $C$ of type $FG Cert$ by setting the field asserting $|FG| = 5$ to the value supplied by the explicit cardinality theorem.
background
In the module on organic functional groups from configDim, five canonical classes are identified corresponding to configuration dimension D = 5: hydroxyl (alcohols/phenols), carbonyl (aldehyde/ketone), carboxyl (acids/esters), amino (amine/amide), and thiol/sulfide. This setup derives from the Recognition Science approach linking molecular features to the underlying configuration space. The upstream result is the theorem establishing that the cardinality of the FunctionalGroup type is exactly 5, proved by decision procedure. The structure FunctionalGroupsCert is defined to hold precisely this cardinality assertion as its sole field.
proof idea
The definition is a one-line record constructor that directly assigns the result of the functionalGroup_count theorem to the five_groups field of the FunctionalGroupsCert structure.
why it matters in Recognition Science
This definition completes the certification of the five functional groups in the chemistry depth of Recognition Science, directly supporting the module's claim of zero sorry statements. It provides the concrete witness for the configDim-derived count, which may feed into broader derivations of molecular properties from the phi-ladder and forcing chain, though no downstream uses are currently recorded. It aligns with the framework's extension of spatial dimensions to configuration dimensions for chemical classification.
scope and limits
- Does not list or classify the individual functional groups beyond their total count.
- Does not derive chemical reactivity or bonding properties from the groups.
- Does not connect the count to specific Recognition Science constants such as phi or the alpha band.
- Does not address extensions to other molecular classes outside the five canonical ones.
formal statement (Lean)
29def functionalGroupsCert : FunctionalGroupsCert where
30 five_groups := functionalGroup_count
proof body
Definition body.
31
32end IndisputableMonolith.Chemistry.OrganicFunctionalGroupsFromConfigDim