StereoClass
plain-language theorem explainer
Recognition Science chemistry defines five stereoisomer classes via an inductive type. Chemists cite the definition when certifying that configDim equals 5 for molecular configurations. The structure is introduced directly with automatic derivation of decidable equality and finite type.
Claim. The stereoisomer classes form the inductive type consisting of the five elements enantiomers, diastereomers, cis-trans geometric isomers, conformational isomers, and atropisomers.
background
The module Stereochemistry Classes from configDim introduces five canonical stereoisomer classes corresponding to configDim D = 5. These comprise enantiomers, diastereomers, cis-trans (geometric), conformational, and atropisomers. The local theoretical setting is the chemistry depth of Recognition Science, with zero sorry or axiom in the Lean formalization.
proof idea
The declaration is the inductive definition that introduces the five constructors directly, followed by derivation of DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the enumeration required by the downstream StereochemistryCert structure asserting Fintype.card equals 5 and by the theorem stereoClass_count proved by decide. It fills the chemistry depth proposition that exactly five classes exist for configDim = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.