module module high

`IndisputableMonolith.Foundation.CostAxioms`

The CostAxioms module sets the axiomatic base for the cost functional J on positive reals, beginning with normalization at unity. Researchers proving uniqueness for J or deriving the phi-ladder constants cite it to fix the reference point where perfect balance incurs zero cost. The module consists of definitions and axiom statements with no internal proofs, directly enabling the T5 result in CostUniqueness.

claimThe cost functional satisfies normalization $J(1)=0$, symmetry $J(x)=J(x^{-1})$, and the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ for all $x,y>0$.

background

This module resides in the Foundation layer and imports the basic Cost definitions, FunctionalEquation helpers for T5, and the main uniqueness theorem from CostUniqueness. Normalization encodes that any deviation-measuring cost must vanish at the reference ratio of unity, corresponding to perfect balance. The setting is the single functional equation whose solutions yield all physics, with J as the unique cost obeying symmetry, convexity, and calibration.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These axioms supply the hypotheses for the main theorem in CostUniqueness: any cost functional F satisfying symmetry, unit normalization, strict convexity, and calibration equals Jcost on positive reals. The module therefore anchors T5 J-uniqueness in the forcing chain, allowing phi to emerge as the self-similar fixed point and subsequent derivations of constants such as hbar = phi^{-5} and G = phi^5 / pi.

scope and limits

Does not derive phi or the eight-tick octave.
Does not address mass formulas or Berry thresholds.
Does not calibrate to the alpha band (137.03, 137.04).
Does not prove existence or uniqueness of J.

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