PRCZeroCalibratedNativeCostUniquenessTarget_refuted
plain-language theorem explainer
The zero-calibrated native-cost uniqueness target is false: a map on ratio orbits can obey the native cost hypotheses and have zero-calibrated doubled trace without matching the canonical orbit map. Anyone auditing PRC cost uniqueness or the native-cost blocker certificate needs this refutation. The proof instantiates the claimed uniqueness at the absolute-value-generated native cost and contradicts canonicity at the orbit of -1.
Claim. It is not the case that every map $F$ from ratio orbits to ratio orbits that satisfies the native cost hypotheses and whose doubled-trace cost is zero-calibrated must obey $F(q)\simeq q$ (cross-equality with the canonical on-orbit embedding) for every ratio orbit $q$.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits constrained by the native cost hypotheses. The doubled-trace construction turns such an $F$ into a real-valued cost; zero-calibration requires that this cost vanish on the identity orbit in the calibrated sense.
The absolute-value character sends each orbit to the orbit of the absolute value of its rational display. As its doc-comment states, it is "a quotient respecting ratio character, but it erases the sign of $-1$." From that character one builds the absolute-value-generated native cost, which the module proves satisfies the native hypotheses and has zero-calibrated doubled trace.
The uniqueness target asserts that any such $F$ must cross-equal the canonical on-orbit embedding everywhere. That would give a unique zero-calibrated native cost from the hypotheses alone.
proof idea
Assume the uniqueness target holds. Instantiate it at the absolute-value-generated native cost, feeding the lemmas that this map satisfies the native cost hypotheses and that its doubled trace is zero-calibrated. The resulting identity at the orbit of $-1$ is handed to the lemma that the absolute-value-generated cost is not canonical at $-1$, yielding the contradiction. The argument is a short term-mode reductio: one counterexample map kills the universal claim.
why it matters
This refutation blocks any claim that zero-calibration plus native hypotheses alone force the canonical native cost. It is consumed by the native-cost uniqueness blocker certificate and by the universal-foundation conditional certificate, so the foundation layer records the failure explicitly rather than leaving a false uniqueness gap.
The repaired path, noted next to this declaration, requires factorization through a signed-admissible character rather than the unsigned admissible interface that absolute value satisfies. That repair is the natural next step after T5 J-uniqueness in the forcing chain: the cost side must retain sign structure that absolute value erases. Without this theorem one could mis-close uniqueness too early and mis-state the PRC cost interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.