PRCNativeCostCharacterTraceLiftTarget
plain-language theorem explainer
Packages the exact d'Alembert trace-lift form of character factorization for PRC-native costs: every cost F on ratio orbits meeting the native hypotheses admits a multiplicative ratio character χ whose doubled trace recovers F. Discrete uniqueness workers cite it as the intermediate target equivalent to full character factorization. Pure Prop abbreviation; downstream both derives it from coherent-root data and refutes it via the zero-flat cost.
Claim. For every map $F$ from ratio orbits to ratio orbits that satisfies the native cost hypotheses (reciprocity, normalization invariance, canonical RCL, and two-calibration), there exists a ratio character $\chi$ (unit at one, multiplicative up to cross-equivalence) such that for all $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to the native doubled trace of $F$ at $q$.
background
In the Primitive Recognition Calculus, costs live on RatioOrbit: rational displays with signed-orbit numerator and nonzero distinction-orbit denominator, compared by cross-equivalence rather than definitional equality. Native cost hypotheses on a map $F$ require reciprocity under inversion, invariance under normalization, the canonical Recognition Composition Law on the discrete surface, and a two-calibration that rules out the identically zero cost.
A ratio character $\chi$ is a unit-preserving multiplicative map on ratio orbits (again up to cross-equivalence). The trace-match predicate says the generated doubled character $\chi(q)+\chi(q)^{-1}$ recovers the native doubled trace built from $F$, which is the discrete stand-in for the continuous identity $F=J\circ\chi$ with $J(x)=(x+x^{-1})/2-1$.
This module isolates uniqueness of the PRC-native cost before real completion. The present definition is the exact d'Alembert trace-lift packaging of character factorization, parallel to the continuous T5 J-uniqueness step but stated entirely on the rational orbit surface.
proof idea
Definitional Prop abbreviation only. The body is the universal quantification over maps $F$ of native cost hypotheses, asserting existence of a ratio character whose trace matches the native doubled trace of $F$. No tactics, no lemmas applied at the definition site; downstream theorems discharge or refute the packaged statement.
why it matters
Sits at the hinge between character factorization and the remaining d'Alembert blocker on the discrete rational surface. Downstream, it is proved equivalent to the full factorization target, and both directions are recorded as one-line transfers via the cost-to-trace and trace-to-cost bridges. It is also the conclusion of the coherent-root and zero-calibrated doubled-trace routes, so any progress on those root targets immediately yields the lift.
In the Recognition chain this is the discrete analogue of the T5 J-factorization step (cost as $J$ composed with a multiplicative character), needed before the continuous real completion exists. The module later records an outright refutation: the zero-flat native cost satisfies the hypotheses yet admits no character trace, so the bare target is false. That refutation forces the coherent-root and calibration strengthenings that close the uniqueness path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.