IndisputableMonolith.CriminalJustice.RecidivismFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Recidivism Rate from J-Cost on Rehabilitation Ratio
   7(Plan v7 fifty-first execution pass — first Criminal Justice module)
   8
   9## Status: STRUCTURAL THEOREM (0 sorry, 0 axiom).
  10
  11Cast recidivism as a J-cost reading on the ratio
  12`r = reoffense_rate / baseline_rate`.
  13
  14Pre-intervention equilibrium corresponds to `r = 1`, `J = 0`.
  15Effective rehabilitation programs push `r < 1` (below baseline),
  16increasing J-cost and restoring the recognition-cost floor.
  17
  18The RS prediction: the minimum detectable difference in recidivism
  19reduction (the "recognition threshold") is `J(φ) ≈ 0.118` —
  20a one-φ-step departure in the reoffense ratio.
  21
  22## Falsifier
  23
  24Any large-N randomized controlled trial (e.g., cognitive-behavioral
  25therapy in US Bureau of Justice Statistics) showing recidivism
  26reduction outside the J-cost band at one-φ-step departure.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace CriminalJustice
  31namespace RecidivismFromJCost
  32
  33open Constants
  34open Cost
  35
  36noncomputable section
  37
  38/-- J-cost on the recidivism ratio (reoffense_rate / baseline_rate). -/
  39def recidivismCost (reoffense baseline : ℝ) : ℝ :=
  40  Jcost (reoffense / baseline)
  41
  42theorem recidivismCost_at_equilibrium (r : ℝ) (h : r ≠ 0) :
  43    recidivismCost r r = 0 := by
  44  unfold recidivismCost; rw [div_self h]; exact Jcost_unit0
  45
  46theorem recidivismCost_nonneg (reoffense baseline : ℝ)
  47    (hr : 0 < reoffense) (hb : 0 < baseline) :
  48    0 ≤ recidivismCost reoffense baseline := by
  49  unfold recidivismCost; exact Jcost_nonneg (div_pos hr hb)
  50
  51theorem recidivismCost_reciprocal (reoffense baseline : ℝ)
  52    (hr : 0 < reoffense) (hb : 0 < baseline) :
  53    recidivismCost reoffense baseline = recidivismCost baseline reoffense := by
  54  unfold recidivismCost
  55  have h : Jcost (reoffense / baseline) = Jcost (baseline / reoffense) := by
  56    rw [Jcost_reciprocal (div_pos hr hb)]
  57    congr 1; field_simp [hb.ne', hr.ne']
  58  exact h
  59
  60theorem recidivismCost_phi_step :
  61    Jcost phi = phi - 3 / 2 := by
  62  exact Jcost_phi_val
  63
  64structure RecidivismCert where
  65  cost_at_equilibrium : ∀ r : ℝ, r ≠ 0 → recidivismCost r r = 0
  66  cost_nonneg : ∀ r b : ℝ, 0 < r → 0 < b → 0 ≤ recidivismCost r b
  67  cost_reciprocal : ∀ r b : ℝ, 0 < r → 0 < b →
  68    recidivismCost r b = recidivismCost b r
  69  phi_step : Jcost phi = phi - 3 / 2
  70
  71noncomputable def cert : RecidivismCert where
  72  cost_at_equilibrium := recidivismCost_at_equilibrium
  73  cost_nonneg := recidivismCost_nonneg
  74  cost_reciprocal := recidivismCost_reciprocal
  75  phi_step := recidivismCost_phi_step
  76
  77theorem cert_inhabited : Nonempty RecidivismCert := ⟨cert⟩
  78
  79end
  80end RecidivismFromJCost
  81end CriminalJustice
  82end IndisputableMonolith
  83