anchor_is_minimality_over_powers
plain-language theorem explainer
Equality of recognition costs at a base and its nth power is equivalent to that exponent being least-cost among all nondegenerate powers. Anyone fixing the input scale of J by minimality cites this. The proof is a two-rewrite chain: both sides reduce to n = 1 via the anchor and least-power characterizations.
Claim. For every real $b>0$ with $b\neq 1$ and every natural number $n\geq 1$, one has $J(b^n)=J(b)$ if and only if $x\mapsto J(x^n)$ is pointwise least among all maps $x\mapsto J(x^m)$ for $m\geq 1$, where $J(x)=(x+x^{-1})/2-1$.
background
The recognition cost $J(x)=(x+x^{-1})/2-1$ is the unique continuous solution (up to scale) of the Recognition Composition Law. The functional equation fixes the output scale; the remaining freedom is the input scale, which this module removes by a minimality principle on power families.
IsLeastPowerCost $n$ asserts that $x\mapsto J(x^n)$ is a least element of the nondegenerate power family under the pointwise order: for every $m\geq 1$ and every $x>0$, $x\neq 1$, one has $J(x^n)\leq J(x^m)$. Exponent zero is excluded because it yields the identically zero cost.
Upstream, anchorPower_iff_canonical shows that $J(b^n)=J(b)$ forces $n=1$ for any single non-unit base $b$. The companion isLeastPower_iff_canonical identifies leastness with the same condition $n=1$. The present statement is the parity-free enlargement of the earlier odd-only anchor.
proof idea
One-line term proof by simultaneous rewrite of both sides. The left-hand equality $J(b^n)=J(b)$ is rewritten via anchorPower_iff_canonical to $n=1$. The right-hand predicate IsLeastPowerCost $n$ is rewritten via isLeastPower_iff_canonical to the same $n=1$. The two characterizations therefore coincide for every admissible base and every $n\geq 1$.
why it matters
This removes the parity restriction from the earlier odd-power anchor, covering every exponent the corrected classification admits. Downstream, discrete_gauge_has_a_floor_and_continuous_gauge_does_not uses the discrete least-cost floor to contrast countable carriers (where least cost selects the unit) against the continuum (where halving always undercuts).
In the Recognition framework this closes the input-scale freedom left after T5 (J-uniqueness from the composition law). The module records the payoff: the cost of the first distinction is now determined rather than stipulated, "telling one from two costs a quarter." The audit script cost_unit_axiom_audit tracks that the unit enters as a derived hypothesis rather than an ambient axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.