`ConsentInterfaceCert`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.ConsentInterfaceFromJCost on GitHub at line 78.

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

  75    IsConsensual sigma sigma sigma_max := by
  76  unfold IsConsensual; exact le_refl _
  77
  78structure ConsentInterfaceCert where
  79  value_at_opt : ∀ s : ℝ, s ≠ 0 → valueFunctional s s = 1
  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.