StereochemistryCert
plain-language theorem explainer
StereochemistryCert packages the assertion that exactly five stereochemistry classes exist under the Recognition Science chemistry model. Molecular theorists working with configDim D = 5 would cite it when confirming the completeness of isomer enumeration. The declaration is a bare structure definition whose single field records the Fintype cardinality of the enumerated classes.
Claim. The structure StereochemistryCert consists of the single datum asserting that the cardinality of the finite type of stereochemistry classes equals five, where the classes are the five enumerated kinds: enantiomers, diastereomers, cis-trans geometric isomers, conformational isomers, and atropisomers.
background
The module establishes five canonical stereoisomer classes tied to configDim D = 5 in the Recognition Science framework. StereoClass is the inductive type whose constructors are precisely enantiomers, diastereomers, cisTransGeometric, conformational, and atropisomers, equipped with Fintype and DecidableEq instances. This local setting follows directly from the upstream derivation of chemistry depth from the unified forcing chain (T0-T8), where self-similarity and the eight-tick octave fix the number of distinct configurational distinctions.
proof idea
The declaration is a structure definition. It contains no tactics, lemmas, or reduction steps; the single field simply records the equality Fintype.card StereoClass = 5.
why it matters
StereochemistryCert supplies the type for the downstream definition stereochemistryCert, which populates the field via stereoClass_count. It thereby closes the chemistry-depth slot in the Recognition Science framework by confirming the five classes predicted by configDim = 5, consistent with the dimensional forcing that yields D = 3 spatial dimensions and the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.