IsLeastPowerCost
plain-language theorem explainer
Predicate on a natural number n: the n-th power is pointwise least-cost among all nondegenerate powers under the recognition cost J. Cited by anyone proving that only the unit exponent minimizes J on the full power family. Pure Prop definition; no proof content.
Claim. For $n \in \mathbb{N}$, the predicate holds iff for every $m \ge 1$ and every real $x > 0$ with $x \ne 1$, one has $J(x^n) \le J(x^m)$, where $J(t) = (t + t^{-1})/2 - 1$.
background
The recognition cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). It is the unique symmetric cost forced by the Recognition Composition Law, vanishes only at the identity ratio $x = 1$, and is strictly positive elsewhere.
This module isolates how the unit scale is selected by minimality of $J$ on power families. Exponent zero gives the zero cost identically, so nondegeneracy means competitors satisfy $m \ge 1$. A sibling predicate compared only odd exponents; the present definition drops the parity cut and orders against every positive integer power under the pointwise $J$-order.
proof idea
No proof body: the declaration is a Prop-valued definition. It packages the quantified statement "the $n$-power is least among nondegenerate powers under $J$" so downstream theorems can name the property without repeating the double quantification over $m$ and $x$.
why it matters
Direct input to the uniqueness theorem that the predicate holds if and only if $n = 1$, so the canonical (unit) exponent is the unique least nondegenerate member of the full power family, not merely the odd subfamily. Also used by the anchor equivalence: $J(b^n) = J(b)$ if and only if this leastness holds (for $b > 0$, $b \ne 1$, $n \ge 1$).
Together these close the unit-from-minimality argument for unrestricted powers. Framework landmark: T5 $J$-uniqueness; the same $J$ forced by the functional equation selects the unit scale by cost minimality on powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.