stereoClass_count
plain-language theorem explainer
The theorem establishes that the finite type of stereochemistry classes has cardinality exactly 5, matching the five classes fixed by configDim D = 5. Chemists working inside the Recognition Science monolith would cite the result when certifying that the stereoisomer enumeration is complete before feeding it into molecular certificates. The proof is a single decision tactic that exhausts the five inductive constructors.
Claim. The set of stereochemistry classes has cardinality five: $|S| = 5$, where $S$ is the finite type whose elements are the five canonical classes (enantiomers, diastereomers, cis-trans geometric, conformational, atropisomers).
background
The module fixes five stereoisomer classes that arise once configDim is set to D = 5. These classes are introduced by an inductive type whose constructors are precisely enantiomers, diastereomers, cis-trans geometric, conformational, and atropisomers; the type automatically derives Fintype, DecidableEq and Repr. The surrounding Chemistry depth of the Recognition Science framework treats this enumeration as the direct consequence of the dimensional parameter D = 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card StereoClass = 5. The tactic succeeds because the inductive type has exactly five constructors and derives Fintype, allowing exhaustive enumeration without further lemmas.
why it matters
The result supplies the five_classes field inside the stereochemistryCert definition, thereby certifying the stereochemistry classification for the Chemistry depth. It directly records the claim that configDim D = 5 produces precisely these five classes, closing one concrete step in the dimensional constraints of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.