ReactionMechanism
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.