module module high

`IndisputableMonolith.Foundation.CostAxioms`

The CostAxioms module declares the core axioms that any cost functional must obey in Recognition Science. It encodes Normalization (vanishing at unity), the Composition Law, Calibration, and related properties of J. These feed directly into the T5 uniqueness theorem. The module organizes the declarative foundation without proofs.

claimAxioms for the cost functional: Normalization $J(1)=0$; Composition $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; Calibration and symmetry conditions on $J:\mathbb{R}_+\to\mathbb{R}$.

background

This module belongs to the Foundation domain and imports Cost, FunctionalEquation, and CostUniqueness. Normalization encodes that perfect balance (ratio = 1) has no cost. Upstream, FunctionalEquation supplies lemmas for the T5 cost uniqueness proof. CostUniqueness states: "Any cost functional F satisfying symmetry, unit normalization, strict convexity, and calibration must equal Jcost on ℝ₊." The setting is the axiomatization of J prior to deriving its explicit form from the forcing chain.

proof idea

This is a definition module, no proofs. It declares the axioms Normalization, Composition, Calibration, CostFunctionalAxioms together with J properties (symmetry, nonnegativity, zero iff unity) that are referenced by the uniqueness theorem.

why it matters in Recognition Science

The module supplies the axiomatic inputs for the T5 uniqueness theorem in CostUniqueness, which shows any qualifying functional equals Jcost. It fills the axiom slot supporting J-uniqueness (T5) in the forcing chain and the Recognition Composition Law.

scope and limits

Does not derive the explicit form of J.
Does not prove the axioms hold for any physical model.
Does not address extensions beyond the one-dimensional cost functional.
Does not contain the uniqueness proof itself.

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