sentencingCost_proportional
plain-language theorem explainer
The result shows that the J-cost of a punishment-to-harm ratio equal to one is exactly zero. Jurisprudence modelers building proportionality axioms would cite it to anchor the null-cost baseline before introducing the recognition quantum φ as the optimal departure. The proof is a one-line wrapper that unfolds the sentencing cost definition, rewrites the ratio to one, and invokes the unit lemma for Jcost.
Claim. For any nonzero real $p$, the J-cost of the ratio of punishment $p$ to harm $p$ is zero: $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ and the sentencing cost is defined as the J-cost of the punishment-to-harm ratio.
background
The module formalizes sentencing proportionality inside Recognition Science by applying the J-cost function to the punishment/harm ratio. J-cost is given by $J(x) = (x-1)^2/(2x)$, which vanishes at unity and quantifies recognition defect. The sentencing cost is then obtained directly as $J$(punishment/harm). Upstream lemma Jcost_unit0 states $J(1) = 0$ by direct simplification of the squared-ratio expression. The module setting treats harm × culpability = punishment as foundational, with the RS prediction that the canonical just ratio equals the recognition quantum φ.
proof idea
The proof is a one-line wrapper. It unfolds sentencingCost to expose Jcost(punishment/harm), rewrites the ratio p/p to 1 via the nonzero hypothesis, and applies the lemma Jcost_unit0.
why it matters
This supplies the zero-cost case required by the downstream SentencingCert structure, which assembles the full set of proportionality statements (ratio > 1, adjacent severity ratio > 2, and cost proportionality). It completes the structural theorem of the module, linking the J-cost null point to the Recognition Science claim that the optimal punishment/harm ratio is φ. The module falsifier remains any corpus of ≥100 cases whose observed ratios lie consistently outside (1.0, 4.0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.