PRCCharacterOrbitProductIdentityIdentity
plain-language theorem explainer
If a ratio-character is display-compatible with orbit products and fixes the directions of two nonzero factors, it fixes the direction of their product. Used when lifting prime-axis identity orientation to composite orbits in the native-cost uniqueness chain. The proof is a four-step cross-equivalence transit through multiplicativity and the orbit-product display law.
Claim. Let $\chi$ be a ratio-character on ratio-orbits that is compatible with the native display of orbit products. Let $a,b,p$ be nonzero finite distinction orbits with $a\cdot b=p$. If $\chi$ fixes the orbit direction of $a$ and of $b$ up to cross-equivalence, then $\chi$ fixes the orbit direction of $p$ up to cross-equivalence.
background
In the Primitive Recognition Calculus, nonzero positions live in DistinctionNat (the base-neutral finite orbit of repeated distinction). Each nonzero $p$ has an associated ratio direction orbitDirection p, a RatioOrbit with numerator the signed orbit of $p$ and denominator one. Cross-equivalence is the quotient-native equality on ratio-orbits (choice-free via the integer bridge).
A PRCRatioCharacter $\chi$ is a map on ratio-orbits that preserves the unit, is multiplicative, and respects reciprocals, all up to cross-equivalence rather than definitional equality. Identity orientation at $p$ means $\chi$ fixes orbitDirection p up to cross-equivalence; this is the composite-orbit form of the prime-axis identity condition used later for trace transport.
Display compatibility is the extra quotient-respect step: $\chi$ on the product orbit agrees with $\chi$ on the ratio-product of the factor directions. It is not automatic from the bare character axioms.
proof idea
Unfold identity orientation on both sides. Chain four cross-equivalences with crossEq_trans (and one crossEq_symm):
- Display compatibility: $\chi(\mathrm{dir},p)\sim\chi(\mathrm{dir},a\cdot\mathrm{dir},b)$.
- Character multiplicativity: $\chi(\mathrm{dir},a\cdot\mathrm{dir},b)\sim\chi(\mathrm{dir},a)\cdot\chi(\mathrm{dir},b)$.
- Congruence of the two factor identities: $\chi(\mathrm{dir},a)\cdot\chi(\mathrm{dir},b)\sim\mathrm{dir},a\cdot\mathrm{dir},b$.
- Symmetrized orbit-product law: $\mathrm{dir},a\cdot\mathrm{dir},b\sim\mathrm{dir},p$.
The composite is $\chi(\mathrm{dir},p)\sim\mathrm{dir},p$. Pure term-mode; no tactics beyond unfold and exact.
why it matters
This is the multiplicative closure step for identity orientation: primes that are fixed by $\chi$ generate fixed composite orbits once display compatibility is in hand. Downstream, PRCCharacterNonunitOrbitAllIdentity_of_all_prime_identity cites it to promote prime-axis identity to all nonunit orbits, and PRCCharacterOrbitProductLocalOrientationPropagates_of_display_compatible_nomix uses the same product logic for local orientation propagation.
Both feed the native-cost uniqueness blocker certificate in this module, which packages zero-calibrated factorization targets for the PRC cost. In the broader Recognition forcing chain, unique native cost is the bridge from the Recognition Composition Law and J-uniqueness (T5) toward the forced self-similar scale $\phi$ (T6). Without product-closure of identity orientation, character factorization cannot leave the prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.