cubeGeneratedNativeCost_two_not_canonical
plain-language theorem explainer
The cube-generated native cost disagrees with the canonical cost on the ratio orbit of two under cross-equality. Anyone arguing that the anchor-free structural ledger fails uniqueness cites this counterexample. The proof is a short reduction to injectivity of odd-power generated costs at the anchor (exponent 3 versus 1).
Claim. The native cost generated by the cube (odd power $3$) is not cross-equal, as a function on ratio orbits, to the canonical cost evaluated on the ratio orbit of $2$.
background
In the Primitive Recognition Calculus ledger, native costs are real-valued functions on ratio orbits built from the J-cost $J(x)=(x+x^{-1})/2-1$ (the unique solution forced by the Recognition Composition Law). Odd-power generators produce a family $q\mapsto J(q^{2k+1})$; the case $k=0$ is the canonical cost, while $k=1$ is the cube-generated cost.
Cross-equality (crossEq) is the ledger's comparison of two costs on a fixed orbit after transporting through the rational presentation of that orbit. The structural ledger without the two-calibration anchor keeps zero-calibration and the other structural fields, but drops the unit choice that pins $\chi(2)=2$.
Upstream, oddPowerGeneratedNativeCost_anchor_injective states that distinct odd exponents yield costs that separate at the anchor orbit. The long module note records that the full gauge-orbit claim (odd-power family equals the whole orbit) still has a factorization gap once the anchor is dropped: traces can be rational while the character itself is not carrier-valued.
proof idea
Instantiate odd-power anchor injectivity at $k=1$ and $k'=0$ (cube versus identity); norm_num discharges $1\neq 0$. Assume for contradiction that the cube-generated cost is cross-equal to the canonical cost on the orbit of two. Rewrite that assumption via crossEq_iff_toRat_eq and the identification of the $k'=0$ generator with the zero case of the odd-power family, then apply crossDisp to obtain equality of the underlying rational displacements. That equality is exactly what injectivity forbids, so the assumption is false.
why it matters
This is the concrete witness that uniqueness fails without the anchor. Downstream, PRCStructuralSansAnchorUniquenessTarget_refuted feeds the cube-generated cost and its sans-anchor certificate into the uniqueness target and invokes this theorem at orbit two, concluding: the anchor is a genuine unit gauge; everything else in the ledger is structure, the last field is a choice of unit.
In the broader Recognition chain this sits under T5 J-uniqueness and the native-cost minimality story: the composition law forces the J shape, but selecting which gauge representative is the physical cost still needs a calibration (here two-calibration). The module note separates the remaining open work (real-valued character factorization without a rational root for $\chi(2)$, then the six-exponentials input that forces the exponent to a nonnegative integer) from this settled negative uniqueness fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.