anchor_iff_canonical
plain-language theorem explainer
For any positive base b ≠ 1 and natural number k, the recognition cost J of the odd power b^(2k+1) equals J(b) exactly when k = 0. Researchers arguing that the structural-ledger anchor is forced (not a free convention) cite this. The proof is a short biconditional: equality for k ≥ 1 contradicts the strict odd-power cost inequality, and k = 0 is immediate.
Claim. Let $J(x) = \frac{x + x^{-1}}{2} - 1$ be the recognition cost on positive reals. For every real $b > 0$ with $b \neq 1$ and every $k \in \mathbb{N}$, $J\bigl(b^{2k+1}\bigr) = J(b)$ if and only if $k = 0$.
background
The recognition cost $J(x) = (x + x^{-1})/2 - 1$ is the standard RS cost on positive ratios: it vanishes only at the unit $x = 1$ and is strictly positive on genuine distinctions. It is the unique continuous solution (up to scale) of the Recognition Composition Law, and appears throughout the Cost modules as Jcost.
In Cost.UnitFromMinimality the anchor-free ledger is reduced, on the countable carrier, to the gauge family of odd powers of a fixed base: members of the form $b^{2k+1}$. The module's standing question is whether a stipulated anchor value on that family is a free convention or is forced by least cost.
The decisive upstream fact is the strict inequality: for $b > 0$, $b \neq 1$, and $k \geq 1$, one has $J(b) < J(b^{2k+1})$. Its doc-comment states the unit is the cheapest gauge member, so least cost picks out $J$ with no calibration and no preferred anchor base.
proof idea
Biconditional via constructor.
Forward direction: assume $J(b^{2k+1}) = J(b)$ and $k \neq 0$. Then $1 \leq k$, so jcost_lt_odd_power yields the strict inequality $J(b) < J(b^{2k+1})$. That contradicts equality by ne_of_gt and absurd.
Reverse direction: substitute $k = 0$, reduce $b^{1} = b$, and close with norm_num. No further lemmas are needed.
why it matters
This is the equality half of the anchor-as-minimality identification. Downstream, anchor_is_minimality rewrites the anchor condition $J(b^{2k+1}) = J(b)$ into the least-odd-power-cost predicate by chaining this iff with isLeast_iff_canonical. Its doc-comment states the point: on the gauge family the stipulated anchor value and genuine leastness hold of exactly the same member, for any anchor base, so the one surviving ledger stipulation is least cost evaluated at a point, not a conventional number.
In the forcing chain this sits under T5 (J-uniqueness): once $J$ is fixed, the odd-power family has a unique cheapest member, and any single non-unit ratio pins that same member. The choice of orbit-two as anchor is therefore immaterial. Leastness over the whole ledger (beyond the inhabited odd-power subfamily) is explicitly deferred to the accompanying paper's classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.