recidivismCost_nonneg
plain-language theorem explainer
The declaration shows that the J-cost of the recidivism ratio (reoffense rate divided by baseline rate) is non-negative for any positive rates. Modelers of rehabilitation interventions within the Recognition Science framework cite it to anchor the cost floor at equilibrium. The proof is a one-line wrapper that unfolds the definition and invokes the general J-cost non-negativity lemma on the positive ratio.
Claim. Let $r > 0$ and $b > 0$ be real numbers. Then $0 ≤ J(r/b)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
In the CriminalJustice.RecidivismFromJCost module recidivism is represented as the J-cost of the ratio $r = $ reoffense_rate / baseline_rate. The J-cost function satisfies $J(x) ≥ 0$ for $x > 0$ with equality precisely at $x = 1$, which corresponds to pre-intervention equilibrium. The module imports the general non-negativity result from IndisputableMonolith.Cost.Jcost_nonneg, whose doc-comment states “J(x) ≥ 0 for positive x (AM-GM inequality)” and whose proof reduces the expression to a square over a positive denominator.
proof idea
The proof is a one-line wrapper: it unfolds recidivismCost to Jcost (reoffense / baseline) and applies the lemma Jcost_nonneg to the strictly positive ratio produced by div_pos hr hb.
why it matters
This supplies the cost_nonneg field of the RecidivismCert structure defined later in the same module. It closes the non-negativity requirement for the J-cost representation in the criminal-justice domain, consistent with the same property used in Gravity.CoherenceCollapse, NavierStokes.PhiLadderCutoff and EnergyProcessingBridge. The module doc-comment identifies the recognition threshold J(φ) ≈ 0.118 as the minimum detectable one-φ-step departure from equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.