cert_inhabited
plain-language theorem explainer
The declaration shows that a SentencingCert structure exists, packaging the three proportionality conditions on sentencing ratios and cost derived from J-cost. Jurisprudence researchers applying Recognition Science would cite it to confirm consistency of the predicted φ-based scaling. The proof is a one-line term that witnesses Nonempty SentencingCert directly from the explicit cert construction.
Claim. There exists a structure $C$ such that $1 < r(C)$, $2 < a(C)$, and for all $p : ℝ$ with $p ≠ 0$ one has $s(p, p) = 0$, where $r$ is the proportionality ratio, $a$ the adjacent severity ratio, and $s$ the sentencing cost function.
background
The module applies the J-cost framework of Recognition Science to criminal sentencing, predicting that the optimal punishment-to-harm ratio equals the golden ratio φ. SentencingCert is the structure whose fields record the three required properties: the proportionality ratio exceeds 1, the adjacent severity ratio exceeds 2, and the sentencing cost vanishes on the diagonal for nonzero inputs. The upstream result is precisely this structure definition, which encodes the RS-derived axioms without additional hypotheses.
proof idea
The proof is a one-line term that constructs an element of Nonempty SentencingCert by applying the Nonempty constructor to the cert witness defined earlier in the module.
why it matters
This theorem closes the structural theorem for the module by establishing that the J-cost proportionality conditions are satisfiable, supporting the RS claim that sentencing scales with φ. It sits inside the broader forcing chain that derives constants and dimensions from the single functional equation, and the module documentation identifies the falsifier as any corpus of cases whose punishment/harm ratios fall outside (1.0, 4.0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.