Chemistry Stereochemistry Classes From Config Dim Stereo Class

The five stereoisomer classes

Stereoisomers are molecules that share the same atoms and the same sequence of bonds but differ in how those atoms sit in space. Chemists group them into five canonical classes: enantiomers, diastereomers, cis-trans geometric isomers, conformational isomers, and atropisomers. Enantiomers are mirror images that cannot be superimposed, like left and right hands. Diastereomers are stereoisomers that are not mirror images. Cis-trans isomers differ by the arrangement of substituents across a double bond or ring. Conformational isomers differ by rotation about single bonds. Atropisomers arise from restricted rotation about a single bond, creating stable chiral shapes.

The classification has practical bite. Enantiomers often behave identically in ordinary reactions but differently in biological settings, where one form may be a medicine and the other a toxin. Diastereomers usually have different physical properties, so chemists can separate them by crystallization or chromatography. Cis-trans and conformational distinctions affect molecular shape, which governs how a molecule fits an enzyme or a receptor. Atropisomerism, once a curiosity, now matters in drug design because the restricted rotation can lock a molecule into a biologically active shape.

In Recognition Science, the machine-checked library of formal theorems defines a StereoClass as an inductive type with exactly those five constructor cases: enantiomers, diastereomers, cisTransGeometric, conformational, atropisomers. A proved theorem, stereoClass_count, states that the number of distinct StereoClass values is five, and the proof is a direct computation. The declaration also bundles this fact into a certificate structure, StereochemistryCert, which carries the count as its only field. The framework thus records the standard chemistry classification as a finite, checkable object: five named classes, no more, no fewer.

What the declaration does not do is just as important. It does not define what each class means chemically; it only names the five categories and fixes their count. It does not say how to assign a given molecule to a class, and it does not claim that every stereoisomer falls into exactly one of these five classes. Real chemistry has edge cases, such as molecules that are both conformational and atropisomeric, and the formal object does not resolve those. The declaration is a vocabulary: a way for the framework to talk about stereochemistry, not a theory of it.

The gain is a stable reference point. When the framework's library discusses stereochemistry, every theorem can rely on a fixed list of five classes, checked by the machine, rather than a prose list that might drift. The count theorem gives a single number, five, that other formal results can use. For a reader, the practical lesson is that the formal declaration mirrors a textbook classification but deliberately stays silent on the chemical judgment that assigns real molecules to those classes.

theorem stereoClass_count : Fintype.card StereoClass = 5 := by decide

structure StereochemistryCert where
  five_classes : Fintype.card StereoClass = 5

What this page does not claim

The declaration does not define the chemical meaning of each stereoisomer class. The declaration does not assign any particular molecule to a class. The declaration does not claim that every stereoisomer falls into exactly one of the five classes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/StereochemistryClassesFromConfigDim.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: