PRCAdmissibleCharacterGlobalOrientationTarget
plain-language theorem explainer
Every ratio character meeting the repaired admissibility interface is required to be globally identity- or reciprocal-oriented pointwise. Native-cost uniqueness and admissible-character rigidity cite this Prop as the orientation bottleneck after valuation twists are excluded. The declaration is a pure universal packaging of that claim, not a proved theorem.
Claim. For every map $\chi$ from rational orbits to rational orbits, if $\chi$ is admissible (ratio-character laws, prime calibration, and prime-pair product cost consistency), then $\chi$ has global cost orientation: for every rational orbit $q$, either $\chi(q)$ is cross-equal to $q$ or cross-equal to the reciprocal of $q$.
background
In the Primitive Recognition Calculus, rational directions are packaged as ratio orbits: a signed integer numerator over a nonzero distinction-natural denominator. Characters act as maps on these orbits. The J-cost is reciprocal-symmetric, so the only orientation data needed for cost propagation is whether each direction is sent to itself or to its reciprocal.
After a two-adic countermodel, admissibility was repaired. An admissible ratio character must obey the ratio-character laws, be prime-direction calibrated, and keep prime-pair product costs consistent. That interface still allows the two global orientations (identity and reciprocal) but excludes valuation twists.
Global cost orientation is the pointwise statement that every rational orbit is mapped either to a cross-equal copy of itself or to its reciprocal. The present definition simply asserts that every admissible character has that property.
proof idea
Definitional packaging only: the body is the universal quantification that every admissible ratio character satisfies global cost orientation. No tactics, no lemmas applied, no proof obligation discharged here. Downstream theorems supply concrete hypotheses (prime-coherence plus propagation, signed unit calibration, etc.) that imply this Prop.
why it matters
This is the orientation bottleneck in the repaired native-cost uniqueness chain. Admissible-character rigidity is reduced to it: once every admissible character is globally identity- or reciprocal-oriented, cost agreement on ratio orbits follows by reciprocal symmetry of J. Downstream, the rigidity target is obtained directly from this Prop, and the strengthened native-cost uniqueness target consumes it together with character factorization and two-calibration.
Several discharge routes exist in-module: global propagation of coherent prime orientation; the same with an explicit prime-coherence hypothesis; signed global propagation; and signed unit calibration. In the broader Recognition forcing picture this sits under T5 J-uniqueness and the Recognition Composition Law: characters that preserve cost must not introduce orientation defects that would break the unique J-cost on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.