recidivismCost_at_equilibrium
plain-language theorem explainer
recidivismCost_at_equilibrium establishes that the J-cost on the reoffense-to-baseline ratio vanishes exactly when those rates are equal. Criminal justice modelers would cite it to fix the zero point of the equilibrium prediction. The proof is a one-line wrapper that unfolds the ratio definition and applies the Jcost unit lemma after division simplification.
Claim. For real $r$ with $r ≠ 0$, the recidivism cost at equal reoffense and baseline rates satisfies $J(r/r) = 0$, where $J$ is the J-cost function.
background
The module casts recidivism as J-cost on the ratio $r =$ reoffense rate over baseline rate. The sibling definition recidivismCost(reoffense, baseline) := Jcost(reoffense / baseline) encodes this reading directly. Upstream Jcost_unit0 states Jcost(1) = 0 and notes that J(x) is expressed as the squared ratio $(x-1)^2/(2x)$. The module doc fixes pre-intervention equilibrium at $r=1$, $J=0$, with rehabilitation pushing $r<1$.
proof idea
One-line wrapper. It unfolds recidivismCost to expose Jcost(r/r), rewrites the ratio to 1 via div_self under the hypothesis $r ≠ 0$, and concludes by exact application of the Jcost_unit0 lemma.
why it matters
The result supplies the cost_at_equilibrium field required by the downstream RecidivismCert structure. It anchors the module's structural claim that the recognition threshold for detectable recidivism reduction is the one-phi-step departure with J(phi) ≈ 0.118. The theorem closes the zero-cost equilibrium case inside the criminal-justice application of the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.