RecidivismCert
plain-language theorem explainer
The RecidivismCert structure certifies four properties of the recidivism cost function, defined as J-cost on the reoffense-to-baseline ratio: zero value at equal rates, non-negativity for positive arguments, symmetry under rate swap, and the explicit value J(phi) = phi - 3/2. Recognition theorists modeling intervention thresholds in criminal justice data would cite it when linking recidivism reduction to the one-phi-step recognition threshold. The declaration is a structure definition that aggregates these properties directly from sibling cost-
Claim. A structure asserting that the recidivism cost function $c(r,b) := J(r/b)$ satisfies $c(r,r)=0$ for all $r≠0$, $c(r,b)≥0$ whenever $r>0$ and $b>0$, $c(r,b)=c(b,r)$ for positive $r,b$, and $J(φ)=φ-3/2$.
background
In this module recidivism is cast as a J-cost reading on the ratio $r=$ reoffense_rate / baseline_rate. The supporting definition recidivismCost(reoffense, baseline) expands to Jcost(reoffense / baseline), where Jcost is the standard Recognition Science cost function. The structure reuses the upstream non-negativity theorem cost_nonneg from ObserverForcing, which states that the cost of any recognition event is non-negative, and mirrors the RecidivismCert structure appearing in the Criminology.RecidivismFromZRungDecay module.
proof idea
This is a structure definition with no proof body. It collects four field properties of recidivismCost, each supplied by a sibling lemma: recidivismCost_at_equilibrium populates the zero-at-equilibrium clause, recidivismCost_nonneg supplies non-negativity, recidivismCost_reciprocal supplies symmetry, and recidivismCost_phi_step supplies the golden-ratio evaluation. The non-negativity field directly invokes the upstream cost_nonneg theorem.
why it matters
RecidivismCert supplies the type for the concrete instance cert and the inhabitedness theorem cert_inhabited constructed in the same file. It is mirrored by the RecidivismCert structure in Criminology.RecidivismFromZRungDecay, which encodes rate positivity, monotonic decay, and five risk domains instead. The structure encodes the Recognition Science prediction that the minimum detectable recidivism reduction occurs at the one-phi-step departure with J(φ) ≈ 0.118, consistent with the forcing-chain landmarks T5–T8 and the J-uniqueness property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.