PRCNativeCostFactorizationAdmissibilityUpgradeTarget_refuted
plain-language theorem explainer
The factorization-side upgrade claim is false: a native cost that factors through some ratio character need not admit an admissible character generating the same cost. Anyone tracking uniqueness or admissibility of native J-cost factorizations would cite this negative result. The proof is a one-line application of an explicit two-adic axis-twist counterexample already constructed in-module.
Claim. The following upgrade statement fails: it is not true that for every native cost $F$ and every ratio character $\chi$ with $F(q)$ cross-equal to the cost generated by $\chi$ at every ratio orbit $q$, there exists an admissible ratio character $\psi$ generating the same cost as $\chi$.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits satisfying a fixed package of algebraic hypotheses (symmetry, normalization, and the Recognition Composition Law structure that forces the classical $J$-shape). Costs can be generated from ratio characters $\chi$ via costFromCharacter; two such values are identified when they are cross-equal on orbits, which is the right notion because $J(\chi q)$ cannot tell a direction from its reciprocal.
The upgrade target asked for a weak replacement: given any native $F$ that matches the cost of some (not necessarily admissible) ratio character $\chi$, produce an admissible character $\psi$ with the same generated cost. Admissibility is the stricter structural filter used elsewhere in the uniqueness chain; the upgrade would have let factorization proofs pass through non-admissible intermediate characters.
Upstream, a concrete two-adic axis-twist native cost is already built and shown to satisfy the native-cost hypotheses while matching a twist-generated character. A companion lemma records that any such twist cost immediately kills the upgrade target.
proof idea
One-line term proof. Apply the general obstruction lemma that says: if a two-adic axis-twist generated cost with native hypotheses exists, then the factorization admissibility upgrade target is false. Feed it the already-constructed witness PRCTwoAdicAxisTwistGeneratedCostNativeHypothesesTarget_constructed, which packages the two-adic generated native cost, its native hypotheses, and the cross-equality to the twist-generated character. No further case analysis is required.
why it matters
This closes a hoped-for shortcut on the factorization side of native-cost uniqueness. The upgrade target was the natural weakening once one notices that $J$ is blind to reciprocal directions; refuting it means uniqueness arguments cannot freely replace an arbitrary ratio-character factor by an admissible one while keeping the generated cost fixed.
In the broader Recognition Science forcing chain this sits next to T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law: the native cost is meant to be forced to that $J$-shape, and factorization through characters is part of how that forcing is organized. The two-adic axis twist is a genuine native-cost object, so the obstruction is internal, not an exotic pathology outside the hypotheses.
No downstream consumers are wired yet; the result stands as a negative landmark that steers later uniqueness proofs away from this upgrade route and toward arguments that either enforce admissibility earlier or work directly with the twist-invariant data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.