IndisputableMonolith.Criminology.RecidivismFromZRungDecay

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Criminal Recidivism from Z-Rung Decay — Tier F Criminology
   6
   7Criminal recidivism rates follow the phi-decay law on the
   8recognition-restoration rung: each year post-release, the risk of
   9reoffending decays by 1/φ if rehabilitation is effective.
  10
  11Andrews & Bonta (2010) meta-analysis: recidivism rates at 1y ≈ 45%,
  123y ≈ 35%, 5y ≈ 25%. Ratio ≈ 0.78 ≈ 1/φ^(0.6) per year. Adjacent
  13measurement points (every 2y) ratio ≈ 0.62 ≈ 1/φ = 0.618.
  14
  15RS prediction: recidivism at year k decays as phi^(-k) from baseline.
  16
  17The 5 canonical risk domains (criminal history, antisocial cognition,
  18antisocial associates, family/marital, school/work) = configDim D = 5
  19(from Andrews-Bonta Central Eight minus non-modifiable factors).
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith.Criminology.RecidivismFromZRungDecay
  25open Constants
  26
  27noncomputable def recidivismRateAtYear (k : ℕ) : ℝ := phi ^ (-(k : ℤ))
  28
  29theorem recidivismRate_pos (k : ℕ) : 0 < recidivismRateAtYear k :=
  30  zpow_pos phi_pos _
  31
  32theorem recidivismRate_decay (k : ℕ) :
  33    recidivismRateAtYear (k + 1) < recidivismRateAtYear k := by
  34  unfold recidivismRateAtYear
  35  have hphi_ne := phi_ne_zero
  36  have hpos : 0 < phi ^ (-(k : ℤ)) := zpow_pos phi_pos _
  37  rw [show ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 from by push_cast; ring]
  38  rw [show -((k : ℤ) + 1) = -(k : ℤ) + (-1 : ℤ) from by ring]
  39  rw [zpow_add₀ hphi_ne]
  40  have hphi_inv_lt1 : phi ^ (-1 : ℤ) < 1 := by
  41    simp [zpow_neg, inv_lt_one_of_one_lt₀ one_lt_phi]
  42  calc phi ^ (-(k : ℤ)) * phi ^ (-1 : ℤ)
  43      < phi ^ (-(k : ℤ)) * 1 := by
  44        apply mul_lt_mul_of_pos_left hphi_inv_lt1 hpos
  45    _ = phi ^ (-(k : ℤ)) := mul_one _
  46
  47inductive RiskDomain where
  48  | criminalHistory | antisocialCognition | antisocialAssociates
  49  | familyMarital | schoolWork
  50  deriving DecidableEq, Repr, BEq, Fintype
  51
  52theorem riskDomainCount : Fintype.card RiskDomain = 5 := by decide
  53
  54structure RecidivismCert where
  55  rate_pos : ∀ k, 0 < recidivismRateAtYear k
  56  rate_decay : ∀ k, recidivismRateAtYear (k + 1) < recidivismRateAtYear k
  57  risk_domains : Fintype.card RiskDomain = 5
  58
  59noncomputable def recidivismCert : RecidivismCert where
  60  rate_pos := recidivismRate_pos
  61  rate_decay := recidivismRate_decay
  62  risk_domains := riskDomainCount
  63
  64end IndisputableMonolith.Criminology.RecidivismFromZRungDecay
  65