PRCDoubledTraceZeroCalibratedCoherentRootTarget_proved
plain-language theorem explainer
Any doubled-trace map on ratio orbits that meets the doubled-trace hypotheses and is zero-calibrated admits a ratio character whose coherent root recovers the trace: T(q) equals χ(q)+χ(q)⁻¹ pointwise up to cross-equality. Native-cost uniqueness and character-trace lift arguments cite this. The proof is a one-line reduction through the already-proved linear-root target.
Claim. For every map $T$ from ratio orbits to ratio orbits, if $T$ satisfies the doubled-trace hypotheses and is zero-calibrated, then there exists a ratio character $\chi$ such that for every orbit $q$, $T(q)$ is cross-equal to $\chi(q)+\chi(q)^{-1}$.
background
In the Primitive Recognition Calculus, native cost is forced by reading a doubled trace on ratio orbits: the object that should behave like $x\mapsto x+x^{-1}$ (equivalently $2J(x)+2$ after centering). A ratio character is a multiplicative map on orbits compatible with the PRC ratio structure; the coherent root of a doubled trace is a character $\chi$ whose sum with its reciprocal recovers the trace pointwise under cross-equality of orbits.
Zero-calibration means the trace vanishes on the zero orbit, blocking the zero-spike pathology that previously obstructed root extraction. The repaired target packages exactly that: doubled-trace hypotheses plus zero-calibration imply existence of a coherent root character.
The local module develops uniqueness of native cost via character-trace matching and d'Alembert-type identities on the doubled trace, feeding the broader J-uniqueness forcing chain (T5: $J(x)=(x+x^{-1})/2-1$).
proof idea
Term-mode one-line wrapper. Apply the conversion lemma that upgrades a linear-root witness to a coherent-root witness, feeding the already-proved linear-root target theorem. No extra case analysis or orbit arithmetic is performed here; all substance lives in those two upstream results.
why it matters
Closes the repaired coherent-root obligation after the zero-spike no-go, so zero-calibrated doubled traces are character-recoverable. Downstream, the character-trace lift from doubled-trace zero-calibration and the zero-calibrated native-cost character-trace lift theorem both invoke this result to promote native-cost hypotheses to an explicit ratio character matching the generated doubled trace.
That lift is a structural step toward native-cost uniqueness in PRC: once the doubled trace is the coherent root of a character, cost is pinned to the canonical J-shape. In the Recognition forcing chain this is the local algebraic content of T5 J-uniqueness and the Recognition Composition Law identity for $J$. The remaining upstream blocker noted in-module is forcing zero trace at the zero orbit from native-cost hypotheses alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.