Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.StereochemistryClassesFromConfigDim

show as:
view Lean formalization →

This module defines stereochemistry classes and certificates derived from configuration dimension in the Recognition Science chemistry layer. Researchers modeling molecular isomers under RS rules would cite these definitions to classify structures. It is a definition module that introduces the core objects without proofs or derivations.

claimThe module introduces $\text{StereoClass}$ (stereochemistry class indexed by configuration dimension), $\text{stereoClass_count}$ (enumeration of such classes), and $\text{StereochemistryCert}$ (certificate linking a class to its dimensional origin).

background

The module sits in the Chemistry domain and imports the Constants module, whose sole documented content is the RS time quantum $\tau_0 = 1$ tick. It also imports Mathlib for basic type and structure support. The sibling declarations StereoClass, stereoClass_count, StereochemistryCert, and stereochemistryCert supply the concrete definitions that the module organizes.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the basic stereochemistry vocabulary that later chemistry results in the monolith are expected to consume, even though the current used_by list is empty. It therefore occupies an early position in the RS chemistry development chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)