module module

`IndisputableMonolith.Foundation.CostFromDistinction`

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

declarations in this module (24)

class ConfigSpace L77
theorem join_emp L112
theorem independent_emp L117
theorem inconsistent_of_join_indep_right L122
structure CostFunction L147
theorem emp_cost_zero L164
theorem cost_pos_iff_inconsistent L169
theorem cost_zero_of_consistent L180
theorem cost_pos_of_inconsistent L185
theorem cost_ne_zero_of_inconsistent L190
theorem additive_three L202
theorem additive_strict_of_both_inconsistent L216
theorem additive_emp_left L231
theorem additive_emp_right L235
theorem uniqueness_on_indep_decomposition L258
theorem uniqueness_three_indep L275
theorem then L294
structure Calibration L299
theorem calibration_pos L317
theorem extension_to_consistent L324
theorem with L350
structure RecognitionWorkConstraintCert L359
def recognition_work_constraint_cert L380
theorem recognition_work_constraint_theorem L409