reciprocal_character_prime_orientation_coherent
plain-language theorem explainer
The total reciprocal map on rational orbits is prime-orientation coherent: on every native prime direction it selects the reciprocal branch uniformly. Anyone assembling native cost characters or the uniqueness blocker certificate cites this. The proof is a one-line right-disjunct discharge via reflexivity of cross-equality after applying recip to each prime direction.
Claim. Let $\chi$ be the total reciprocal on ratio orbits, $\chi(q)=q^{-1}$ (with the zero-to-zero convention). Then $\chi$ is prime-axis orientation coherent: for every native prime orbit $p$, $\chi$ of the associated prime direction is cross-equal to the reciprocal of that prime direction (the uniform-reciprocal branch of the coherence disjunction).
background
In the primitive recognition calculus, ratio orbits package a signed integer numerator over a nonzero distinction-natural denominator, the discrete stand-in for positive rationals. The total reciprocal on ratio orbits mirrors $x\mapsto x^{-1}$ on $\mathbb{Q}$, sending the zero orbit to itself. Each native prime orbit determines a prime direction in ratio-orbit space.
Prime-axis orientation coherence for a character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ means $\chi$ does not mix orientations across primes: either $\chi$ fixes every prime direction (identity branch), or $\chi$ sends every prime direction to its reciprocal (reciprocal branch). Cross-equality is the balanced identification of ratio orbits used throughout the integer-rational layer; it is reflexive.
This sits inside native cost uniqueness: characters that generate costs must be coherently oriented on the prime axes before one can force agreement with the canonical $J$-cost.
proof idea
Discharge the right disjunct of orientation coherence. For an arbitrary native prime $p$ with primality witness, apply the reciprocal character to the prime direction and compare to the reciprocal of that same direction. The two sides are definitionally the same orbit, so crossEq_refl finishes. No case analysis on primes or nonzero checks is required beyond what recip already packages.
why it matters
Native cost uniqueness needs every admissible character to pick a single global orientation on the prime skeleton; mixed orientations would spawn non-canonical costs. This lemma certifies that the pure reciprocal character is admissible on that skeleton, feeding the blocker certificate prc_native_cost_uniqueness_blocker_certificate that packages zero-calibrated factorization targets and signed-admissible refutations.
In the broader forcing chain this is infrastructure under T5 $J$-uniqueness: the reciprocal involution is the dual-recognition symmetry the framework is built on, and coherent orientation ensures the discrete character layer cannot invent a second cost functional by flipping primes independently. Without this fact the uniqueness blocker cannot close the reciprocal branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.