PRCNativeCostCharacterTraceLiftTarget_of_factorization
plain-language theorem explainer
Factorization of every admissible PRC-native RCL cost through a ratio character implies the exact d'Alembert trace-lift form of that factorization. Cited by anyone equating or refuting the two native-cost uniqueness blockers. Proof unpacks the factorization witness and upgrades pointwise cost cross-equality to character-trace matching via one conversion lemma.
Claim. If every map $F$ on ratio orbits satisfying the PRC-native cost hypotheses factors through some ratio character $\chi$ so that $F(q)$ is cross-equal to the cost reconstructed from $\chi$ at every orbit $q$, then every such $F$ also admits a ratio character whose trace matches the cost of $F$ (the exact d'Alembert trace-lift target).
background
Primitive Recognition Calculus treats native costs on ratio orbits under the Recognition Composition Law (RCL). The discrete d'Alembert factorization demand is that any admissible native cost $F$ arise from a multiplicative ratio character $\chi$ via the standard cost-from-character reconstruction.
Two packaged targets state that demand. The factorization target asks for a character with pointwise cross-equality between $F(q)$ and the reconstructed cost. The trace-lift target keeps the same character existence but replaces the matching condition by character-trace matching, the form used in doubled-trace d'Alembert analysis.
The only nontrivial upstream step is the conversion that turns pointwise cost cross-equality into character-trace matching. Both targets quantify over maps satisfying the native cost hypotheses; this theorem relates the two residual goals without discharging those hypotheses.
proof idea
Short tactic proof, essentially a one-step upgrade of witnesses. Introduce an admissible native cost $F$. Apply the factorization hypothesis to obtain a ratio character $\chi$ together with pointwise cross-equality of $F$ against the character-derived cost. Pass that equality to the conversion lemma that turns cost cross-equality into character-trace matching, then reassemble the existential package required by the trace-lift target.
why it matters
One half of the equivalence between the factorization blocker and the trace-lift blocker. Downstream, the iff theorem uses this direction as its forward arrow, and the refutation of factorization reduces immediately to the already-refuted trace-lift target by applying this implication. In the Recognition foundation stack these blockers sit on the path to uniqueness of the native J-cost (T5 J-uniqueness under the RCL), so identifying the two formulations prevents the uniqueness campaign from splitting into inequivalent residual goals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.