Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.OxidationReductionPotentialFromJCost

show as:
view Lean formalization →

Chemistry module that ties oxidation–reduction potential to the Recognition J-cost. It defines a domain cost on redox ratios, proves nonnegativity and equilibrium vanishing, and packages a canonical positive threshold into a RedoxPotentialCert. Electrochemists or RS chemists cite it when grounding half-cell scales in the same cost that forces φ and the forcing chain. The argument is definitional plus short algebraic lemmas from Cost and Constants.

claimOn redox concentration (or activity) ratios $x>0$, a domain cost $C(x)$ built from the J-cost satisfies $C\ge 0$, $C=0$ at equilibrium, and a canonical threshold $\theta>0$ marks the onset of a measurable potential. A certificate packages these facts as a inhabited redox-potential witness in RS-native units.

background

Recognition Science measures mismatch by the unique cost $J(x)=(x+x^{-1})/2-1$ fixed by the Recognition Composition Law and T5. Chemistry inherits that cost rather than inserting a separate Nernst prefactor by hand.

This module sits in the Chemistry domain and imports Constants (RS time quantum $\tau_0=1$ tick) and Cost (the J-cost API). Sibling objects introduce a domain cost on positive ratios, its value at equilibrium, nonnegativity, a canonical threshold with positivity, and a RedoxPotentialCert bundle with an inhabited certificate.

The local setting is therefore: treat oxidation–reduction imbalance as a positive real ratio, score it with J (or a monotone image of J), and read the electrochemical scale off the same cost geometry used for masses and coupling constants.

proof idea

Definition-heavy module with short supporting lemmas, not a deep tactic development. Domain cost is introduced as a Cost-derived functional on redox ratios; equilibrium vanishing and nonnegativity are immediate from J-properties ($J\ge 0$, $J(1)=0$). Canonical threshold is a positive constant (or φ-ladder expression) with a one-line positivity proof. The certificate structure packages those facts; inhabitation is by exhibiting the concrete threshold and the cost lemmas. No multi-step analytic PDE or continuum electrochemistry is proved here.

why it matters in Recognition Science

Gives chemistry a first-class hook into the same J-cost that drives T5–T8, so redox scales are not an external empirical add-on. Downstream used_by edges are empty in the current graph, so the module is a leaf certificate layer: it closes a chemistry interface rather than feeding a named parent theorem yet. In the broader RS program it is the natural place to later connect half-cell potentials to φ-ladder rungs, Berry threshold $\phi^{-1}$, and RS-native units ($c=1$, $\hbar=\phi^{-5}$). Referees should treat it as the formal bridge from Cost to oxidation–reduction language.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)