exponent_zero_undercuts_everything
plain-language theorem explainer
For every natural exponent n and every positive real base x, the recognition cost of the zeroth power is at most the cost of the nth power. Anyone arguing that the unit ratio is the unique cheapest gauge member cites this comparison. The proof rewrites the left side to zero via the zero-exponent identity, then applies nonnegativity of J.
Claim. For every $n \in \mathbb{N}$ and every $x > 0$, $J(x^{0}) \le J(x^{n})$, where $J(t) = (t + t^{-1})/2 - 1$ is the recognition cost on positive reals.
background
The recognition cost is $J(x) = (x + x^{-1})/2 - 1$ on $x > 0$. By AM-GM it is nonnegative, and it vanishes exactly at the unit ratio $x = 1$. The module UnitFromMinimality treats the unit as a selection principle: among discrete power gauges, the cheapest cost pins the canonical member rather than an arbitrary numeric anchor.
A sibling fact, exponent_zero_charges_nothing, records that $J(x^{0}) = 0$ for $x > 0$, since $x^{0} = 1$. Nonnegativity of $J$ on positive arguments is the standard lemma Jcost_nonneg. Together they give a uniform lower bound: the zero-power cost undercuts every natural power cost.
This sits inside the cost-functional side of Recognition Science, where the T5 uniqueness of $J$ (equivalently $\cosh(\log x) - 1$) and the Recognition Composition Law fix the shape of admissible costs before gauge classification begins.
proof idea
Term-mode, two steps. First rewrite the left-hand side by exponent_zero_charges_nothing, which replaces $J(x^{0})$ by $0$. The goal is then $0 \le J(x^{n})$. Apply Jcost_nonneg to the positive argument $x^{n}$, whose positivity is pow_pos from $x > 0$. No functional equation or uniqueness input is needed.
why it matters
This is the floor comparison that makes the unit the cheapest discrete gauge member. Downstream, discrete_gauge_has_a_floor_and_continuous_gauge_does_not packages the discrete side (strict cheapest among odd powers) against the continuum (halving always undercuts), and quotes the module's claim that least cost selects on the countable carrier but not on the real line.
It also feeds GaugeOrbitClassification.nontrivial_is_signedPower, which identifies the nondegenerate branch as a sign-extended power cost once SansAnchor hypotheses and a nontrivial rational trace are in force. In the surrounding narrative, the structural ledger's anchor $J(2) = 1/4$ is shown to cut the gauge family at the same place as minimality, so the anchor is the cheapest-cost condition written at one point, not an arbitrary convention. That is the local link to T5 J-uniqueness and the forced canonical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.