PRCNativeCostCharacterFactorizationTarget_iff_trace_lift
plain-language theorem explainer
The discrete character-factorization blocker for PRC-native RCL costs is equivalent to its exact d'Alembert trace-lift form. Anyone attacking native-cost uniqueness can switch freely between the two formulations. The proof is a two-line constructor applying the already-proved one-way implications in each direction.
Claim. Every admissible PRC-native RCL cost $F$ factors through a ratio character $\chi$ (so $F(q)$ is cross-equal to the character-induced cost at every ratio orbit $q$) if and only if every such $F$ admits a ratio character $\chi$ whose doubled trace matches $F$.
background
In the Primitive Recognition Calculus, admissible native costs on ratio orbits are maps $F$ satisfying a package of RCL-style hypotheses (normalization, symmetry, and the discrete composition law descending from $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$). The classical continuous solution is the T5 cost $J(x)=(x+x^{-1})/2-1$.
The first exact blocker asks that any such $F$ factor through a multiplicative ratio character $\chi$: there exists $\chi$ with $F(q)$ cross-equal to the cost built from $\chi$ at every orbit $q$. The trace-lift blocker is the exact d'Alembert version of the same demand: $\chi$ must be a ratio character whose doubled trace realizes $F$. Both live in the native-cost uniqueness module and are the discrete stand-ins for the classical d'Alembert factorization of $J$.
proof idea
Pure bidirectional packaging. constructor splits the biconditional. The forward direction is the existing lemma that factorization implies the trace-lift target; the reverse is the existing lemma that the trace-lift target implies factorization. No new algebra is done here.
why it matters
Native-cost uniqueness is the discrete counterpart of T5 J-uniqueness inside the PRC stack. The factorization target is documented as the first exact blocker (discrete d'Alembert factorization); the trace-lift target is its exact doubled-trace form. Equating them lets later work discharge either formulation without loss.
No downstream consumers are wired yet (used_by is empty), but the next documented blocker in the same module demands that a calibrated rational character cost collapse to the canonical identity character, eliminating prime-direction freedom. Closing either side of this iff is a prerequisite for that collapse and for the full uniqueness theorem that pins the native cost to the identity-character $J$-form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.