oddPowerGeneratedNativeCost_anchor_injective
plain-language theorem explainer
Distinct odd-power native costs disagree at the orbit of 2: the anchor values J(2^{2k+1}) and J(2^{2k'+1}) are unequal whenever k ≠ k'. Anyone classifying the gauge orbit of native costs, or separating the cube generator from the canonical cost, cites this. The proof reduces cross-equality to rational equality and applies strict monotonicity of jq on powers of two at or above 1.
Claim. For natural numbers $k \neq k'$, the native costs generated by the odd powers $2k+1$ and $2k'+1$ are not cross-equal on the ratio orbit of $2$. Equivalently, their anchor values satisfy $J(2^{2k+1}) \neq J(2^{2k'+1})$.
background
In the primitive recognition calculus, native costs are compared on ratio orbits via cross-equality: two costs are cross-equal when they induce the same values after transport to a common rational representative. The family oddPowerGeneratedNativeCost k assigns, on positive ratios, the J-cost of the $(2k+1)$-st power; at the distinguished orbit of $2$ this is exactly $J(2^{2k+1})$.
The local ledger works with a rationalized J-cost jq on $\mathbb{Q}_{>0}$. Sibling facts record that jq is nonnegative, vanishes only at $1$, and is strictly monotone on $[1,\infty)$. The Recognition Composition Law forces $J(x)=(x+x^{-1})/2-1$ (T5), so monotonicity of jq above the unit is the discrete shadow of that uniqueness.
The module builds a structural ledger of native costs that satisfy the PRC hypotheses without fixing the anchor. Separating members of the odd-power family at the orbit of $2$ is the first step toward showing that ledger is infinite and that the cube generator is non-canonical.
proof idea
Rewrite cross-equality as equality of the rationalized costs via RatioOrbit.crossEq_iff_toRat_eq, then unfold oddPowerGeneratedNativeCost_toRat and two_toRat so the goal is $jq(2^{2k+1}) \neq jq(2^{2k'+1})$.
A local lemma hstrict shows $i < j$ implies $jq(2^{2i+1}) < jq(2^{2j+1})$: apply jq_strictMono on the interval $[1,\infty)$, using $1 \le 2^{2i+1}$ and the strict power comparison $2^{2i+1} < 2^{2j+1}$ from pow_lt_pow_right₀.
Case-split on $k < k'$ versus $k' < k$ via lt_or_gt_of_ne, and discharge each side by ne_of_lt or ne_of_gt against hstrict.
why it matters
This injectivity is the separation engine for the odd-power gauge orbit. Downstream, gauge_orbit_contains_every_odd_power packages it with the sans-anchor hypotheses: every odd exponent inhabits the anchor-free ledger, and distinct exponents disagree at the anchor, so the gauge orbit is infinite.
It also feeds cubeGeneratedNativeCost_two_not_canonical by specializing to $k=1$, $k'=0$: the cube cost charges $J(8)=49/16$ at orbit $2$, while the canonical cost charges $J(2)=1/4$, so the cube generator is not cross-equal to the on-orbit canonical cost.
In the broader RS chain this is ledger hygiene rather than a new forcing step: T5 already fixed $J$, and the eight-tick / $D=3$ story lives upstream. The point here is structural: native-cost candidates generated by odd powers are pairwise distinguishable at a single concrete anchor, which keeps the PRC structural ledger from collapsing under gauge identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.