`cert`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethics.ConsentInterfaceFromJCost
domain: Ethics
line: 83 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.ConsentInterfaceFromJCost on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  80  sigma_pres_consensual : ∀ s s_max : ℝ, 0 < s → 0 < s_max →
  81    IsConsensual s s s_max
  82
  83noncomputable def cert : ConsentInterfaceCert where
  84  value_at_opt := valueFunctional_at_optimum
  85  sigma_pres_consensual := sigma_preserving_consensual
  86
  87theorem cert_inhabited : Nonempty ConsentInterfaceCert := ⟨cert⟩
  88
  89end
  90end ConsentInterfaceFromJCost
  91end Ethics
  92end IndisputableMonolith

papers checked against this theorem

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