PRCNativeCostCharacterTraceLiftTarget_of_doubled_trace_zero_calibrated
plain-language theorem explainer
If every native PRC cost has doubled d'Alembert trace zero at the zero orbit, then every such cost admits a multiplicative ratio character whose trace realizes it. Uniqueness and factorization arguments in the primitive recognition calculus cite this reduction. The proof packages native-cost hypotheses into doubled-trace hypotheses, applies the zero-calibration assumption, and invokes the already-proved coherent-root existence theorem.
Claim. Assume that for every map $F$ on ratio orbits satisfying the native PRC cost hypotheses, the doubled trace $T_F(q)=2(F(q)+1)$ obeys $T_F(0)\sim 0$ (cross-equality at the zero orbit). Then for every such $F$ there exists a multiplicative ratio character $\chi$ with $\mathrm{trace}(\chi)$ matching $F$ in the d'Alembert sense (character-trace lift).
background
In the primitive recognition calculus, a native cost is a map $F$ on ratio orbits obeying reciprocity, normalization, and the d'Alembert functional law that forces the Recognition Composition Law shape of $J$. The doubled trace is $T_F(q)=2(F(q)+1)$; for a genuine character cost this equals $\chi(q)+\chi(q)^{-1}$.
PRCDoubledTraceHypotheses packages the reciprocal, normalized, and d'Alembert constraints on such a $T$. Zero-orbit calibration is independent of the nonzero d'Alembert law: characters with the intended zero image need $T(0)\sim 0$, recorded as PRCDoubledTraceZeroCalibrated. The target hypothesis here asserts that every native cost forces that calibration on its generated doubled trace.
The character-trace-lift target asks, for each native $F$, for a multiplicative ratio character $\chi$ whose doubled trace matches $F$. Upstream, native cost hypotheses already imply doubled-trace hypotheses, and a coherent-root theorem produces the character once zero calibration is known.
proof idea
Term-mode packaging of three steps. Fix $F$ with native cost hypotheses. Lift those hypotheses to PRCDoubledTraceHypotheses on nativeCostDoubledTrace F via nativeCostDoubledTrace_hypotheses_of_native_cost_hypotheses. Instantiate the assumed zero-calibration target at $F$ to obtain PRCDoubledTraceZeroCalibrated on that doubled trace. Apply PRCDoubledTraceZeroCalibratedCoherentRootTarget_proved to extract a ratio character $\chi$ with the matching-trace witness, and return the existential package required by the lift target.
why it matters
This is the exact bridge from the remaining zero-orbit blocker to d'Alembert character-trace lift for native PRC costs. Downstream, PRCNativeCostCharacterFactorizationTarget_of_doubled_trace_zero_calibrated composes it with the trace-lift-to-factorization step, so full character factorization of native costs reduces to zero calibration alone.
In the Recognition forcing chain this sits under T5 $J$-uniqueness: native costs are meant to be forced to $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), and character factorization is the analytic route that identifies the cost with a multiplicative character trace. Closing zero calibration therefore collapses the last local obstruction on the uniqueness path for the PRC native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.