PRCCharacterOrbitProductReciprocalReciprocal
plain-language theorem explainer
If a ratio character is display-compatible with orbit products, reciprocal orientation on two nonzero factors transfers to their product: χ on the product direction matches the reciprocal of that direction. Cited when closing reciprocal-branch globalization from primes to composite orbits in native cost uniqueness. The proof is a short crossEq chain through multiplicativity, display compatibility, and reciprocal-of-product identities.
Claim. Let $\chi$ be a ratio character (unit, multiplicative, and reciprocal up to cross-equivalence on ratio orbits) that is display-compatible with orbit products. For nonzero distinction orbits $a,b,p$ with $a\cdot b=p$, if $\chi$ sends the direction of $a$ and of $b$ each to the reciprocal of that direction (up to cross-equivalence), then $\chi$ sends the direction of $p$ to the reciprocal of the direction of $p$.
background
In the Primitive Recognition Calculus, nonzero positions live in DistinctionNat (finite repeated-distinction orbits). Each nonzero $p$ has an orbitDirection: the ratio orbit with numerator the signed orbit of $p$ and denominator one. Ratio orbits are compared by crossEq, a choice-free balanced equivalence rather than definitional equality.
A PRCRatioCharacter is a map $\chi$ on ratio orbits that is a unit-preserving, multiplicative, reciprocal candidate for the d'Alembert factorization of a PRC cost, all stated via crossEq. Display compatibility (PRCCharacterOrbitProductDisplayCompatible) is the extra quotient-respect step: $\chi$ on the product orbit direction agrees with $\chi$ on the ratio product of the factor directions. Reciprocal orientation on a direction means $\chi(\mathrm{dir},p)\sim\mathrm{recip}(\mathrm{dir},p)$.
The local setting is native cost uniqueness: characters that could factor the native cost must have controlled orientation on orbit directions so the cost is forced to the unique $J$-shape.
proof idea
Unfold the reciprocal-orientation goal to a single crossEq. Chain five equivalences with crossEq_trans:
- Display compatibility equates $\chi(\mathrm{dir},p)$ with $\chi(\mathrm{dir},a\cdot\mathrm{dir},b)$.
- Character multiplicativity equates that with $\chi(\mathrm{dir},a)\cdot\chi(\mathrm{dir},b)$.
- Congruence of multiplication under the two reciprocal hypotheses replaces the factors by $\mathrm{recip}(\mathrm{dir},a)\cdot\mathrm{recip}(\mathrm{dir},b)$.
- The algebraic identity that product of reciprocals is reciprocal of product (up to
crossEq) yields $\mathrm{recip}(\mathrm{dir},a\cdot\mathrm{dir},b)$. - Reciprocal congruence plus symmetry of
orbitDirection_mul_crossEqidentifies that with $\mathrm{recip}(\mathrm{dir},p)$.
No case split; pure transitive glue of already-proved orbit identities.
why it matters
Reciprocal orientation must close under multiplication before it can globalize from primes to every nonunit orbit. Downstream, PRCCharacterNonunitOrbitAllReciprocal_of_all_prime_reciprocal uses this product rule to lift prime-axis reciprocal data to all composites. The same lemma feeds PRCCharacterOrbitProductLocalOrientationPropagates_of_display_compatible_nomix, which packages local orientation propagation under a no-mixed-orientation hypothesis.
Both sit on the path to prc_native_cost_uniqueness_blocker_certificate, the certificate that zero-calibrated native-cost character factorization is settled (proved target, signed-admissible branch refuted). In the broader RS forcing picture this is bookkeeping toward T5 $J$-uniqueness: only the reciprocal-consistent character branch survives as a cost factor, matching $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law. Without product closure, prime witnesses would not force the full reciprocal branch on the orbit lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.