SentencingCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.