module module

`IndisputableMonolith.Ethics.ConsentInterfaceFromJCost`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (9)

def valueFunctional L47
theorem valueFunctional_at_optimum L50
theorem valueFunctional_nonneg L54
def IsConsensual L60
theorem consensual_iff_jcost_nondecreasing L64
theorem sigma_preserving_consensual L73
structure ConsentInterfaceCert L78
def cert L83
theorem cert_inhabited L87