PRCCharacterPositiveOrbitReciprocal_of_all_prime_reciprocal
plain-language theorem explainer
If a quotient-native ratio character sends every prime orbit direction to its reciprocal, then it does so for every nonzero orbit direction. Cost-uniqueness arguments cite this to globalize the reciprocal branch from the prime generators. The proof splits on units versus nonunits: units reduce to the character's unit axiom via cross-equivalence, and nonunits invoke the prime-factorization reciprocal lemma.
Claim. Let $\chi$ be a ratio-orbit character that is multiplicative, fixes the unit orbit, 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 the reciprocal of that direction (up to cross-equivalence). Then for every nonzero distinction $p$, $\chi$ sends the orbit direction of $p$ to the reciprocal of that direction (up to cross-equivalence).
background
In the Primitive Recognition Calculus, rational data live as RatioOrbit displays: a signed numerator orbit over a nonzero distinction denominator. Equality is not definitional; it is the internal cross-multiplication relation crossEq, which matches rational equality of verifier displays (crossEq_iff_toRat_eq). Reciprocals are total on ratio orbits, sending zero to zero as in $\mathbb{Q}$.
A PRCRatioCharacter is a candidate factor for the d'Alembert factorization of a PRC cost at the ratio-orbit level: it fixes the unit orbit, is multiplicative under orbit multiplication, and interacts with reciprocals, all up to crossEq rather than definitional equality. Two extra hypotheses make a raw map quotient-native: it must respect crossEq on inputs, and it must be compatible with the native display of an orbit product (character on the product orbit agrees with character on the ratio product of factor orbits).
The target property PRCCharacterOrbitDirectionReciprocal asserts that on the positive direction of a nonzero distinction $p$, the character lands on the reciprocal of that direction. The hypothesis supplies this only on prime directions; the theorem globalizes it to every nonzero orbit direction.
proof idea
Case split on whether $p$ is a unit distinction.
If $p$ is a unit, unit_iff_toNat_eq_one plus crossEq_iff_toRat_eq shows the orbit direction is cross-equivalent to the unit orbit, and the unit orbit is cross-equivalent to the reciprocal of that direction (via one_toRat, recip_toRat, and a norm_num identity). Apply character respect for crossEq to move $\chi$ across the first equivalence, use the character's unit axiom $\chi(1)\sim 1$, and close by crossEq_trans.
If $p$ is nonunit, discharge by the upstream lemma PRCCharacterNonunitOrbitAllReciprocal_of_all_prime_reciprocal, which uses multiplicativity, product-display compatibility, and the prime-reciprocal hypothesis on a prime factorization of $p$.
why it matters
Native-cost uniqueness in PRC proceeds by identifying the cost with a doubled-trace d'Alembert factorization built from a ratio character. Reciprocal orientation on orbit directions is part of pinning that character to the geometric reciprocal branch rather than a twisted alternative.
This lemma is the orbit-direction step: primes generate the reciprocal condition, and it lifts to every nonzero positive direction. The sole downstream consumer is PRCCharacterPositiveRatioReciprocal_of_all_prime_reciprocal, which extends the same conclusion from orbit directions to general positive ratio orbits. Together they feed the uniqueness pipeline for the native PRC cost (J-cost side of the Recognition Composition Law and the T5 J-uniqueness landmark), ensuring the character used in cost reconstruction is the reciprocal character on the positive cone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.