PRCCharacterOrbitProductNoMixedOrientation
plain-language theorem explainer
Defines the product-level no-mixed-orientation property for a ratio-orbit character: nonunit factors of a nonunit product cannot be oriented one identity and one reciprocal. Native-cost uniqueness arguments cite it as the residual obstruction after same-orientation product algebra. It is a pure Prop abbreviation, not a proved theorem.
Claim. For a map $\chi$ on rational orbits, the following holds: whenever nonzero nonunit distinctions $a,b,p$ satisfy $a\cdot b=p$, it is not the case that $\chi$ orients $a$ by the identity branch and $b$ by the reciprocal branch, and not the case that $\chi$ orients $a$ by the reciprocal branch and $b$ by the identity branch.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12). Units are the trivial one-step orbits; nonunits carry genuine multiplicative content. Rational displays are RatioOrbit pairs (signed numerator over nonzero distinction denominator, K4.7).
A ratio-orbit character $\chi$ assigns to each display another display. Orientation of a nonzero orbit under $\chi$ is classified as identity branch or reciprocal branch (the reciprocal automorphism of cost algebra / ledger forcing swaps source and target and inverts the ratio). The identity event sits at the $J$-cost minimum $x=1$.
This module isolates native-cost uniqueness hypotheses. After pure same-orientation product algebra is discharged, the remaining obstruction is mixed identity/reciprocal orientation of product factors. The definition packages exactly that obstruction as a Prop on $\chi$.
proof idea
No proof: this is a def equating a name to a universal Prop. The body quantifies over nonzero nonunit distinctions $a,b,p$ with $a\cdot b=p$ and asserts the conjunction of two negated mixed-orientation conjunctions (identity-on-$a$ with reciprocal-on-$b$, and the swap), using the sibling direction predicates for identity and reciprocal branches.
why it matters
Doc-comment: product factors cannot be mixed identity/reciprocal oriented; this is the exact obstruction left after same-orientation product algebra. Downstream, it is equivalent to the nonunit no-mixed orientation predicate, is implied by nonunit orientation coherence (all nonunits identity, or all reciprocal), and by identity-branch transport. It feeds local orientation propagation under display compatibility, the native-cost uniqueness blocker certificate, and the prime-calibration target that forces the no-mixed product property. In the Recognition forcing chain this sits under native $J$-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), ruling out characters that would break reciprocal symmetry on composite orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.