`SentencingCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Jurisprudence.SentencingProportionalityFromJCost
domain: Jurisprudence
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Jurisprudence.SentencingProportionalityFromJCost on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  52    sentencingCost p p = 0 := by
  53  unfold sentencingCost; rw [div_self h]; exact Jcost_unit0
  54
  55structure SentencingCert where
  56  ratio_gt_one : 1 < proportionalityRatio
  57  adj_gt_two : (2 : ℝ) < adjacentSeverityRatio
  58  cost_proportional : ∀ p : ℝ, p ≠ 0 → sentencingCost p p = 0
  59
  60noncomputable def cert : SentencingCert where
  61  ratio_gt_one := proportionalityRatio_gt_one
  62  adj_gt_two := adjacentSeverityRatio_gt_two
  63  cost_proportional := sentencingCost_proportional
  64
  65theorem cert_inhabited : Nonempty SentencingCert := ⟨cert⟩
  66
  67end
  68end SentencingProportionalityFromJCost
  69end Jurisprudence
  70end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.