PRCDoubledTraceCoherentRootTarget
plain-language theorem explainer
The coherent-root target asserts that every map T on ratio orbits obeying the doubled-trace hypotheses is the orbit-level trace χ + χ⁻¹ of some multiplicative ratio character χ. Native-cost uniqueness work cites it as the remaining d'Alembert factorization blocker. The body is a pure Prop definition packaging that universal claim; it is later refuted by a zero-spike counterexample.
Claim. For every map $T$ from ratio orbits to ratio orbits that is reciprocal, normalization-invariant, and satisfies the nonzero d'Alembert law, there exists a multiplicative ratio character $\chi$ (unit at $1$, multiplicative up to cross-equivalence) such that for every ratio orbit $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to $T(q)$.
background
In the Primitive Recognition Calculus, rationals are displayed as ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Equality is not definitional; it is the cross-multiplication relation crossEq, which balances scaled numerators and denominators as signed orbits. Reciprocals are total and send the zero orbit to itself, matching $\mathbb{Q}$.
A ratio character $\chi$ is a map on ratio orbits that is a unit at $1$ and multiplicative up to cross-equivalence. Its doubled trace is the orbit sum $\chi(q)+\chi(q)^{-1}$. The structure PRCDoubledTraceHypotheses packages what a native PRC cost's doubled trace must satisfy: reciprocity $T(q)\sim T(q^{-1})$, invariance under denominator normalization, and a d'Alembert identity restricted to nonzero inputs.
This module studies uniqueness of the native cost via d'Alembert factorization. The coherent-root target is the remaining blocker: whether every such $T$ is realized as the doubled trace of some ratio character.
proof idea
Definitional packaging only. The Prop is the universal quantification over maps $T$ of ratio orbits, the doubled-trace hypothesis bundle as antecedent, and an existential for a ratio character $\chi$ whose pointwise doubled trace $\chi(q)+\mathrm{recip}(\chi(q))$ matches $T(q)$ under cross-equivalence. No tactics or lemmas are applied in the body.
why it matters
This is the coherent-root form of the remaining d'Alembert blocker for native PRC cost uniqueness. Downstream, PRCDoubledTraceCoherentRootTarget_refuted shows the claim is false: a doubled trace that is canonical off zero but spikes the zero orbit to trace $1$ still meets the hypotheses (their d'Alembert law ignores zero) yet admits no ratio-character trace.
Two conditional bridges still use it as a hypothesis: if the target held, it would imply the character trace-lift target and, via that, the character factorization target for native costs. The refutation therefore forces a sharper route around zero, rather than a blanket coherent-root factorization. In the broader Recognition chain this sits under cost uniqueness feeding J-uniqueness (T5) and the Recognition Composition Law, where the cost must be forced as $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.