ReactionMechanism
ReactionMechanism enumerates the five canonical organic reaction mechanisms that Recognition Science ties to configDim equal to 5. Chemists or foundational modelers would cite the enumeration when certifying that the dimensional constraint admits exactly these reaction types. The declaration is a direct inductive type definition with five constructors and automatic derivation of Fintype and related instances.
claimThe type of organic reaction mechanisms consists of the five constructors SN1 (unimolecular substitution), SN2 (bimolecular substitution), E1 (unimolecular elimination), E2 (bimolecular elimination), and pericyclic (concerted, orbital-symmetry-controlled).
background
The module Chemistry.ReactionMechanismsFromConfigDim defines five canonical core organic reaction mechanisms corresponding to configDim D = 5: SN1 (unimolecular substitution), SN2 (bimolecular substitution), E1 (unimolecular elimination), E2 (bimolecular elimination), pericyclic (concerted, orbital-symmetry-controlled). The module carries zero sorry statements or axioms. No upstream lemmas are referenced by the declaration.
proof idea
The declaration is a direct inductive definition introducing five distinct constructors. Automatic derivation supplies the DecidableEq, Repr, BEq, and Fintype instances with no explicit proof steps required.
why it matters in Recognition Science
This definition supplies the finite set whose cardinality is proved equal to 5 by the sibling theorem reactionMechanism_count and is certified by the structure ReactionMechanismsCert. It realizes the configDim = 5 constraint stated in the module documentation, embedding the five mechanisms into the Recognition Science framework.
scope and limits
- Does not enumerate mechanisms outside the five listed constructors.
- Does not derive rate laws, stereochemical outcomes, or selection rules.
- Does not connect to specific molecular structures, reagents, or conditions.
formal statement (Lean)
17inductive ReactionMechanism where
18 | sn1
19 | sn2
20 | e1
21 | e2
22 | pericyclic
23 deriving DecidableEq, Repr, BEq, Fintype
24