IsLeastOddPowerCost
plain-language theorem explainer
Predicate saying the odd-power gauge member of index k is pointwise least-cost among all odd powers of the recognition cost J, at every positive ratio other than the unit. Used to pin the canonical member (k=0) as the unique least element of that family, and to equate anchor conditions with minimality. Pure Prop definition: packages a universal inequality, no proof content.
Claim. For $k\in\mathbb{N}$, the $k$-th odd-power gauge member is least-cost when $\forall j\in\mathbb{N}$ and all $x>0$ with $x\neq 1$, $J(x^{2k+1})\le J(x^{2j+1})$, where $J(t)=(t+t^{-1})/2-1$.
background
The recognition cost is $J(x)=(x+x^{-1})/2-1$ on positive reals (the T5 unique solution of the Recognition Composition Law up to the usual normalizations). It vanishes only at the unit ratio $x=1$ and is strictly positive elsewhere.
This module studies how the unit of the cost gauge is forced by minimality rather than by an external convention. The odd-power family is the set of maps $x\mapsto J(x^{2m+1})$ for $m\in\mathbb{N}$. Odd exponents preserve the reciprocal symmetry of $J$ and stay inside the inhabited part of the anchor-free ledger.
The predicate packages pointwise leastness of one member of that family: the $k$-th member charges no more than any other member, at every ratio other than the unit. No reference to a preferred base or to a numerical anchor value appears in the statement.
proof idea
Definitional packaging only. The body is the Prop $\forall j,;\forall x>0,;x\neq 1,; J(x^{2k+1})\le J(x^{2j+1})$. No tactics, no lemmas applied at this site. Downstream theorems discharge or characterize the predicate.
why it matters
Feeds two local characterizations. isLeast_iff_canonical proves the predicate holds if and only if $k=0$, so the canonical cost is the unique least element of the odd-power gauge family; the doc-comment stresses that leastness is quantified over the family alone and happens to select exactly one member. anchor_is_minimality then equates the stipulated anchor identity $J(b^{2k+1})=J(b)$ with this leastness predicate, for any base $b>0$, $b\neq 1$.
In the Recognition ledger this converts the last numerical stipulation into a pure minimality statement (T5 $J$-uniqueness in the background). The accompanying note on anchor_is_minimality records the residual open: leastness over the whole ledger, not just the odd-power subfamily, still needs the paper's full classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.