Pith. sign in
module module low

IndisputableMonolith.Chemistry.ESSolution5

show as:
view Lean formalization →

Certificate module for ES Solution 5 in the RS chemistry layer. It defines a domain cost, proves that cost is nonnegative, fixes a positive canonical threshold, and packages both into an inhabited certificate record. Chemistry audits that need a closed cost-threshold bundle cite this module. The argument is definitional scaffolding plus short nonnegativity and positivity lemmas over the imported cost calculus.

claimThe module supplies a domain cost $C$ with $C \ge 0$, a canonical threshold $\theta > 0$, and an inhabited certificate bundling these facts for ES Solution 5 in Recognition Science chemistry units (built from the RS cost $J$ and the constants module).

background

Recognition Science measures mismatch with the cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law. The Cost import exposes that calculus; Constants supplies the RS-native tick $\tau_0 = 1$ and related units ($c = 1$, $\hbar = \varphi^{-5}$, etc.).

Chemistry modules lift those primitives to domain-level costs and decision thresholds used when matching predicted ladders or shell structure against observation. This file is the ES Solution 5 slice of that layer: a named domain cost, its pointwise evaluation identity, nonnegativity, and a strictly positive canonical threshold.

The certificate record then freezes those facts into a single inhabitable object so downstream chemistry proofs can assume a closed cost-threshold package without re-deriving positivity.

proof idea

Definition-first module, not a deep derivation. It introduces the domain cost and the canonical threshold as defs, then discharges two short analytic obligations: nonnegativity of the domain cost (inherited from nonnegativity of $J$ and the Cost layer) and positivity of the threshold. Equality-at-evaluation is a definitional or one-line rewrite. The certificate type packages those lemmas; inhabitation is by direct construction from the proved fields. No long tactic scripts or external chemistry hypotheses appear in the sibling surface.

why it matters in Recognition Science

Gives the chemistry stack a named, closed certificate for ES Solution 5 so later shell, rung, or gap arguments can cite one object instead of re-proving cost nonnegativity and threshold positivity. No downstream used-by edges are recorded yet; the module sits as a leaf certificate in the chemistry domain, ready for mass-ladder or shell-matching parents that need a cost-threshold pair in RS-native units. It touches the Cost and Constants foundations (J-cost, $\tau_0$) without advancing the T0–T8 forcing chain itself. Open work is wiring this certificate into concrete ES Solution 5 comparison theorems once those parents land.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)