module module

`IndisputableMonolith.CostUniqueness`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.CostAxioms module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.Convexity module_import
IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.CPM.LawOfExistence module_import
IndisputableMonolith.Foundation.ClosedObservableFramework module_import

declarations in this module (10)

theorem T5_uniqueness_complete L27
structure UniqueCostAxioms L116
lemma Jcost_continuous_pos L130
theorem Jcost_is_reciprocal L145
theorem Jcost_is_normalized L149
theorem Jcost_satisfies_composition_law L153
theorem Jcost_is_calibrated L157
theorem unique_cost_on_pos_from_rcl L167
theorem unique_cost_on_pos L194
def Jcost_regularity_cert L203