recidivismCost
plain-language theorem explainer
The definition assigns the recidivism cost to the J-cost of the ratio of reoffense rate to baseline rate. Criminologists modeling rehabilitation outcomes cite it when mapping rate changes onto the recognition-cost floor. The construction is a direct one-line application of the J-cost function to the input ratio.
Claim. Define the recidivism cost by $J(r/b)$ where $r$ denotes the reoffense rate, $b$ the baseline rate, and $J$ is the J-cost function satisfying $J(1)=0$ and $J(x)=J(1/x)$.
background
J-cost is the function $J(x)=(x+x^{-1})/2-1$ (equivalently cosh(log x)-1) that measures departure from unity on a positive real ratio. The module casts recidivism as a J-cost reading on the ratio $r=$ reoffense_rate / baseline_rate. Pre-intervention equilibrium is $r=1$, $J=0$; effective programs drive $r<1$ and raise the cost above the recognition floor. The RS prediction states that the minimum detectable recidivism reduction occurs at a one-phi-step departure with $J(phi)approx0.118$.
proof idea
One-line definition that applies the J-cost function directly to the ratio of the two input rates.
why it matters
The definition supplies the cost term used by the RecidivismCert structure to certify equilibrium zero, non-negativity, reciprocity, and the phi-step value. It implements the module's structural claim that recidivism reduction is a J-cost reading on the rehabilitation ratio, linking to T5 J-uniqueness and the phi-ladder. The module supplies an explicit falsifier: any large-N RCT showing recidivism reduction outside the J-cost band at one-phi-step departure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.