PRCNativeCostCharacterTraceLiftTarget_of_doubled_trace_coherent_root
plain-language theorem explainer
Assuming every native doubled trace admits a multiplicative ratio character realizing it as χ+χ⁻¹, every PRC-native RCL cost admits a character whose doubled trace matches the cost. Cited by anyone closing the discrete d'Alembert factorization for native costs. Proof is a short transport: push native-cost hypotheses to doubled-trace hypotheses, apply the coherent-root assumption, and return the same character.
Claim. If every map $T$ on ratio orbits that satisfies the doubled-trace hypotheses admits a multiplicative ratio character $\chi$ with $\chi(q)+\chi(q)^{-1}=T(q)$ (up to cross-equality), then every native cost $F$ satisfying the PRC-native cost hypotheses admits a ratio character $\chi$ whose doubled trace matches $F$.
background
In the Primitive Recognition Calculus, admissible costs on ratio orbits are constrained by the Recognition Composition Law. The native doubled trace of a cost $F$ is $T_F(q)=2(F(q)+1)$; for a cost generated by a character this equals $\chi(q)+\chi(q)^{-1}$.
The coherent-root target asks that any $T$ obeying the doubled-trace hypotheses (reciprocity and the discrete d'Alembert relation) be realized as the trace of some multiplicative ratio character. The character-trace-lift target is the corresponding statement for native costs: every $F$ with PRC-native cost hypotheses factors through a character whose trace matches the cost.
Upstream, nativeCostDoubledTrace builds $T_F$ from $F$, and a companion lemma shows native-cost hypotheses imply doubled-trace hypotheses on $T_F$. That bridge is what lets the coherent-root assumption speak about costs.
proof idea
Term-mode transport, not a new analytic argument. Fix $F$ with native-cost hypotheses. Form its doubled trace $T_F$ and apply the upstream conversion lemma to obtain doubled-trace hypotheses on $T_F$. Feed $(T_F,\text{hypotheses})$ into the coherent-root assumption; it returns a ratio character $\chi$ with $\chi+\chi^{-1}=T_F$. Package $(\chi,\text{character proof},\text{trace match})$ as the witness for the character-trace-lift target. No extra algebraic identities are proved here.
why it matters
This is the exact d'Alembert trace-lift step in the native-cost uniqueness chain. Downstream it is the sole input to the factorization theorem that upgrades trace-lift to full character factorization of every admissible PRC-native RCL cost (the first exact blocker named in the module doc).
In the broader Recognition Science forcing chain this sits under T5 J-uniqueness: the cost $J(x)=(x+x^{-1})/2-1$ is forced by the composition law, and discrete character factorization is how that uniqueness is recovered on ratio orbits. Closing the coherent-root hypothesis would discharge both this lift and the factorization parent, completing the discrete half of native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.