PRCDoubledTraceCoherentRootTarget_refuted
plain-language theorem explainer
The coherent-root closure demand for native doubled traces is false: not every map satisfying the doubled-trace hypotheses arises as χ+χ⁻¹ for a multiplicative ratio character. Anyone tracking uniqueness of the native cost via d'Alembert character traces would cite this. The proof is a one-line counterexample application of the zero-spike doubled trace.
Claim. It is not the case that every map $T$ on ratio orbits obeying the doubled-trace hypotheses (reciprocity, normalized invariance, and the nonzero d'Alembert law) is realized by some multiplicative ratio character $\chi$ in the sense that $\chi(q)+\chi(q)^{-1}$ matches $T(q)$ for every orbit $q$.
background
In the primitive recognition calculus, native cost uniqueness is pursued by asking whether doubled-trace data on ratio orbits come from multiplicative characters. A ratio character $\chi$ yields the doubled trace $q \mapsto \chi(q)+\chi(q)^{-1}$. The doubled-trace hypotheses package reciprocity, a normalization/invariance condition, and a d'Alembert functional equation restricted to nonzero inputs.
The coherent-root target asserts that every $T$ meeting those hypotheses is the doubled trace of some ratio character. That would close the remaining d'Alembert blocker by forcing character realization for arbitrary native doubled traces.
The zero-spike map is canonical away from zero (matching the native cost doubled trace) but sends the zero orbit to $1$. Because d'Alembert only constrains nonzero inputs, this spike still satisfies the hypotheses, yet character traces with the intended zero image must give doubled trace $0$ at the zero orbit.
proof idea
Assume the coherent-root target. Instantiate it at the zero-spike doubled trace, using the already-proved fact that this map satisfies the doubled-trace hypotheses. The target then supplies a ratio character whose doubled trace equals the spike everywhere. That existence statement is exactly what zeroSpikeDoubledTrace_no_ratio_character_trace negates, yielding the contradiction. The argument is a pure counterexample specialization: no new algebraic work beyond feeding the spike into the universal claim.
why it matters
Native cost uniqueness in the PRC stack needs a clean bridge from d'Alembert-type doubled traces to multiplicative characters (the route that recovers the J-cost shape forced at T5). The coherent-root target was the remaining candidate for that bridge. Refuting it shows the current doubled-trace hypothesis package is too weak: nonzero d'Alembert leaves $T(0)$ free, while genuine character traces pin the zero orbit.
No downstream theorem yet consumes this refutation (used_by is empty), so its role is diagnostic. It forces any future uniqueness proof to add zero-orbit compatibility (or an equivalent constraint) before claiming character realization. Within the forcing chain, this sits upstream of J-uniqueness and the Recognition Composition Law: without a sound character bridge, the native cost cannot yet be identified with $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.