recidivismCost_reciprocal
plain-language theorem explainer
The theorem proves symmetry of recidivism cost under interchange of reoffense and baseline rates. Researchers modeling rehabilitation outcomes via J-cost on ratios would cite it to confirm invariance under inversion. The proof is a short tactic sequence that unfolds the definition, applies the J-cost reciprocal lemma to the positive ratio, and finishes with congruence plus field simplification.
Claim. Let $r, b > 0$. Then the recidivism cost, defined as the J-cost function applied to the ratio $r/b$, satisfies $J(r/b) = J(b/r)$.
background
The J-cost function on positive reals satisfies $J(x) = J(x^{-1})$, as recorded by the reciprocal lemma in the Cost module. Recidivism cost is defined as the J-cost of the ratio of reoffense rate to baseline rate. This module treats recidivism as a J-cost reading on the rehabilitation ratio, with pre-intervention equilibrium at ratio 1 giving zero cost and effective programs driving the ratio below 1.
proof idea
The proof unfolds the recidivism cost definition to reduce the claim to equality of J-cost on a ratio and its reciprocal. It applies the Jcost_reciprocal lemma to the positive ratio reoffense/baseline, then uses congruence and field simplification to identify the two sides.
why it matters
This supplies the reciprocal field required by the RecidivismCert structure defined later in the same module. It completes a structural requirement for the criminal-justice application of the J-cost framework, confirming the symmetry that follows from the recognition composition law. The module doc lists the recognition threshold at one phi-step as the falsifier for the broader model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.