RedoxPotentialCert
plain-language theorem explainer
Certificate record bundling three properties of the redox domain cost: it vanishes on the equilibrium diagonal, stays non-negative for positive metal and electron arguments, and the canonical threshold is strictly positive. Cited by anyone assembling the φ-ladder reduction-potential span (Li/Li+ to F2/F−). Pure structural packaging with no proof body.
Claim. A redox-potential certificate is a record of three assertions: (i) the domain cost vanishes at equilibrium, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
The module builds a redox-potential ladder from the Recognition Science J-cost and the φ-ladder. Empirically, standard reduction potentials run from Li/Li+ (−3.04 V) to F2/F− (+2.87 V), a span of about 6 V, identified with φ^5 rung spacing times a reference energy (φ^5 ≈ 11.09 half-steps × 0.543 V ≈ 6 V).
The domain cost C(m,e) is the J-cost specialization used for metal/electron ratio pairs in this chemistry layer. Equilibrium means equal arguments: C(r,r) should be the J-minimum (zero). Non-negativity of recognition cost is the global RS fact that every recognition event has cost ≥ 0 (upstream cost_nonneg via Jcost_nonneg). The canonical threshold is the positive scale that sets the voltage rung height against which the φ-ladder is compared.
proof idea
No proof: this is a structure definition whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas carry the actual algebra (J-cost minimum on the diagonal, non-negativity for positive ratios, and positivity of the threshold constant).
why it matters
Gives a single named interface for the redox-from-J-cost story so downstream code can demand the three properties without restating them. The module’s cert builds a concrete inhabitant; cert_inhabited then records Nonempty RedoxPotentialCert, closing the structural theorem claim (0 sorry, 0 axiom) for this pass.
In the broader framework this sits under chemistry applications of the J-cost (T5 uniqueness of J) and the φ-ladder mass/energy spacing. The φ^5 factor matches the same Z_cf = φ^5 band used elsewhere in RS (constants and creation thresholds). It does not yet derive numerical half-cell voltages from first principles; it certifies the cost-theoretic scaffolding those voltages would sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.