PRCZeroCalibratedNativeCostCharacterTraceLiftTarget_proved
plain-language theorem explainer
Under native cost hypotheses on a map F of ratio orbits, plus zero calibration of its doubled trace T_F(q)=2(F(q)+1), a ratio character χ exists whose doubled character trace matches F. The character-factorization theorem cites this lift. The proof is a thin packaging: convert native hypotheses to doubled-trace hypotheses, then apply the zero-calibrated coherent-root theorem.
Claim. For every map $F$ on ratio orbits satisfying the native cost hypotheses, if the doubled trace $T_F(q)=2(F(q)+1)$ is zero-calibrated, then there exists a ratio character $\chi$ such that $\chi$ is a PRC ratio character and the character trace of $\chi$ matches the cost $F$.
background
In the primitive recognition calculus, a native cost is a map $F$ on ratio orbits obeying a fixed package of algebraic hypotheses (reciprocity, normalization invariance, and a d'Alembert-type composition law). From any such $F$ one forms the doubled trace $T_F(q)=2(F(q)+1)$. For a cost generated by a character this equals $\chi(q)+\chi(q)^{-1}$, the standard character-trace pairing.
The structure PRCDoubledTraceHypotheses records the reciprocal, normalized-invariant, and d'Alembert properties that $T_F$ inherits from the native cost package. Zero calibration of that doubled trace is an extra root condition: the trace vanishes on the distinguished zero orbit in the calibrated sense required by the coherent-root target.
The unqualified character-lift target (native hypotheses alone) is false; Pass 294 closed that route. The repaired surface therefore demands native hypotheses plus explicit zero calibration of $T_F$ before asserting existence of a matching ratio character.
proof idea
Term-mode packaging, not a new calculation. Introduce $F$, its native-cost hypotheses, and the zero-calibration hypothesis on $T_F$. Apply nativeCostDoubledTrace_hypotheses_of_native_cost_hypotheses to obtain PRCDoubledTraceHypotheses for nativeCostDoubledTrace F. Feed that package, together with zero calibration, into PRCDoubledTraceZeroCalibratedCoherentRootTarget_proved, which returns a ratio character $\chi$ with the coherent-root and trace-match data. Re-export the same triple as the native-cost lift witness. No extra algebraic work occurs at this layer.
why it matters
This is the repaired native-cost entry point for character lifting inside PRC native-cost uniqueness. Downstream, PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved immediately consumes the witness and continues to full character factorization of the cost.
In the Recognition framework the move is the cost-to-character half of J-uniqueness (forcing-chain T5): once a native cost is zero-calibrated on its doubled trace, it must arise from a ratio character whose doubled trace is $\chi+\chi^{-1}$, the algebraic skeleton behind $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law. The declaration exists because the unqualified lift was disproved; zero calibration is the exact extra hypothesis that restores a true theorem rather than a false interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.