recidivismRateAtYear
plain-language theorem explainer
Recidivism rates under the Recognition Science model follow an exponential phi-decay on the recognition-restoration rung, with the rate at year k given directly by phi to the power of negative k. Criminologists extending Andrews-Bonta risk-domain analysis or RS theorists applying the phi-ladder to social restoration would cite this definition to ground positivity and monotonicity results. The declaration is a one-line noncomputable definition that encodes the RS prediction without further computation or proof obligations.
Claim. The recidivism rate at year $k$ is defined by $r(k) = phi^{-k}$, where $phi$ is the golden ratio and $k$ ranges over the natural numbers.
background
Recognition Science models criminal recidivism as following a phi-decay law on the recognition-restoration rung. Each year post-release the risk of reoffending decays by a factor of $1/phi$ when rehabilitation is effective. The module documentation cites the Andrews-Bonta meta-analysis with observed ratios near $1/phi$ and states the RS prediction that rates at year $k$ decay as $phi^{-k}$ from baseline. The five canonical risk domains (criminal history, antisocial cognition, antisocial associates, family/marital, school/work) are identified with configDim $D=5$.
proof idea
This is a direct one-line definition that sets recidivismRateAtYear k to phi raised to the power of minus k after casting the natural-number index to an integer for the exponentiation operator.
why it matters
This definition supplies the functional form required by the RecidivismCert structure and the two supporting theorems recidivismRate_pos and recidivismRate_decay. It realizes the RS prediction stated in the module documentation for recidivism rates on the phi-ladder, extending the self-similar fixed point of T6 to restoration processes. The declaration closes the criminology application without introducing new hypotheses or open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.