PRCCharacterPositiveRatioReciprocal_of_all_prime_reciprocal
plain-language theorem explainer
If a ratio-orbit character is reciprocal on every prime direction, then it is reciprocal on every positive rational ratio n/d (nonzero numerator and denominator), up to cross-equivalence. Cost-uniqueness and signed-orientation arguments cite this to lift prime-level reciprocity to the full positive rational group. The proof multiplies the already-proved positive-orbit reciprocal lemmas for n and d and rearranges with the character's multiplicativity and double-reciprocal identities.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence) that respects cross-equivalence and is compatible with native orbit-product displays. Suppose that for every prime distinction $p$, $\chi$ sends the prime direction of $p$ to its reciprocal (cross-equivalent). Then for all nonzero distinctions $n,d$, $\chi$ sends the ratio orbit of $n/d$ to the reciprocal of that same ratio orbit (again up to cross-equivalence).
background
In the Primitive Recognition Calculus, ratios live as RatioOrbit displays rather than bare rationals. Two displays are identified by cross-equivalence: numerators and denominators balance after cross-scaling of signed orbits. A ratio character $\chi$ is a map on ratio orbits that is unit at one, multiplicative under orbit multiplication, and intertwines reciprocal, all stated with cross-equivalence so the interface stays quotient-native.
Two extra hypotheses close the quotient gap: the character must send cross-equivalent inputs to cross-equivalent outputs, and its value on a native product orbit must match its value on the ratio product of the factor orbits. Reciprocal here means the character flips direction the way the cost algebra's reciprocal automorphism does on positive reals, and the way ledger reciprocal events invert recognition ratios.
The local module builds native-cost uniqueness via d'Alembert factorization of PRC costs. The prime-level reciprocal hypothesis is the seed; this theorem extends it from prime directions to arbitrary positive rational ratios built as $n\cdot d^{-1}$.
proof idea
Term-mode proof by chaining cross-equivalence steps.
First apply the sibling lemma that already lifts prime reciprocity to every positive orbit direction, once for $n$ and once for $d$, obtaining $\chi(n)\sim n^{-1}$ and $\chi(d)\sim d^{-1}$.
From the character's built-in reciprocal law plus congruence of reciprocal and double-reciprocal cancellation, deduce $\chi(d^{-1})\sim d$.
Separately rearrange products: $n^{-1}\cdot d$ is cross-equivalent to $(n\cdot d^{-1})^{-1}$ via mul-congruence, double-reciprocal, and the mul-recip identity.
Finally multiply: multiplicativity gives $\chi(n\cdot d^{-1})\sim\chi(n)\cdot\chi(d^{-1})$, substitute the two reciprocal facts, and finish with the product rearrangement.
why it matters
Native PRC cost uniqueness needs a global reciprocal character on positive ratios, not merely on primes. This lemma is the rational-ratio step in that lift: once primes are reciprocal, every positive $n/d$ is reciprocal under $\chi$.
Its sole recorded consumer is PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved, which asserts that signed coherent prime orientation propagates to the global target. That parent opens by recovering cross-equivalence respect from the normalize-ratio canonical target, then uses reciprocal propagation of this kind to move from prime orientations to arbitrary ratio orbits.
In the broader Recognition chain this sits under cost uniqueness for the J-cost factorization (T5 landmark: $J(x)=(x+x^{-1})/2-1$), where characters play the role of the reciprocal automorphism in the cost algebra. Closing prime-to-global reciprocity is a necessary algebraic step before uniqueness of the native doubled-trace cost can be stated without residual orientation choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.