PRCStructuralSansAnchorUniquenessTarget_refuted
plain-language theorem explainer
The anchor-free structural ledger does not force the canonical native cost: uniqueness fails once the unit-gauge anchor is dropped. Anyone citing the stratification certificate, or arguing that calibration is partly continuum overhead rather than pure structure, will use this. The proof is a short contradiction: the cube-generated cost meets every sans-anchor hypothesis yet disagrees with the canonical cost at the orbit of two.
Claim. It is false that every map $F$ from ratio orbits to ratio orbits that satisfies the anchor-free structural native-cost hypotheses is pointwise cross-equal to the canonical cost on the ratio orbit. Equivalently, the structural ledger without its anchor field does not uniquely determine the Recognition cost.
background
In the Primitive Recognition Calculus, native costs on the ratio-orbit carrier are constrained by a structural ledger. The anchor-free fragment packages base structure, orientation (sign) reversal, monotonicity, and zero-calibration; the full ledger adds an anchor that fixes the unit gauge.
The uniqueness target for that sans-anchor fragment asserts that any $F$ meeting those hypotheses agrees with the canonical cost (the orbit image of the standard $J$-cost) at every ratio orbit. On the completed line the composition law is looser: it admits the full scale family $x \mapsto J(x^\ell)$ for every real $\ell > 0$, and calibration must collapse that uncountable gauge orbit. The free carrier does not inherit that whole family.
Upstream, every nonnegative integer power character, sign-extended, inhabits the anchor-free ledger: signed powers satisfy base structure, sign-reversal, monotonicity, and zero-calibration at every index. Pure even powers fail sign-reversal; the signed versions do not. The cube-generated cost is the concrete countermodel used below.
proof idea
Assume uniqueness holds for every cost meeting the sans-anchor structural hypotheses. Instantiate that claim at the cube-generated native cost, which is already known to satisfy those hypotheses. Uniqueness then forces the cube-generated cost to match the canonical cost at the ratio orbit of two. A prior lemma states that the cube-generated cost is not canonical at two. The contradiction refutes the uniqueness target. The argument is a two-step term proof: intro on the uniqueness hypothesis, then apply the non-canonicity lemma to the instance at two.
why it matters
This is the gauge-inhabitation clause of the structural stratification certificate. Downstream, that certificate packages full (anchored) uniqueness, slimness, positivity, and this refutation as the witness that the anchor-free ledger is multi-valued, so the anchor is a genuine unit choice rather than redundant structure.
In framework terms it answers part of the continuum-versus-calibration question around the Recognition Composition Law and T5 $J$-uniqueness. On the completed line, calibration kills the full scale family (with $\ell = 2$ the headline continuum countermodel). On the carrier, sign-reversal already kills pure even powers without any anchor, yet signed power characters still populate the sans-anchor ledger. The anchor remains the price of pinning the unit. The module explicitly limits the claim: non-integer exponents are settled elsewhere (rational-trace integrality, six-exponentials), and the surviving wall is factorization into the odd-power family, not this exclusion alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.