cert
plain-language theorem explainer
The definition cert constructs the RecidivismCert record by populating its four fields with the equilibrium vanishing property, nonnegativity, reciprocity under ratio inversion, and the explicit value at phi. Researchers modeling recidivism reduction through J-cost on reoffense-to-baseline ratios would cite this record to invoke the complete structural package at once. It is a direct record construction that delegates each field to an upstream theorem without further reasoning.
Claim. Let recidivismCost(r, b) stand for Jcost(r/b). The definition cert supplies the RecidivismCert instance satisfying: for all r ≠ 0, recidivismCost(r, r) = 0; for all r, b > 0, recidivismCost(r, b) ≥ 0 and recidivismCost(r, b) = recidivismCost(b, r); and Jcost(φ) = φ − 3/2.
background
The module casts recidivism as a J-cost reading on the ratio r = reoffense rate over baseline rate. Equilibrium holds at r = 1 with zero cost; effective rehabilitation drives r < 1 and raises the recognition cost. recidivismCost is defined by applying Jcost to this ratio, inheriting nonnegativity, reciprocity, and the unit value at 1 from the J-cost axioms. The upstream theorems recidivismCost_at_equilibrium, recidivismCost_nonneg, recidivismCost_reciprocal, and recidivismCost_phi_step establish the four required properties by unfolding the definition and invoking Jcost_unit0, Jcost_nonneg, Jcost_reciprocal, and Jcost_phi_val respectively.
proof idea
This is a one-line record construction that assigns cost_at_equilibrium to recidivismCost_at_equilibrium, cost_nonneg to recidivismCost_nonneg, cost_reciprocal to recidivismCost_reciprocal, and phi_step to recidivismCost_phi_step. No tactics or additional lemmas are applied beyond these direct references.
why it matters
cert supplies the canonical RecidivismCert instance that realizes the structural theorem of the module, which predicts a recognition threshold of J(φ) ≈ 0.118 for detectable recidivism reduction. It closes the interface for the Criminal Justice domain by bundling the four properties without new hypotheses and connects to the Recognition Science forcing chain through the J-cost function and the phi-ladder. The module documentation states the falsifier as any large-N RCT showing recidivism reduction outside the one-φ-step J-cost band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.