PRCZeroCalibratedNativeCostCharacterTraceLiftTarget
plain-language theorem explainer
Defines the repaired target for lifting a native PRC cost to a ratio character: any F on rational orbits that obeys the native cost hypotheses and whose doubled trace vanishes at zero admits a multiplicative character χ whose d'Alembert trace recovers F. Cost-classification and uniqueness arguments cite this surface. It is a pure Prop package; the companion theorem discharges it.
Claim. For every map $F$ from rational orbits to rational orbits, if $F$ satisfies the native cost hypotheses (reciprocity, normalization invariance, canonical RCL, and two-calibration) and the doubled trace $T_F(q)=2(F(q)+1)$ obeys $T_F(0)=0$, then there exists a ratio character $\chi$ (unit at $1$, multiplicative up to cross-equivalence) such that $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to $T_F(q)$ for every orbit $q$.
background
In the Primitive Recognition Calculus, costs and characters live on RatioOrbit: integer numerator over a nonzero orbit denominator, compared by cross-equivalence rather than definitional equality. A native cost $F$ is constrained by PRCNativeCostHypotheses: reciprocity under inversion, invariance under normalization, the canonical Recognition Composition Law on the discrete rational surface, and two-calibration (ruling out the zero cost).
The doubled d'Alembert trace of such an $F$ is $T_F(q)=2(F(q)+1)$. For a genuine character factorization $F=J\circ\chi$ one expects $T_F(q)=\chi(q)+\chi(q)^{-1}$. A ratio character is a map $\chi$ with $\chi(1)\sim 1$ and multiplicativity up to cross-equivalence. Zero calibration of the trace, $T(0)=0$, is independent of the nonzero d'Alembert law and must be stated separately: character traces with the intended zero image force this condition.
The module packages uniqueness and factorization of native costs via this discrete d'Alembert lift, prior to real completion.
proof idea
No proof body: this is a def equating a name to a Prop. The proposition packages three ingredients already defined upstream: native cost hypotheses on $F$, zero calibration of nativeCostDoubledTrace F, and existence of a PRCRatioCharacter whose doubled trace matches the cost via PRCCharacterTraceMatchesCost. Discharge is deferred to the companion theorem PRCZeroCalibratedNativeCostCharacterTraceLiftTarget_proved, which builds doubled-trace hypotheses from the native ones and invokes the zero-calibrated coherent-root target.
why it matters
Pass 294 showed the unqualified character-lift target (native hypotheses alone) is false: without zero calibration of the generated doubled trace, factorization can fail at the zero orbit. This definition is the exact repaired interface. Downstream, PRCZeroCalibratedNativeCostCharacterTraceLiftTarget_proved asserts the proposition, feeding native cost uniqueness and the discrete d'Alembert route to $F=J\circ\chi$.
In the Recognition framework this sits under T5 J-uniqueness and the Recognition Composition Law: the continuous story forces $J(x)=(x+x^{-1})/2-1$, and here the same factorization is recovered on the rational-orbit surface once zero is pinned. It closes a scaffolding gap between native cost hypotheses and character existence without waiting for internal real completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.