EntropyProductionCert
plain-language theorem explainer
A certificate type packing three structural properties for irreversible entropy production from the J-cost: diagonal vanishing of the domain cost, nonnegativity on positive arguments, and positivity of the canonical recognition threshold. Anyone deriving sigma_irr = J(phi) F J / T or the RS Onsager coefficient L = J(phi) cites this bundle. It is a pure structure definition; inhabitance is supplied by the concrete cert instance.
Claim. An entropy-production certificate is a triple of facts: (i) the domain cost vanishes on equal nonzero arguments, $C(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive inputs, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical recognition threshold $\tau$ satisfies $\tau>0$.
background
The module treats irreversible entropy production in Recognition Science units: $\sigma_{\mathrm{irr}} = J(\phi), F, J / T$, with thermodynamic force $F$, flux $J$, and RS Onsager coefficient $L = J(\phi)$ evaluated at the recognition threshold. The underlying cost is the standard J-cost $J(x)=(x+x^{-1})/2-1$, forced unique by the T5 step of the forcing chain and nonnegative for $x>0$.
Here the domain cost $C(m,e)$ is the local two-argument cost used on thermodynamic pairs (mass-like and energy-like positives). The canonical threshold is the positive scale at which recognition events sit; upstream, cost_nonneg already records that every recognition event has nonnegative cost via $J$-nonnegativity. The certificate simply freezes the three inequalities the entropy-production argument needs as a single inhabitant type.
proof idea
No proof body: this is a structure definition whose three fields are Prop-valued requirements. Downstream, the noncomputable cert fills them by the sibling lemmas that establish diagonal vanishing of the domain cost, its nonnegativity on positive reals, and positivity of the canonical threshold. cert_inhabited then packages that instance as Nonempty.
why it matters
This is the structural gate for the Plan v7 entropy-production pass: without a single certificate type, later lemmas cannot uniformly assume diagonal vanishing, cost nonnegativity, and a positive threshold. It is inhabited by cert and exposed as nonempty by cert_inhabited, so any thermodynamic derivation in the module can assume the bundle rather than re-prove the three facts.
In the broader framework it ties the T5 J-uniqueness / J-nonnegativity story to continuum thermodynamics: the same cost that forces $\phi$ and the eight-tick octave supplies the nonnegative generator of irreversible entropy, with $L=J(\phi)$ at threshold. It does not close open dynamical questions (explicit Onsager matrix, fluctuation theorems); it only locks the cost-side hypotheses those results will need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.