reciprocal_character_global_orientation
plain-language theorem explainer
The reciprocal map on ratio orbits has global cost orientation: every orbit lands on itself or on its reciprocal (up to cross-equality). Native-cost uniqueness arguments that need a coherent orientation on rational directions cite this fact. The proof is a one-line right-disjunct: reflexivity of cross-equality on the reciprocal image.
Claim. The reciprocal map $q \mapsto q^{-1}$ on ratio orbits has global cost orientation: for every ratio orbit $q$, either the image is cross-equal to $q$, or it is cross-equal to $q^{-1}$.
background
In the primitive recognition calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Its total reciprocal sends zero to zero and otherwise inverts, matching the usual reciprocal on $\mathbb{Q}$.
A character $\chi$ on ratio orbits has global cost orientation when, for every $q$, $\chi(q)$ is cross-equal either to $q$ or to $q^{-1}$. The module doc for that predicate states the reason: "Since J-cost is reciprocal-symmetric, this is exactly the orientation information needed for cost propagation." Cross-equality is the balanced identification of orbits; it is reflexive by a short unfold to signed-orbit balance.
The ambient setting is native cost uniqueness for PRC characters: orientation must be coherent globally so that prime-level calibration cannot invert primes independently while preserving prime costs and breaking composites.
proof idea
Fix an arbitrary ratio orbit $q$. Global cost orientation for the reciprocal map asks for the disjunction: reciprocal image cross-equal to $q$, or reciprocal image cross-equal to the reciprocal of $q$. Take the right branch and apply reflexivity of cross-equality to $\mathrm{recip}(q)$. No case split on zero or nonzero is required.
why it matters
This pins the canonical dual-recognition map (the reciprocal involution) as an oriented character in the sense needed for cost propagation. Downstream it is consumed by the native cost uniqueness blocker certificate, which packages zero-calibrated factorization targets and refutations of signed-admissible factorizations.
In the broader Recognition chain this is orientation infrastructure under J-uniqueness (T5): $J(x)=(x+x^{-1})/2-1$ is reciprocal-symmetric, and the Recognition Composition Law encodes that symmetry. Without a global orientation lemma, independent prime inversions can preserve prime costs while breaking composite costs; the sharper propagation blocker in the orientation predicate's doc-comment is exactly that gap. The result is a proved, zero-sorry orientation witness rather than a hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.