proportionalityRatio_gt_one
plain-language theorem explainer
The theorem establishes that the canonical punishment-to-harm ratio exceeds unity. Jurisprudence modelers using Recognition Science would cite it to fix the lower bound on scaled penalties. The proof is a one-line term application of the golden-ratio inequality.
Claim. $1 < r$, where $r$ is the canonical punishment-to-harm ratio defined as the golden ratio.
background
The module derives sentencing proportionality from J-cost, with the RS prediction that the optimal punishment-to-harm ratio equals the recognition quantum φ. proportionalityRatio is defined directly as phi. The upstream lemma one_lt_phi states that 1 < phi and is imported from Constants and PhiSupport, where it is proved via the standard quadratic inequality for the golden ratio.
proof idea
The proof is a term-mode one-liner that applies the one_lt_phi lemma from Constants.
why it matters
This supplies the ratio_gt_one field inside the SentencingCert definition, which packages the three core inequalities for the proportionality structure. It places the φ > 1 landmark from the forcing chain into the jurisprudence setting, confirming the departure from null cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.