PRCStrengthenedNativeCostUniquenessTarget_of_signed_admissible_factorization
plain-language theorem explainer
If every strengthened native cost factors through some signed-admissible ratio character, then every such cost is cross-equal to the canonical on-orbit cost. Anyone chasing uniqueness of the PRC native cost cites this implication. The proof is a short term argument: unpack the factor character, then transit cross-equality through signed-admissible character rigidity.
Claim. Assume that every map $F$ on ratio orbits satisfying the strengthened native-cost hypotheses factors through some signed-admissible ratio character $\chi$ in the sense that $F(q)$ is cross-equal to the cost built from $\chi$ at every orbit $q$. Then every such $F$ is cross-equal to the canonical on-orbit cost: $F(q)\sim\mathrm{onRatioOrbit}(q)$ for all $q$.
background
In the Primitive Recognition Calculus, costs and characters act on RatioOrbit, a choice-free display of a rational as a signed numerator orbit over a nonzero distinction-nat denominator. Equality of values is the relation crossEq, a polynomial cross-multiplication identity that is transitive by an integer-bridge lemma (no classical choice on rationals).
The strengthened native-cost uniqueness target asks that any $F$ obeying the strengthened native-cost hypotheses agree, via crossEq, with the canonical cost onRatioOrbit. An earlier unsigned factorization interface was already refuted by absolute-value characters. The repaired factorization target therefore demands a signed-admissible character $\chi$ with $F(q)$ cross-equal to costFromCharacter $\chi$ $q$.
Upstream, signed-admissible characters are rigid: for every such $\chi$ and every $q$, costFromCharacter $\chi$ $q$ is already cross-equal to onRatioOrbit $q$ (proved by global orientation, same-or-inverse cases).
proof idea
Term-mode, four steps. Fix $F$ and the strengthened hypotheses, and fix an orbit $q$. Apply the factorization hypothesis to obtain a signed-admissible character $\chi$ with $F(q)\sim\mathrm{costFromCharacter},\chi,q$. Invoke the already-proved signed-admissible rigidity theorem at $(\chi,q)$ to get $\mathrm{costFromCharacter},\chi,q\sim\mathrm{onRatioOrbit},q$. Close by crossEq_trans. No extra case splits or classical choice.
why it matters
This is the bridge from the repaired signed factorization interface to the strengthened uniqueness target that replaced the old, refuted native uniqueness claim. Downstream it is used only once: the factorization target is refuted by composing this implication with the already-established refutation of uniqueness. In the Recognition forcing picture this sits inside the native-cost uniqueness campaign around the J-cost (T5) and the Recognition Composition Law: it shows that even the strengthened signed-admissible factorization route cannot salvage a non-canonical native cost, because rigidity collapses every signed-admissible factor back to the canonical on-orbit cost. The open question it closes is whether signed admissibility restores a viable factorization path; the answer, via this lemma plus the uniqueness refutation, is no.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.