PRCCharacterNonunitIdentityWitnessExcludesReciprocal
plain-language theorem explainer
Packages one-sided branch coupling for a ratio-orbit character: if any nonunit orbit carries an identity orientation witness, then no nonunit orbit may carry a reciprocal orientation witness. Cost-uniqueness and orientation-globalization arguments cite this Prop as the local exclusion hypothesis. The body is pure definitional packaging of that implication; no proof work lives here.
Claim. For a map $\chi$ on rational orbits, the following holds: if there exists a nonzero nonunit distinction $p$ at which $\chi$ is identity-oriented, then for every nonzero nonunit distinction $r$, $\chi$ is not reciprocal-oriented at $r$.
background
In the Primitive Recognition Calculus, distinctions are counted by a base-neutral inductive type (zero and successor). Nonzero distinctions that are not units label genuine nonunit orbits. Rational orbits package a signed numerator over a nonzero distinction denominator and serve as the domain of a character $\chi$, a self-map of rational orbits used to read cost and orientation.
Identity versus reciprocal orientation of $\chi$ at a distinction records which branch of the cost automorphism is active: the identity branch sits at the J-cost minimum (ratio $1$), while the reciprocal branch swaps source and target and inverts the ratio. Branch coupling is the demand that a single character not mix these two orientations across nonunit orbits.
This module develops native-cost uniqueness for such characters. The present definition isolates the one-sided exclusion form of coupling: existence of any identity-oriented nonunit witness already forbids every reciprocal-oriented nonunit witness. Local orientation data is deliberately not bundled into the statement.
proof idea
Definitional, not a theorem. The Prop is the implication from an existential identity-orientation witness (a nonzero nonunit distinction $p$ at which the character is identity-oriented) to the universal claim that no nonzero nonunit distinction $r$ can be reciprocal-oriented. The body simply writes that implication; downstream lemmas convert it to and from the symmetric no-mixed form and the globalization form.
why it matters
Native cost uniqueness needs a clean handle on branch coupling so that a character cannot simultaneously support identity and reciprocal nonunit witnesses. This definition is that handle in one-sided existential form.
It is equivalent to the symmetric no-mixed nonunit orientation predicate (via the two conversion lemmas and the iff), and it is implied by the existential no-mixed-witness form. Combined with local orientation, it yields globalization of an identity witness. Those bridges feed the uniqueness pipeline that forces the native cost to match the doubled-trace/J-cost side of the Recognition Composition Law, tying back to T5 J-uniqueness in the forcing chain.
Without this packaging, every uniqueness proof would re-inline the same exclusion quantifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.