reactionMechanism_count
plain-language theorem explainer
The theorem asserts that the finite type of canonical organic reaction mechanisms has cardinality exactly five. Chemists or foundational modelers working in the Recognition Science chemistry module would cite this cardinality when fixing configDim to D = 5. The proof is a one-line decision procedure that exhausts the five inductive constructors.
Claim. $|ReactionMechanism| = 5$, where ReactionMechanism is the inductive type with 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. The upstream inductive definition ReactionMechanism enumerates exactly these five cases and derives the Fintype instance required for cardinality computation. This supplies the local setting for counting mechanisms in the chemistry depth of the framework.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card of the inductive type ReactionMechanism by exhaustive enumeration of its constructors.
why it matters
This theorem supplies the five_mechanisms field inside the reactionMechanismsCert definition in the same module. It fills the enumeration step tied to configDim D = 5 in the organic reaction mechanisms section of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.