PRCCharacterNonunitIdentityWitnessExcludesReciprocal_of_globalizes
plain-language theorem explainer
If a ratio-orbit character has the property that one nonunit identity-oriented witness forces every nonunit orbit to be identity-oriented, then that same witness already rules out any nonunit reciprocal orientation. Branch-coupling arguments in the native-cost uniqueness chain cite this implication. The proof is a short term argument: globalize the identity witness, transport via cross-equivalence symmetry and transitivity, and contradict the fact that a nonunit direction is never cross-equivalent to its reciprocal.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever some nonunit nonzero distinction $p$ is identity-oriented under $\chi$, every nonunit nonzero distinction is identity-oriented under $\chi$. Then whenever some nonunit nonzero distinction is identity-oriented under $\chi$, no nonunit nonzero distinction can be reciprocal-oriented under $\chi$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction denominator. Two such displays are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality). The total reciprocal recip sends zero to zero and otherwise inverts a nonzero ratio orbit.
Each nonzero distinction $r$ has an associated direction orbitDirection r, the ratio with numerator the signed orbit of $r$ and denominator one. Characters $\chi$ act on ratio orbits; identity versus reciprocal orientation of a direction records which branch of the character the orbit sits on.
PRCCharacterNonunitIdentityWitnessGlobalizes is the witness form of identity-branch transport: one identity-oriented nonunit direction, if it exists, fixes the identity branch globally. PRCCharacterNonunitIdentityWitnessExcludesReciprocal is the one-sided exclusion form: once any nonunit identity witness exists, no nonunit reciprocal witness can coexist with it. Local orientation is not bundled into that statement.
proof idea
Term-mode proof by contradiction on the exclusion goal. Assume an identity witness exists and that some nonunit $r$ is reciprocal-oriented. Apply the globalizes hypothesis to that witness to conclude $r$ is identity-oriented.
Identity and reciprocal orientations of the same direction yield two crossEq facts relating orbitDirection r to $\chi$ of that direction and to the reciprocal of that direction. Symmetry of crossEq plus crossEq_trans glue them into crossEq (orbitDirection r) (recip (orbitDirection r)).
That contradicts orbitDirection_nonunit_not_crossEq_recip, which states a nonunit direction is never cross-equivalent to its own reciprocal. Hence no such reciprocal witness can exist.
why it matters
Native-cost uniqueness for PRC characters needs a clean separation of identity and reciprocal branches once any nonunit identity witness appears. This lemma converts the stronger globalizes hypothesis into the one-sided exclusion form used downstream.
It is consumed by PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget_of_identity_witness_globalizes, which packages prime-calibration forcing into a local exclusion target once identity-witness globalization is assumed. That sits inside the PRC native-cost uniqueness module, where doubled-trace d'Alembert structure and character-to-cost matching pin the cost functional.
In the broader Recognition forcing chain this supports uniqueness of the J-cost (T5 landmark: $J(x)=(x+x^{-1})/2-1$), by ensuring branch mixing cannot survive once an identity witness globalizes. It does not itself force globalization; it only transports that hypothesis into exclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.