module module moderate

`IndisputableMonolith.Cost.UnitFromMinimality`

J-cost is inversion-blind, so gauge and minimality statements reduce to bases above one. The module shows the unit is uniquely selected by minimality of J among integer powers and among odd powers, with real-exponent forms for the continuum half of T5. Cite it when arguing that cost minimality forces the canonical unit in Recognition cost theory. Arguments are elementary comparisons from the closed form of J and power monotonicity.

claimThe Recognition cost satisfies $J(x^{-1})=J(x)$. For bases $x>1$, $J(x^r)$ is strictly monotone in the positive real exponent $r$ (and likewise for integer and odd powers). The unit base is therefore the unique minimizer of $J$ on the power orbit and on the odd-power orbit; least-cost predicates are equivalent to the canonical unit choice.

background

Recognition cost theory centers on the unique nonnegative cost $J$ fixed by T5, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The Recognition Composition Law and the functional-equation helpers in Cost.FunctionalEquation pin this $J$ as the unique solution of the T5 axioms.

Because $J(x^{-1})=J(x)$, any gauge or comparison statement about bases may be reduced to the half-line $x>1$. The continuum half of the uniqueness argument needs real exponents, so the module states power comparisons for real $r$ as well as for integer and odd integer powers.

Local predicates such as least odd-power cost and least power cost package the claim that the unit is the unique minimizer of $J$ on the corresponding orbit; equivalence lemmas identify those predicates with the canonical unit.

proof idea

The module is a short lemma pack, not a single theorem. Inversion identities for $J$ on real and integer powers reduce all comparisons to bases above one. Strict inequalities $J(x)<J(x^n)$ (and the odd-power and real-exponent analogues) follow from the closed form of $J$ and elementary monotonicity for $x>1$.

Least-cost predicates are then defined, and equivalence lemmas rewrite "is a least-cost base on the orbit" as "is the canonical unit." The two headline results are the unit-selection statements: minimality of $J$ on odd powers, and on all integer powers, forces the unit.

why it matters in Recognition Science

T5 forces a unique cost $J$. Once $J$ is unique, one still needs that the dimensionless unit is the unique cost minimizer on natural power orbits; otherwise a free gauge choice would remain in the cost calculus. This module closes that gap with explicit minimality and equivalence lemmas.

Downstream it is imported by the cost-unit axiom audit script, which checks that unit selection is derived rather than postulated. In the broader forcing chain it supports the T5 uniqueness package and the passage from the functional equation to a rigid, unit-normalized cost used by later rungs (mass ladder, $\alpha$ band, eight-tick bookkeeping).

scope and limits

Does not re-prove T5 uniqueness of $J$; assumes the cost module's $J$.
Does not treat complex bases or non-power orbits.
Does not derive physical constants or the mass ladder from unit selection.
Does not address discrete tick structure beyond power comparisons.
Real-exponent inequalities are for the continuum half only, not a full dynamical model.

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