pith. sign in
module module moderate

IndisputableMonolith.CriminalJustice.RecidivismFromJCost

show as:
view Lean formalization →

The module applies the J-cost function to the recidivism ratio defined as reoffense rate over baseline rate. Criminal justice researchers working inside the Recognition Science framework would cite it when modeling reoffense costs. The module supplies the core definition together with elementary properties such as nonnegativity and equilibrium behavior.

claimRecidivism cost is given by $J(r/b)$ where $r$ is the reoffense rate, $b$ the baseline rate, and $J(x)=(x+x^{-1})/2-1$.

background

Recognition Science obtains the J function from the forcing chain T5 and the Recognition Composition Law. The imported Constants module fixes the native time unit at $ au_0=1$ tick. The Cost module supplies the general J-cost construction that this module specializes to the ratio of reoffense to baseline rates.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the recidivism-specific cost object used by the CriminalJustice domain. It feeds downstream properties such as equilibrium values and nonnegativity that appear in the sibling declarations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)