cert
plain-language theorem explainer
The definition assembles a SentencingCert record by supplying three theorems that establish the punishment-to-harm ratio exceeds one, adjacent severity ratios exceed two, and the sentencing cost vanishes when punishment equals harm. Jurisprudence researchers working in Recognition Science would cite the resulting certificate to assert proportionality bounds derived from the recognition quantum. It is assembled as a direct record of three sibling theorems.
Claim. Let $\phi$ be the golden ratio. The structure $\mathrm{SentencingCert}$ is realized by the record whose fields satisfy $1 < \phi$, $2 < \phi^2$, and $\forall p \in \mathbb{R} \setminus \{0\}, \ \mathrm{sentencingCost}(p,p)=0$.
background
The module develops sentencing proportionality from the J-cost function. J-cost obeys the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ and has fixed point $\phi$. SentencingCert is the structure requiring $1<$ proportionalityRatio, $2<$ adjacentSeverityRatio, and sentencingCost $p$ $p=0$ for $p\neq0$. The local setting states that proportionality (harm $\times$ culpability = punishment) is foundational in criminal justice, with RS predicting the optimal ratio equals $\phi$. Upstream, proportionalityRatio_gt_one reduces to one_lt_phi while adjacentSeverityRatio_gt_two reduces to phi_squared_bounds.1.
proof idea
The definition is a direct record constructor that populates the three fields of SentencingCert using the theorems proportionalityRatio_gt_one, adjacentSeverityRatio_gt_two, and sentencingCost_proportional.
why it matters
This certificate consolidates the proportionality results inside the jurisprudence module and supports the structural claim that the optimal punishment-to-harm ratio equals the recognition quantum $\phi$. It aligns with the phi-ladder and T5 J-uniqueness in the forcing chain. The module doc labels the entire development a structural theorem with zero axioms; no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.