PRCDoubledTraceZeroCalibratedCoherentRootTarget_of_linear_root
plain-language theorem explainer
If every zero-calibrated doubled-trace map admits a working linear root candidate, then it admits a coherent root: a ratio character χ with χ(q)+χ(q)⁻¹ matching T(q) pointwise. Used to discharge the repaired coherent-root target after the zero-spike no-go. Proof packages the linear-root hypothesis with the explicit trace-root candidate as the existential witness.
Claim. Assume that for every map $T$ on ratio orbits, the native doubled-trace hypotheses plus zero-calibration imply that the linear root candidate works for $T$. Then every such $T$ admits a coherent root: there exists a ratio character $\chi$ such that $\chi(q)+\chi(q)^{-1}$ is cross-equal to $T(q)$ for all ratio orbits $q$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, a doubled-trace map $T$ on ratio orbits is the algebraic stand-in for the cost side of a d'Alembert identity (the Recognition Composition Law shape $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$). A ratio character $\chi$ is a multiplicative orbit map whose split trace $\chi(q)+\chi(q)^{-1}$ is meant to recover $T(q)$.
Zero-calibration repairs the zero-spike no-go: it forces the zero orbit to behave so a root can still be chosen. The linear root candidate is the explicit formula forced by the split-trace identity at the distinguished axis $2$: when $\chi(2)=2$, one has $\chi(q)=(2,T(2q)-T(q))/3$ off zero, with the zero orbit supplied by the calibration field.
The linear-root target asserts that this candidate works (is a character and matches the trace). The coherent-root target only asks for existence of some character with matching split trace. This lemma is the implication from the stronger linear package to the existential coherent package.
proof idea
Short packaging proof. Fix $T$ with doubled-trace hypotheses and zero-calibration. Apply the linear-root target hypothesis to obtain that the linear candidate works: a character property together with pointwise trace matching. Return the existential coherent-root witness as the explicit trace-root candidate for $T$, carrying those two properties. No further algebra is done here.
why it matters
Closes the gap between the constructive linear-root package and the repaired coherent-root target used in native cost uniqueness. Downstream, the proved coherent-root theorem is exactly this implication applied to the proved linear-root target, so the whole coherent-root obligation reduces to verifying the linear candidate.
In the Recognition framework this sits under J-uniqueness (forcing-chain T5) and the RCL/d'Alembert structure of native cost: recovering a character whose split trace equals $T$ is the orbit-level form of writing cost as $J$-type data. The doc flags an exact upstream zero-orbit blocker left after the coherent-root theorem; this bridge does not remove that blocker, it only routes the coherent target through the linear candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.