PRCCharacterNonunitNoMixedWitnesses_iff_identity_witness_excludes
plain-language theorem explainer
The existential no-mixed-nonunit-witness form of branch coupling for a ratio-orbit character is equivalent to the one-sided rule that any identity-oriented nonunit witness excludes every reciprocal-oriented nonunit witness. Native-cost uniqueness arguments cite this to switch formulations without changing content. The proof is a pure Iff constructor from the two directed lemmas.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) there do not simultaneously exist a nonunit identity-oriented witness and a nonunit reciprocal-oriented witness for $\chi$; (ii) if any nonunit identity-oriented witness for $\chi$ exists, then no nonunit reciprocal-oriented witness can exist.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-natural denominator (K4.7). Characters here are maps $\chi$ on ratio orbits. Branch coupling constrains how such a character can orient nonunit distinction naturals: identity-oriented versus reciprocal-oriented witnesses must not mix.
Two Prop packages encode that constraint. The existential form asserts that one cannot have both a nonunit identity witness and a nonunit reciprocal witness at once. The one-sided form asserts that the mere existence of any nonunit identity witness forces every candidate nonunit reciprocal witness to fail. Local orientation data is deliberately not bundled into either statement.
This module develops uniqueness of the native cost built from character and doubled-trace data (siblings such as cost-from-character and native-cost doubled trace). The present declaration only equates the two branch-coupling packages so later uniqueness steps can pick the more convenient shape.
proof idea
Term-mode Iff pair, no tactics. The forward arrow is the already-proved lemma that no-mixed-witnesses implies identity-excludes-reciprocal (introduces an identity witness and a reciprocal witness, then feeds their pair into the negated conjunction). The reverse arrow is the dual lemma that identity-excludes-reciprocal implies no-mixed-witnesses (destructs a mixed pair and applies the exclusion hypothesis). The theorem is exactly $\langle$forward, reverse$\rangle$.
why it matters
Branch coupling is a gate on admissible characters before native cost can be identified with the unique J-type cost on ratio data. Equating the existential and one-sided packages means uniqueness proofs may assume whichever form matches the ambient quantifier structure, without a separate conversion argument at each use site.
No downstream consumers are recorded yet; the declaration sits as a local bridge inside PRC native-cost uniqueness, beside character-trace matching and doubled-trace d'Alembert hypotheses. In the broader forcing chain it supports the T5 J-uniqueness lane: once characters are forced not to mix identity and reciprocal nonunit witnesses, the cost extracted from $\chi$ is pinned to the canonical $J(x)=(x+x^{-1})/2-1$ shape rather than a mixed-orientation impostor.
It closes no open scaffold; it only collapses two already-proved directed implications into a single reusable equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.