PRCCharacterOrbitProductLocalOrientationPropagates_of_display_compatible_nomix
plain-language theorem explainer
If a ratio-orbit character is display-compatible on products and forbids mixed identity/reciprocal factor orientations, then local orientation multiplies: two nonunit locally oriented factors force their product orbit to be locally oriented. Cited by the prime-calibration orientation-coherence and product-local-orientation targets in native-cost uniqueness. Proof is four-way case split on the two local orientations, routing same-orientation cases to pure product lemmas and mixed cases to the no-mix hypothesis.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). Suppose $\chi$ is display-compatible on orbit products, and product factors cannot carry mixed identity/reciprocal local orientations. Then local orientation propagates under multiplication: whenever nonunit $a,b,p$ satisfy $a\cdot b=p$ and each of $a,b$ is locally identity- or reciprocal-oriented under $\chi$, the product $p$ is likewise locally oriented under $\chi$.
background
In the Primitive Recognition Calculus, costs are analyzed via d'Alembert-style factorization through ratio-orbit characters. A RatioOrbit is a rational display (signed numerator over nonzero distinction denominator). A ratio character $\chi$ maps orbits to orbits and, up to cross-equivalence, fixes the unit, multiplies, and sends reciprocals to reciprocals.
Local orientation of a nonunit distinction $a$ means $\chi$ sends the orbit direction of $a$ either to the identity display or to the reciprocal display. Product-local-orientation propagation is the multiplicative step that lifts prime-axis orientation to composite orbit directions: if two nonunit factors are each locally oriented, their product should be too.
Display compatibility is the missing quotient-respect condition: $\chi$ on the product orbit must agree (cross-equivalently) with $\chi$ on the ratio product of the factor orbits. No-mixed-orientation is the residual obstruction after pure same-orientation product algebra is settled: factors cannot be one identity-oriented and one reciprocal-oriented.
proof idea
Term-mode proof by introduction of the product data, then nested case splits on the two local-orientation disjunctions for $a$ and $b$.
- Both identity: apply the identity-identity product theorem (character + display compatibility) to conclude the product is identity-oriented, hence left disjunct of the goal.
- $a$ identity and $b$ reciprocal: the no-mixed-orientation hypothesis's first conjunct yields absurdity on that pair; eliminate.
- $a$ reciprocal and $b$ identity: likewise, the second conjunct of no-mixed-orientation eliminates.
- Both reciprocal: apply the reciprocal-reciprocal product theorem to conclude the product is reciprocal-oriented, hence right disjunct.
No further arithmetic; the pure same-orientation algebra and the mixed-orientation ban do all the work.
why it matters
Native-cost uniqueness needs orientation coherence on all nonunit orbits, not just primes. This lemma is the exact multiplicative bridge: once primes are oriented and products neither mix orientations nor break display compatibility, composites inherit local orientation.
Downstream it is applied directly in the prime-calibration force theorems that discharge the nonunit product-local-orientation target (both the display-compatible/no-mix route and the identity-comparable-trace route), and in the orientation-coherence target derived from product no-mix. Those feed the native-cost uniqueness blocker certificate, which packages the zero-calibrated factorization target and the refutation of signed-admissible alternatives.
In the broader RS forcing picture this sits under uniqueness of the native cost (the J-cost side of T5), ensuring character factorizations cannot wander in orientation when climbing the multiplicative monoid of distinction naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.