Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.Flash_Point_FromJCost

show as:
view Lean formalization →

Module that packages chemistry flash-point thresholds from the RS J-cost. It defines a domain cost, a canonical positive threshold, and an inhabited FlashPointCert bundle. RS chemistry auditors use it when a phase or ignition bound must sit on the same cost functional as the rest of the monolith. Content is mostly definitions plus short nonnegativity and positivity lemmas.

claimPackage a domain cost $C$ built from the RS cost $J$, a canonical threshold $\theta>0$, and a flash-point certificate asserting the threshold relation on chemical domains, with an explicit inhabited witness.

background

Recognition Science forces a unique nonnegative cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) via the Recognition Composition Law; that functional lives in the Cost import. Constants supplies the RS-native tick $\tau_0=1$.

In the chemistry layer, flash point is treated as a pure threshold crossing: evaluate a domain cost on a chemical configuration and compare it to a fixed positive cutoff. The module therefore introduces a domain cost (with an evaluation identity and a nonnegativity lemma), a canonical threshold (with a positivity lemma), and a FlashPointCert structure together with a concrete inhabited certificate.

proof idea

Definition module, not a deep proof development. Domain cost is assembled from the imported $J$-cost; nonnegativity of the domain cost and positivity of the canonical threshold are short analytic lemmas. FlashPointCert is a structure bundling the threshold data; an inhabitation lemma supplies one concrete certificate. No forcing-chain or RCL argument is replayed here.

why it matters in Recognition Science

Anchors chemistry flash-point language on the same $J$-cost that T5 forces unique for the whole framework. Downstream chemistry or materials results that need a certified ignition or phase threshold in RS-native units are the intended consumers. The module currently has no recorded used-by edges, so it functions as a leaf definitional layer awaiting those parents.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)