cert
plain-language theorem explainer
Packages three elementary facts about the restorative domain cost into a single certificate: cost vanishes on equal ratios, cost is nonnegative for positive arguments, and the canonical threshold is positive. Anyone stating restorative-justice bounds in RS ethics cites this bundle. The body is pure structure assembly from three already-proved lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical restoration threshold is strictly positive.
background
The Ethics module formalizes restorative justice in Recognition Science: repair is complete when the J-cost of the ratio harm_repaired/harm_done vanishes, and partial restoration is acceptable when that cost stays below a fixed threshold tied to $\varphi$. Domain cost is the J-cost specialized to a pair of positive magnitudes (repaired vs done); it inherits nonnegativity from the global recognition cost $J$.
The structure RestorationJust4Cert is the interface that packages the three properties any such domain cost must satisfy before justice thresholds can be stated. Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J\ge 0$ on positive states. The canonical threshold is the positive cutoff (linked to $J(\varphi)$) separating acceptable partial repair from incomplete repair.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq (cost of equal nonzero ratios is zero), domainCost_nonneg (nonnegativity on positive pairs), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed; the def only witnesses that those three facts inhabit the certificate structure.
why it matters
Gives the Ethics module a single named certificate that restorative domain cost behaves as required by the session-3 structural theorem (0 sorry, 0 axiom). Downstream justice statements can assume one object rather than three separate lemmas. In the RS framework this sits under the J-cost uniqueness (T5) and the $\varphi$-threshold language of the primer: full repair is $J=0$, acceptable partial repair is $0<J<J(\varphi)$. No consumers are wired yet (used_by empty), so the certificate is presently the export surface of the ethics cost facts rather than an intermediate step in a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.