PRCStrengthenedNativeCostUniquenessTarget_refuted
plain-language theorem explainer
The strengthened native-cost uniqueness claim is false: even after adjoining the prime-pair product cost axiom, uniqueness of the canonical cost on ratio orbits still fails. Anyone tracking the native-cost selection ledger or the continuum price residue wall will cite this. The proof is a one-shot counterexample: the absolute-value character cost meets the strengthened hypotheses yet disagrees with the canonical cost at the orbit of −1.
Claim. It is not the case that every map $F$ from ratio orbits to ratio orbits satisfying the strengthened native-cost hypotheses (reciprocity, normalization invariance, canonical RCL on nonzero orbits, unit-zero, two-calibration, and the prime-pair product cost law) agrees with the canonical cost $q \mapsto J(q)$ under cross-equality on every ratio orbit $q$.
background
In the Primitive Recognition Calculus, costs are maps on ratio orbits. The canonical cost is the orbit-level display of the J-cost $J(x)=(x+x^{-1})/2-1$ forced by T5. Native-cost hypotheses package reciprocity, normalization invariance, the Recognition Composition Law on nonzero orbits, unit-zero, and two-calibration. The strengthened package adds a prime-pair product cost law.
The uniqueness target asserts that any $F$ obeying those strengthened hypotheses is cross-equal to the canonical cost on every orbit. Cross-equality means the underlying rational displays agree. The ratio orbit of $-1$ is the standard probe for missing signed-unit calibration: absolute-value characters erase the sign of $-1$ and therefore cannot match $J(-1)$.
Upstream, absValueGeneratedNativeCost is built from the absolute-value character (zero at the unit orbit, otherwise the character cost). It has already been shown to satisfy the strengthened hypotheses, and separately shown not to match the canonical cost at the orbit of $-1$.
proof idea
Term-mode reductio. Assume the uniqueness target. Instantiate it at the absolute-value generated native cost, feeding the already-proved fact that this cost satisfies the strengthened hypotheses, and evaluate at the orbit of $-1$. The uniqueness assumption then yields cross-equality between that cost and the canonical cost at $-1$. Discharge by the prior lemma that the absolute-value generated cost is not canonical at $-1$. No further algebraic work.
why it matters
This closes the strengthened uniqueness door in the native-cost selection program. Downstream, the continuum price residue wall records it as strengthened_insufficient, and both the full and slim premise ledgers list the base/strengthened uniqueness refutations as necessity witnesses: reciprocity-plus-RCL-plus-prime-pair data alone do not pin the canonical J-cost. A further sibling uses this refutation to kill the signed-admissible character factorization target, showing that even factoring through admissible characters does not restore uniqueness under the strengthened package.
In framework terms this sits under the T5 J-uniqueness story: the functional equation forces $J$ among continuous (or otherwise regular) solutions, but the purely algebraic native-cost axioms on ratio orbits still admit the absolute-value twist. The residue wall therefore forces additional selection structure (orientation, signed units, continuum price) before the canonical cost is unique. That is the selection deposit this lemma underwrites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.