reactionMechanismsCert
plain-language theorem explainer
This definition supplies a certified structure asserting that the finite type of core organic reaction mechanisms has exactly five elements when the configuration dimension equals five. Researchers modeling organic chemistry within Recognition Science would cite it to anchor the enumeration of SN1, SN2, E1, E2, and pericyclic reactions. The definition is a direct instantiation that assigns the result of a decidable cardinality theorem to the structure field.
Claim. Let $R$ be the finite type of core organic reaction mechanisms. The declaration supplies the structure whose sole field asserts that the cardinality of $R$ equals 5.
background
The module establishes five canonical organic reaction mechanisms corresponding to configuration dimension D = 5: SN1 (unimolecular substitution), SN2 (bimolecular substitution), E1 (unimolecular elimination), E2 (bimolecular elimination), and pericyclic (concerted, orbital-symmetry-controlled). The structure ReactionMechanismsCert is defined to hold precisely when the cardinality of the ReactionMechanism type is five. The upstream theorem reactionMechanism_count establishes this equality by a decidable computation.
proof idea
The definition is a one-line wrapper that constructs an instance of ReactionMechanismsCert by setting its five_mechanisms field to the theorem reactionMechanism_count.
why it matters
This definition completes the certification of the five-mechanism count in the chemistry depth of the Recognition framework, directly supporting the claim that configDim D = 5 yields exactly these five core mechanisms. It fills the structure required by the module's theoretical setting and provides a zero-sorry anchor for downstream chemical derivations. No open questions are addressed here as the count is decidable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.