Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.Kinetic_Resolution3_FromJCost

show as:
view Lean formalization →

Packages three-component kinetic resolution in chemistry as cost inequalities derived from the Recognition J-cost. Defines a domain cost, a strictly positive canonical threshold, and an inhabited certificate type recording the resolution bounds. Chemists or RS auditors tracking selection rules from cost geometry would cite it. The module is largely definitional, with short nonnegativity and positivity lemmas.

claimFrom the Recognition cost $J$, the module defines a domain cost $C$, a canonical threshold $\theta>0$, and a certificate type asserting three-way kinetic-resolution inequalities for $C$ relative to $\theta$. Nonnegativity of $C$ and positivity of $\theta$ are recorded, and the certificate type is inhabited.

background

Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ on positive reals (equivalently $\cosh(\log x)-1$). The Recognition Composition Law constrains how $J$ behaves under products and quotients; chemistry modules import that cost geometry rather than re-deriving it.

This module sits in the Chemistry domain and builds on Constants (RS-native units, including the tick $\tau_0$) and Cost. Sibling names indicate a domain-level cost functional, its evaluation identity, nonnegativity, a canonical threshold with a positivity proof, and a certificate bundle KinRes3Cert together with a concrete inhabitant.

Kinetic resolution here means cost-ordered discrimination among three competing channels or stereochemical pathways. The threshold is the cut that separates resolved from unresolved regimes once costs are measured in J-units.

proof idea

Definition-first module, not a deep theorem chain. It introduces domainCost and proves an evaluation identity plus nonnegativity, defines canonicalThreshold and proves positivity, then packages the three-way resolution inequalities into KinRes3Cert with an explicit inhabitant cert. Supporting facts are short algebraic or positivity arguments off the imported J-cost; there is no multi-step forcing or analytic existence proof in the module skeleton.

why it matters in Recognition Science

Gives Chemistry a reusable certificate shape for three-component kinetic resolution forced by J-cost geometry, rather than by fitted rate constants. That keeps selection rules inside the same cost language as the forcing chain (T5 J-uniqueness and the RCL) and the RS unit conventions from Constants.

No downstream edges are recorded yet, so the module presently acts as a local interface: later stereochemistry or catalysis results can assume KinRes3Cert instead of reopening cost inequalities. It does not itself close a named paper proposition; it standardizes the cost-side hypothesis those propositions will cite.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)