SentencingCert
SentencingCert packages three properties that certify proportionality in sentencing under the J-cost model: the punishment-to-harm ratio exceeds 1, the adjacent severity ratio exceeds 2, and the cost is zero when punishment equals harm. A legal theorist or philosopher of law working in Recognition Science would cite it to formalize the harm-by-culpability principle as a zero-cost fixed point at unity ratio. The definition is a plain record type whose fields are supplied directly by the three sibling lemmas on phi and Jcost.
claimA certificate structure asserting that the canonical punishment-to-harm ratio satisfies $1 < phi$, the adjacent severity ratio satisfies $2 < phi^2$, and the J-cost of equal punishment and harm vanishes: for all nonzero real $p$, $J(p/p) = 0$, where $J$ denotes the J-cost function.
background
In this module proportionalityRatio is defined as phi, the self-similar fixed point forced by the recognition chain. adjacentSeverityRatio is defined as phi squared. sentencingCost(punishment, harm) is defined as Jcost applied to the ratio punishment/harm. The module develops sentencing proportionality from J-cost, predicting that the optimal punishment-to-harm ratio is phi, representing the canonical just departure from the null cost of no punishment. Evidence cited includes multiplicative scaling in US Federal Sentencing Guidelines and UK Sentencing Council guidelines, where adjacent severity ratios lie near 2-3, consistent with phi squared approximately 2.618.
proof idea
As a structure definition the construction is a direct record whose three fields are supplied by the sibling definitions proportionalityRatio, adjacentSeverityRatio, and sentencingCost together with their supporting lemmas. No tactics or reductions are required beyond the record constructor.
why it matters in Recognition Science
This structure is instantiated by the downstream cert definition and shown inhabited by cert_inhabited. It realizes the structural theorem for sentencing proportionality from J-cost, linking the J-cost zero at unity ratio to the phi-based departure in punishment scales. It touches the Recognition Science prediction that the just ratio is phi, with the module falsifier being any comparative sentencing study showing the punishment/harm ratio consistently outside (1.0, 4.0) across a corpus of at least 100 cases.
scope and limits
- Does not establish the numerical value of phi from first principles.
- Does not prove the inequalities 1 < phi or 2 < phi squared.
- Does not apply to non-real punishment or harm values.
- Does not address empirical validation against actual sentencing data.
Lean usage
noncomputable def cert : SentencingCert where ratio_gt_one := proportionalityRatio_gt_one adj_gt_two := adjacentSeverityRatio_gt_two cost_proportional := sentencingCost_proportionalformal statement (Lean)
55structure SentencingCert where
56 ratio_gt_one : 1 < proportionalityRatio
57 adj_gt_two : (2 : ℝ) < adjacentSeverityRatio
58 cost_proportional : ∀ p : ℝ, p ≠ 0 → sentencingCost p p = 0
59