cert
plain-language theorem explainer
Packages the three structural facts of RS forcing-chain module 4 into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive measure and expectation, and the canonical threshold is strictly positive. Anyone citing the J-cost minimum at equilibrium (ratio 1) uses this bundle. The definition is a pure structure inhabitant wiring three local lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 4 of the RS forcing chain treats the J-cost minimum: $J(1)=0$ at ratio one (equilibrium), with the side evaluation $J(\varphi)=\varphi-3/2$ at the golden ratio. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on pairs of positive reals (measure and expectation). The certificate structure demands three properties: cost vanishes when the two arguments agree and are nonzero; cost is nonnegative on the positive quadrant; and a fixed positive threshold (the canonical threshold) sits above zero.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity, and that the canonical identity event sits at the $J$-cost minimum $x=1$. The three field proofs in this module specialize that picture to domain cost and the module threshold.
proof idea
One-line structure inhabitant. Each field is filled by the matching local lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra algebra or case splits.
why it matters
This is the export handle for Foundation module 4: the J-cost minimum at equilibrium. It sits on the forcing-chain path toward T5 (J-uniqueness, $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Downstream consumers that need a single named witness for "cost is a true cost with a positive threshold" take this certificate rather than the three lemmas separately.
No used_by edges are recorded yet; the sibling cert_inhabited is the natural next step that turns the definition into an inhabited-type fact. The module doc marks the block as a closed structural theorem, so this definition is the packaging step, not an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.