ReactionMechanismsCert
plain-language theorem explainer
The structure ReactionMechanismsCert packages a cardinality certificate fixing exactly five core organic reaction mechanisms in the Recognition Science chemistry layer. Researchers modeling reactions under configDim = 5 would cite it to anchor the enumeration of SN1, SN2, E1, E2, and pericyclic cases. The definition is a direct structure whose single field asserts the Fintype cardinality equality on the inductive type.
Claim. Let $R$ be the inductive type whose constructors are the five mechanisms SN1, SN2, E1, E2, and pericyclic. The structure ReactionMechanismsCert consists of the single field asserting that the cardinality of $R$ equals 5.
background
The module sets configDim to 5 to match the five canonical organic reaction mechanisms: SN1 (unimolecular substitution), SN2 (bimolecular substitution), E1 (unimolecular elimination), E2 (bimolecular elimination), and pericyclic (concerted, orbital-symmetry-controlled). The sibling inductive type ReactionMechanism enumerates precisely these five cases and derives DecidableEq, Repr, BEq, and Fintype instances. This structure therefore supplies a Lean-level certificate that the count is fixed at five, consistent with the module's claim of zero sorry or axiom.
proof idea
This is a structure definition whose sole field requires Fintype.card ReactionMechanism = 5. The equality holds definitionally once the inductive type supplies its five constructors and the derived Fintype instance is in scope; no tactics or lemmas are applied beyond the inductive construction itself.
why it matters
The certificate is instantiated by the downstream definition reactionMechanismsCert, which supplies the concrete value reactionMechanism_count. It anchors the chemistry depth of the framework by fixing the mechanism count to configDim = 5, aligning with the eight-tick octave and dimensional forcing (T8) that produces integer counts from the J-uniqueness and phi fixed-point steps. It leaves open the derivation of these specific mechanisms from the Recognition Composition Law or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.