PRCCoherentPrimeOrientationPropagatesToGlobalTarget
plain-language theorem explainer
Packages the assertion that every multiplicative ratio character with coherent orientation on prime axes automatically has global cost orientation (identity or reciprocal at every ratio). Native-cost uniqueness proofs cite it as sharper orientation blocker B. The body is a pure Prop abbreviation; no proof is attached, and a sibling theorem already refutes the claim via the absolute-value character.
Claim. For every map $\chi$ from ratio orbits to ratio orbits: if $\chi$ is a multiplicative ratio character and is orientation-coherent on every prime axis, then $\chi$ has global cost orientation (at each ratio orbit, $\chi$ acts as the identity or the reciprocal).
background
In the Primitive Recognition Calculus native-cost uniqueness module, cost functionals are recovered from multiplicative characters on ratio orbits. A ratio character is a multiplicative map on those orbits; cost is read off via the J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$).
Orientation asks whether the character acts pointwise as the identity event or the reciprocal event (the ledger swap that inverts the recognition ratio). Prime orientation coherence means this identity-or-reciprocal choice is already fixed on every positive prime axis. Global cost orientation demands the same choice at every ratio orbit, including signed units.
The reciprocal automorphism of the cost algebra and the reciprocal recognition event supply the two allowed local orientations. This definition isolates the pure propagation step from prime axes to the full orbit set.
proof idea
Definitional packaging only: the declaration is a Prop abbreviation equal to the universal statement that every ratio character with coherent prime orientation already has global cost orientation. There is no tactic proof and no lemma application inside the body.
why it matters
This is sharper orientation blocker B in the native-cost uniqueness program. Downstream wrappers turn it into admissible global-orientation and rigidity targets (e.g. global orientation from prime coherence plus this propagation, and the corresponding admissible-character rigidity targets). The Pass-25 uniqueness blocker certificate records the split of missing mathematics into exact Lean targets of this shape.
A sibling already refutes the bare claim: the absolute-value character is prime-orientation coherent yet sends $-1$ to $+1$, so global orientation fails at the signed unit. The repaired path therefore demands signed-unit calibration before asking for pointwise identity-or-reciprocal orientation. In the broader RS chain this sits under cost uniqueness for the J-functional (T5), not under the later geometric forcing steps T6–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.