cert
plain-language theorem explainer
Packages three structural properties of the redox domain cost into one certificate: it vanishes at equal nonzero arguments, stays nonnegative for positive mass/energy, and the canonical threshold is positive. Anyone citing the φ-ladder construction of standard reduction potentials would point here. The body is a pure structure assembly of three sibling lemmas.
Claim. There is a redox-potential certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module builds a structural account of electrochemical reduction potentials on the Recognition Science φ-ladder. Empirically, aqueous standard potentials run from Li/Li⁺ (−3.04 V) to F₂/F⁻ (+2.87 V), a span of about 6 V. The module notes that φ⁵ ≈ 11.09 half-steps times a reference step ~0.543 V recovers that range.
The domain cost is the local J-cost specialization used for redox pairs (imported from the Cost layer). Recognition cost is forced nonnegative by the observer-forcing theorem: any recognition event has cost ≥ 0 because Jcost is nonnegative on positive states. Equilibrium is the diagonal of the domain cost, where the two arguments match.
RedoxPotentialCert is the bundle of the three algebraic facts needed before any ladder spacing or voltage comparison is stated: zero on the diagonal, global nonnegativity off it, and a positive threshold scale.
proof idea
Pure structure construction. The three fields of RedoxPotentialCert are filled by the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos. No extra tactics or arithmetic; the definition is the certificate.
why it matters
Closes the certificate layer of the redox-from-J-cost module (Plan v7, eighty-fourth pass), marked STRUCTURAL THEOREM with zero sorry and zero axioms. Downstream consumers (none yet wired in the graph) can assume a single inhabited cert rather than re-proving diagonal vanishing, cost positivity, and threshold positivity. In the broader RS chain this sits under the J-uniqueness / cost-nonnegativity strand (T5 and observer forcing): redox potentials are treated as cost differences on the φ-ladder, not as independent electrochemical postulates. The numerical 6 V span and the φ⁵ rung count remain interpretive context in the module doc; this declaration only locks the algebraic prerequisites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.