module module moderate

`IndisputableMonolith.Cost.UnitFromMinimality`

The module proves that the multiplicative unit is uniquely selected by minimality of the J-cost among real powers and among odd integer powers. Anyone citing T5 uniqueness or the cost-gauge reduction to bases greater than one needs these lemmas. Arguments rest on J being blind to inversion together with strict increase of J on (1,∞).

claimIf $J(x)=(x+x^{-1})/2-1$, then $J(x^r)=J(x^{-r})$ for real $r$, so gauge statements reduce to bases $x>1$. Among odd powers (resp. all integer powers) of a fixed base $x\neq 1$, the least $J$-cost is attained exactly at the unit exponent, i.e. at $x^{\pm 1}$ in the canonical normalization.

background

Recognition Science forces a unique symmetric cost $J$ on $\mathbb{R}_{>0}$ via the Recognition Composition Law and T5 uniqueness: $J(x)=\cosh(\log x)-1=(x+x^{-1})/2-1$. The cost vanishes only at the multiplicative unit and is strictly increasing on $[1,\infty)$.

Because $J(x)=J(x^{-1})$, any comparison of costs of powers is invariant under inverting the base. The continuum half of the forcing chain therefore only needs statements for bases strictly above one and for real exponents. The parent Cost and FunctionalEquation modules supply the algebraic identities for $J$ used here.

The module packages two parallel minimality packages: one for odd integer powers (natural in discrete octave/tick settings) and one for general integer powers, each with a predicate for least cost and an iff linking that predicate to the canonical unit representative.

proof idea

Inversion identities jcost_rpow_inv / jcost_pow_inv are immediate from $J(x)=J(x^{-1})$ and functoriality of real/integer powers. Strict inequalities jcost_lt_odd_power and jcost_lt_pow (and their of_one_lt variants) reduce to monotonicity of $J$ on $(1,\infty)$ after folding exponents into the base via inversion blindness.

The selection theorems unit_is_selected_by_minimality and unit_is_selected_by_minimality_over_powers assemble those inequalities into a least-element claim. The predicates IsLeastOddPowerCost / IsLeastPowerCost and the iff lemmas isLeast_iff_canonical / isLeastPower_iff_canonical merely rephrase that least element as the canonical unit gauge.

why it matters in Recognition Science

T5 forces $J$ uniquely; this module turns that uniqueness into a gauge-fixing principle: the multiplicative unit is the unique cost-minimizer among powers. Downstream, scripts.cost_unit_axiom_audit imports the module to audit that the unit-cost axiom is not an extra assumption but a consequence of minimality.

In the broader forcing chain the result supports the reduction steps that treat only $x>1$ and that identify the self-similar fixed point $\varphi$ without redundant inverse copies. It is local Cost infrastructure rather than a named T0–T8 landmark, but every later mass-ladder or eight-tick argument that normalizes to unit cost sits on this selection fact.

scope and limits

Does not re-prove T5 uniqueness of J; assumes the standard J-cost from Cost.
Does not treat non-power families or continuous one-parameter subgroups beyond real powers of a fixed base.
Does not select units in dimensionful physical constants; only multiplicative real bases.
Does not address bases in (0,1) except via the inversion reduction already built in.

used by (1)

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

scripts.cost_unit_axiom_audit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (24)

lemma jcost_rpow_inv L59
lemma jcost_pow_inv L66
lemma jcost_lt_odd_power_of_one_lt L75
theorem jcost_lt_odd_power L89
theorem unit_is_selected_by_minimality L101
def IsLeastOddPowerCost L114
theorem isLeast_iff_canonical L121
lemma jcost_lt_pow_of_one_lt L157
theorem jcost_lt_pow L170
theorem unit_is_selected_by_minimality_over_powers L179
def IsLeastPowerCost L186
theorem isLeastPower_iff_canonical L191
theorem exponent_zero_charges_nothing L213
theorem exponent_zero_undercuts_everything L217
theorem anchor_iff_canonical L234
theorem anchor_is_minimality L252
theorem anchorPower_iff_canonical L258
theorem anchor_is_minimality_over_powers L271
theorem cost_of_the_first_distinction L280
lemma gauge_halving_is_cheaper_of_one_lt L286
theorem no_least_gauge_member L299
theorem gauge_tendsto_zero L311
theorem zero_cost_is_admissible L329
theorem discrete_gauge_has_a_floor_and_continuous_gauge_does_not L349