PRCStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted
plain-language theorem explainer
The repaired claim that every strengthened native cost factors through a signed-admissible ratio character is false. Cite this when closing off character-factorization routes in the PRC native-cost uniqueness program. The proof is a one-line composition: signed-admissible factorization implies the uniqueness target, which is already refuted.
Claim. It is false that every map $F$ on ratio orbits satisfying the strengthened native-cost hypotheses admits a signed-admissible ratio character $\chi$ such that $F(q)$ is cross-equal to the cost induced by $\chi$ at every orbit $q$.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits obeying a strengthened hypothesis package (symmetry, normalization, and d'Alembert-type constraints tied to the J-cost). Characters on ratio orbits induce candidate costs via costFromCharacter; the unsigned admissible interface was already killed by the absolute-value character counterexample.
The signed-admissible factorization target is the repaired upgrade: every strengthened native cost should factor as the character-cost of some signed-admissible $\chi$, with agreement witnessed by cross-equality on orbits. A companion lemma shows that any such factorization immediately yields the strengthened uniqueness target (all strengthened native costs are cross-equal to a fixed canonical cost).
That uniqueness target is independently refuted: the absolute-value-generated native cost satisfies the strengthened hypotheses yet fails canonicity at the negative-one ratio orbit.
proof idea
Term-mode reductio. Assume the signed-admissible factorization target. Apply the implication lemma that turns any such factorization into the strengthened uniqueness target (extract $\chi$, then transport cross-equality). Feed that uniqueness instance into the existing uniqueness refutation, which derives a contradiction from the absolute-value-generated native cost at the negative-one orbit. No new analytic work; pure composition of the two upstream results.
why it matters
Closes the natural repair of the character-factorization route after the unsigned admissible interface failed. In the Recognition forcing chain, native-cost uniqueness is the local avatar of T5 J-uniqueness ($J(x)=\cosh(\log x)-1$): if strengthened costs had to factor through signed-admissible characters, uniqueness would follow, but both the uniqueness target and this factorization target are now refuted.
No downstream consumers yet (used_by is empty). The result is a negative landmark: it forces the uniqueness program either to weaken the hypothesis package, change the character interface, or abandon character factorization as the path to canonicity. It sits beside the absolute-value counterexample as a hard constraint on what a PRC-native cost calculus can demand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.