PRCCharacterNonunitNoMixedWitnesses
plain-language theorem explainer
For a ratio-orbit character χ, identity-oriented and reciprocal-oriented nonunit witnesses cannot coexist. Anyone proving native cost uniqueness or prime-to-composite witness control cites this packing of branch coupling. The body is a pure Prop definition: negation of the joint existence of both witness kinds.
Claim. A map $\chi$ from ratio orbits to ratio orbits has no mixed nonunit witnesses when it is impossible that both (i) some nonzero nonunit distinction orbit is identity-oriented under $\chi$ and (ii) some nonzero nonunit distinction orbit is reciprocal-oriented under $\chi$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed orbit numerator over a nonzero finite distinction denominator. DistinctionNat is the base-neutral finite orbit of repeated distinction; its only multiplicative unit is the one-step orbit.
A character $\chi$ acts on ratio orbits. Identity orientation at a nonzero orbit direction $p$ means $\chi$ fixes that direction up to the native cross-equality; reciprocal orientation means $\chi$ sends it to its reciprocal. These orientations are stated for arbitrary nonzero orbits, not only primes, so trace transport can pass through composite positions.
The local module develops uniqueness of the native cost from character data. Branch coupling is the demand that $\chi$ not mix identity and reciprocal orientations across witnesses. This definition packages that demand in existential form over all nonunit witnesses.
proof idea
No proof: this is a Prop-valued definition. The body is the negation of a conjunction of two existentials. The first existential asserts a nonzero nonunit distinction orbit at which $\chi$ is identity-oriented; the second asserts a nonzero nonunit distinction orbit at which $\chi$ is reciprocal-oriented. Unfolding therefore reduces any use site to ordinary classical logic on those two witness predicates.
why it matters
This is the composite-side packing of branch coupling after primes are isolated. Downstream, it is equivalent to the exclusion form "any identity nonunit witness rules out every reciprocal nonunit witness," and it is the conclusion of the bridge "prime no-mixing controls arbitrary nonunit witnesses."
It is also the target that prime calibration is asked to force for every ratio character: once primes are calibrated, no mixed nonunit witnesses should remain. That target sits on the path from character data to native cost uniqueness in the PRC forcing stack, which feeds the J-uniqueness landmark (T5) and the Recognition Composition Law by locking the cost character to a single orientation branch.
Parent uses include the prime-witness specialization, the iff with identity-excludes-reciprocal, and the prime-calibration forces-nonunit-no-mix target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.