PRCNativeCostCharacterFactorizationTarget_of_trace_lift
plain-language theorem explainer
If every admissible PRC-native cost admits a ratio character whose doubled trace matches the cost, then every such cost factors through a ratio character in the discrete d'Alembert sense. Anyone closing the native-cost uniqueness chain cites this implication. The proof is a short term unpack: extract the character from the trace-lift hypothesis and convert trace-match into cross-equality via the dedicated conversion lemma.
Claim. Assume that for every map $F$ on ratio orbits satisfying the PRC-native cost hypotheses there exists a ratio character $\chi$ whose character-trace matches $F$. Then for every such $F$ there exists a ratio character $\chi$ with $\mathrm{crossEq}(F(q),\,\mathrm{costFromCharacter}(\chi,q))$ for all ratio orbits $q$.
background
In the Primitive Recognition Calculus, admissible costs on ratio orbits are those obeying the PRC-native cost hypotheses (the discrete stand-in for the Recognition Composition Law). The first exact uniqueness blocker asks that every such cost factor through a multiplicative ratio character: $F(q)$ must be cross-equal to the cost reconstructed from $\chi$.
A parallel formulation, the trace-lift target, asks only that some ratio character realize the same doubled-trace data as $F$ (via PRCCharacterTraceMatchesCost). That is the exact d'Alembert trace-lift version of character factorization.
Upstream, cost_crossEq_of_PRCCharacterTraceMatchesCost already converts a trace match into pointwise cross-equality with costFromCharacter. The present theorem packages that conversion into an implication between the two target propositions.
proof idea
Term-mode unpack of the universal quantifiers. Fix an admissible $F$. Apply the trace-lift hypothesis to obtain a ratio character $\chi$ together with a trace-match witness. Feed that witness to cost_crossEq_of_PRCCharacterTraceMatchesCost, which yields $\forall q,,\mathrm{crossEq}(F(q),\mathrm{costFromCharacter}(\chi,q))$. Repackage $(\chi,\text{character proof},\text{crossEq})$ as the factorization witness. No extra analytic work.
why it matters
This is one half of the equivalence PRCNativeCostCharacterFactorizationTarget_iff_trace_lift, which identifies the discrete d'Alembert factorization blocker with its trace-lift form. Downstream wrappers route coherent-root and zero-calibrated doubled-trace hypotheses through this implication (..._of_doubled_trace_coherent_root, ..._of_doubled_trace_zero_calibrated), so any progress on those stronger targets immediately discharges the factorization target.
In the Recognition framework this is the discrete step toward J-uniqueness (forcing-chain T5) and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$: once every native cost factors through a ratio character, the cost is forced onto the standard $J$-shape. The theorem itself is pure glue; the remaining open work sits in establishing the trace-lift (or its coherent-root/zero-calibrated strengthenings).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.