recidivismCost_phi_step
plain-language theorem explainer
The result states that the J-cost function evaluated at the golden ratio equals phi minus 3/2. Researchers modeling recidivism rates through recognition costs cite this calibration when fixing the one-phi-step threshold for detectable rehabilitation effects. The proof is a direct reference to the pre-established evaluation of J at phi.
Claim. The J-cost function satisfies $J(φ) = φ - 3/2$, where $J$ is the recognition cost on the reoffense-to-baseline ratio and $φ$ is the golden ratio.
background
In this module recidivism is cast as a J-cost reading on the ratio r = reoffense_rate / baseline_rate. Equilibrium corresponds to r = 1 with J = 0; effective programs push r < 1 and raise J-cost above the recognition floor. The module doc states the RS prediction that the minimum detectable difference is J(φ) ≈ 0.118, a one-φ-step departure in the ratio.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_phi_val from the Constants module.
why it matters
This supplies the phi-step value to the RecidivismCert definition, which aggregates equilibrium, nonnegativity, reciprocal, and phi-step properties. It realizes the framework landmark that J(φ) supplies the recognition threshold for recidivism reduction. The result closes the structural theorem for the Criminal Justice module by providing the concrete calibration point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.