PRCCharacterPositiveRatioIdentity_of_all_prime_identity
plain-language theorem explainer
If a ratio-orbit character is multiplicative, reciprocal, quotient-respecting, product-display compatible, and fixes every prime direction under cross-equivalence, then it fixes every positive rational direction n/d. Cost-uniqueness and signed-orientation arguments cite this to lift prime-level identity to all positive ratios. The proof applies the positive-orbit identity lemma to numerator and denominator, then closes with reciprocal and multiplicative character laws plus crossEq congruence.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal under cross-equivalence) that respects cross-equivalence and is compatible with native orbit-product displays. Suppose that for every prime distinction orbit $p$, $\chi$ fixes the prime direction of $p$ up to cross-equivalence. Then for all nonzero distinction orbits $n,d$, $\chi$ fixes the ratio direction $n/d$ up to cross-equivalence: $\chi(n\cdot d^{-1})\sim n\cdot d^{-1}$.
background
In the Primitive Recognition Calculus, rational displays live as RatioOrbit objects: a signed numerator orbit over a nonzero distinction-orbit denominator. Equality is not definitional; it is the internal cross-multiplication relation crossEq (K4.10), balancing scaled signed orbits without leaving the $\delta$-orbit language.
A PRCRatioCharacter is a candidate factor map $\chi$ on ratio orbits for the d'Alembert factorization of a PRC cost. It is quotient-native: unit, multiplicativity, and reciprocity are stated with crossEq rather than =. Two extra hypotheses close the gap between a raw function and a true quotient map: respect for crossEq, and compatibility of $\chi$ on a product orbit with $\chi$ on the ratio product of the factor orbits.
The local module develops native-cost uniqueness: characters that match the cost on primes should match it globally. The immediate upstream step is the positive-orbit identity lemma (same prime-fix package implies $\chi$ fixes every nonzero orbit direction), which this result extends from pure orbits to ratios $n/d$.
proof idea
Term-mode composition of three cross-equivalence steps.
First apply PRCCharacterPositiveOrbitIdentity_of_all_prime_identity to $n$ and to $d$, obtaining $\chi(\mathrm{dir},n)\sim\mathrm{dir},n$ and $\chi(\mathrm{dir},d)\sim\mathrm{dir},d$.
For the reciprocal factor, chain the character reciprocity law $\chi(\mathrm{recip},x)\sim\mathrm{recip}(\chi,x)$ with congruence of recip under the identity on $d$, yielding $\chi(\mathrm{recip},\mathrm{dir},d)\sim\mathrm{recip},\mathrm{dir},d$.
Finally apply character multiplicativity on $\mathrm{dir},n$ and $\mathrm{recip},\mathrm{dir},d$, then congruence of mul under the two identities already proved. Transitivity of crossEq glues the chain.
why it matters
This is the ratio-level half of the prime-to-global identity ladder for PRC characters. Downstream, PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved uses it (with signed coherence and normalize-ratio canonicity) to show that a signed-coherent prime orientation on $\chi$ propagates to every global target ratio orbit.
In the Recognition framework this sits inside native-cost uniqueness for the Primitive Recognition Calculus: the cost factor that appears in the d'Alembert / J-cost story must be the identity character once it is pinned on primes. That uniqueness feeds the forcing chain's J-uniqueness landmark (T5: $J(x)=(x+x^{-1})/2-1$) by ensuring the PRC-side factorization cannot introduce a second independent multiplicative character on positive ratios.
No scaffolding remains on this lemma itself; it is a proved bridge from prime identity to all positive rational directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.