isLeastPower_iff_canonical
plain-language theorem explainer
For every natural exponent n at least 1, the power-n cost is pointwise least among all nondegenerate power costs if and only if n equals 1. Anyone citing uniqueness of the canonical unit cost over the full power family (not just odd exponents) uses this. The proof is a short constructor: the forward direction contradicts strict cheapness of the unit via jcost_lt_pow; the reverse applies that same strict inequality when the competitor exponent is at least 2.
Claim. Let $n\in\mathbb{N}$ with $n\ge 1$. Then $J(x^n)\le J(x^m)$ for every $m\ge 1$ and every $x>0$ with $x\ne 1$ if and only if $n=1$. (Here nondegeneracy means competitors satisfy $m\ge 1$, excluding the identically zero exponent-zero cost.)
background
The module selects the unit scale of the Recognition cost by a pure minimality principle on power families, without naming $J$ in the selection predicate. The cost $J$ (written Jcost in the development) is the unique nonnegative symmetric solution of the Recognition Composition Law; on ratios it is $J(x)=(x+x^{-1})/2-1$.
IsLeastPowerCost n asserts that the map $x\mapsto J(x^n)$ is a least element, under the pointwise order on $(0,\infty)\setminus{1}$, among all nondegenerate power costs $x\mapsto J(x^m)$ with $m\ge 1$. Exponent zero is excluded because it is the zero functional and would trivially undercut every positive cost.
The key upstream fact is jcost_lt_pow: for any base $x>0$, $x\ne 1$, and any exponent $n\ge 2$, one has the strict inequality $J(x)<J(x^n)$. That lemma removes the odd-parity restriction from the earlier odd-power comparison, which is exactly what the corrected full-power classification needs.
proof idea
Bidirectional constructor.
Forward: assume leastness at $n$ and $n\ne 1$. Then $n\ge 2$. Instantiate leastness at competitor $m=1$ and base $x=2$ to get $J(2^n)\le J(2)$. Rewrite $2^1=2$ and apply jcost_lt_pow at base 2 and exponent $n$ to obtain the strict reverse inequality, a contradiction.
Reverse: set $n=1$. For competitor $m$ and base $x$, rewrite $x^1=x$. If $m=1$, both sides agree. If $m\ge 2$, jcost_lt_pow supplies $J(x)<J(x^m)$, hence the weak inequality required by leastness.
why it matters
This is the full-power uniqueness statement that the canonical cost (exponent 1) is the unique least nondegenerate member of the power family. The doc-comment stresses that the condition never names $J$, so selection is purely order-theoretic.
It feeds anchor_is_minimality_over_powers, which equates the anchor identity $J(b^n)=J(b)$ with leastness over the whole nondegenerate family (parity restriction removed). It is also used by the discrete-versus-continuous gauge comparison and by the PRC ledger fact that the cube-generated native cost at two is not canonical.
In the broader framework this pins the unit of the T5 $J$-cost on the discrete gauge: minimality selects exponent 1 uniquely among powers, consistent with the forcing chain's uniqueness of $J$ and with the discrete eight-tick structure that continuous gauges cannot floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.