module module

`IndisputableMonolith.Foundation.CostAxioms`

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 (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.CostUniqueness module_import

declarations in this module (19)

class Normalization L58
class Composition L68
class Calibration L78
class CostFunctionalAxioms L82
def J L91
lemma J_eq_Jcost L94
theorem J_symmetric L138
theorem J_nonneg L145
theorem J_eq_zero_iff L152
theorem J_arbitrarily_large_near_zero L174
theorem J_tendsto_atTop_as_x_to_zero L211
def Exists L229
theorem law_of_existence L232
theorem unity_is_unique_existent L236
theorem mp_from_cost L254
theorem nothing_costs_infinity L259
theorem Composition_implies_CoshAddIdentity L272
theorem Composition_Normalization_implies_symmetry L301
theorem uniqueness_specification L337