PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved
plain-language theorem explainer
A ratio-orbit character that is multiplicative, signed-unit calibrated, and coherent on primes extends to a global identity-or-reciprocal orientation on every ratio orbit. Cost-uniqueness and admissible-character arguments cite this as the repaired propagation step after the absolute-value countermodel. The proof case-splits on zero, positive, and negative rational displays and pushes prime coherence through cross-equivalence and multiplicativity.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose $\chi$ is a PRC ratio character, is calibrated on the signed unit (so $\chi(-1)\sim -1$ under cross-equivalence), and is prime-orientation coherent (on every prime direction it acts either as the identity everywhere or as reciprocal everywhere). Then for every ratio orbit $q$, either $\chi(q)\sim q$ or $\chi(q)\sim q^{-1}$ under cross-multiplication equivalence.
background
Primitive Recognition Calculus works with ratio orbits: pairs of signed $\delta$-orbits standing in for rational displays. Cross-equivalence crossEq is the internal relation that two orbits balance under cross-multiplication of numerator and denominator scales; it agrees with equality of the rational verifier displays (crossEq_iff_toRat_eq).
A PRC ratio character is a multiplicative map on this monoid of orbits. Global cost orientation means that at every orbit the character is cross-equivalent either to the identity or to reciprocal. Prime-orientation coherence is the weaker demand that this dichotomy holds uniformly on prime directions. Signed-unit calibration fixes the image of the negative unit orbit, which absolute-value characters can flip.
The module targets native $J$-cost uniqueness for admissible characters. The repaired target (after an absolute-value countermodel) requires signed-unit calibration before coherent prime orientation can be asked to imply global pointwise identity-or-reciprocal orientation.
proof idea
Fix $\chi$ with the three hypotheses and an arbitrary orbit $q$. First obtain that $\chi$ respects cross-equivalence (from the proved normalize-ratio canonical target) and is orbit-product display compatible.
If $q$ displays as $0$, prime-coherent characters send zero to zero; transport by cross-equivalence gives the identity branch.
If $q\neq 0$, invoke the signed ratio decomposition: $q$ is cross-equivalent to a positive fraction of orbit-directions, or to that fraction times the negative unit. On the positive piece, prime coherence (all-identity or all-reciprocal) lifts by the positive-ratio identity/reciprocal lemmas. On the negative piece, multiplicativity of $\chi$ plus signed-unit calibration multiplies the positive conclusion by $-1$, using reciprocal-congruence and the self-reciprocal law for the negative unit, then transport back along the decomposition.
why it matters
This is the exact repaired orientation bridge in native cost uniqueness: coherent primes plus signed-unit calibration yield global cost orientation. Downstream, PRCSignedAdmissibleRatioCharacter_global_orientation applies it directly to signed-admissible characters, and PRCAdmissibleCharacterGlobalOrientationTarget_of_signed_unit_calibration packages the admissible-interface form.
It feeds the native-cost uniqueness blocker certificate and, one layer up, the conditional universal-foundation certificate. In the forcing chain this sits under T5 $J$-uniqueness: characters that could seed a cost must be globally oriented as id or reciprocal before the Recognition Composition Law and the unique $J(x)=\cosh(\log x)-1$ can be forced. The absolute-value countermodel forced the signed-unit repair; this theorem closes that gap on the propagation side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.