exponent_zero_charges_nothing
plain-language theorem explainer
For any real ratio x, the recognition cost of x to the zeroth power is identically zero. Unit-from-minimality arguments cite this to flag the degenerate exponent before imposing nondegeneracy. The proof reduces via x^0 = 1 to the elementary fact that J(1) = 0.
Claim. For every real number $x$, $J(x^{0}) = 0$, where $J(y) = \frac{y + y^{-1}}{2} - 1$ is the recognition cost functional.
background
The recognition cost is $J(x) = \frac{x + x^{-1}}{2} - 1$, the unique functional forced by the Recognition Composition Law (T5 J-uniqueness). It vanishes at the unit ratio: $J(1) = 0$.
This module studies selection of the unit by minimality among power costs $J(x^n)$. The zero exponent is degenerate in that family: $x^0 = 1$ for every $x$, so the cost is always zero independent of the underlying ratio.
Upstream, the unit identity $J(1) = 0$ is already a basic lemma on the cost functional; the present claim simply transports it to the power family.
proof idea
One-line term proof. Rewrite the natural-number power via the identity $x^0 = 1$, then apply the existing unit lemma $J(1) = 0$. No positivity hypothesis is needed.
why it matters
Immediate parent is the companion comparison: the zero-exponent cost is less than or equal to $J(x^n)$ for every natural $n$ and every positive $x$. That undercutting is cost-independent (it holds because the left side is zero), which is exactly why the module doc insists that selection needs nondegeneracy rather than leastness alone.
In the broader framework this sits under Cost after T5 has fixed $J$. It clears the degenerate member of the power family so later theorems can isolate the genuine unit $x^1$ by minimality among nondegenerate powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.