PRCNativeCostCharacterTraceLiftTarget_refuted
plain-language theorem explainer
The exact d'Alembert trace-lift form of character factorization for native costs is false: not every native cost admits a multiplicative ratio character whose doubled trace recovers it. Cite this when ruling out character-trace uniqueness routes for the Recognition native cost. The proof is a one-line counterexample: instantiate the universal claim at the zero-flat native cost and apply the known nonexistence of a matching character for that cost.
Claim. It is not true that every map $F$ from ratio orbits to ratio orbits that satisfies the native cost hypotheses admits a multiplicative ratio character $\chi$ such that the character doubled-trace of $\chi$ matches $F$.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits obeying the Recognition Composition Law interface (reciprocity and the RCL-type identities) on nonzero inputs. A ratio character is a multiplicative map $\chi$ on those orbits; the doubled-trace construction builds a candidate cost from $\chi$ in the d'Alembert style (trace of $\chi+\chi^{-1}$ type data).
The target proposition asserts a universal lift: every native cost $F$ would factor as the character-trace of some ratio character $\chi$. That is the exact d'Alembert trace-lift version of character factorization.
A concrete native cost, the zero-flat cost, is canonical on every nonzero orbit but flattened to zero at the zero orbit. It still satisfies the native cost hypotheses because RCL only quantifies over nonzero inputs. Upstream, that cost is already known to admit no matching ratio character under the trace-matching predicate.
proof idea
Term-mode reductio. Assume the universal trace-lift target. Specialize it at the zero-flat native cost together with the theorem that this cost meets the native cost hypotheses. The resulting existential (a ratio character whose trace matches the zero-flat cost) contradicts the upstream lemma that no such character exists for the zero-flat cost. Discharge by that contradiction.
why it matters
This closes the exact d'Alembert trace-lift route as a path to uniqueness of the native Recognition cost: character-trace factorization cannot hold for every native cost. Downstream it is the sole ingredient in refuting the broader character-factorization target (via the implication from factorization to trace-lift). In the PRC uniqueness program this steers away from pure character-trace lifts and toward whatever remaining native-cost constraints actually pin $J$ (the T5 J-cost $(x+x^{-1})/2-1$ forced by RCL). It is a negative landmark inside native-cost uniqueness, not a construction of $J$ itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.