PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_local_two_prime_branch_controls
plain-language theorem explainer
Local prime orientation plus two-prime branch control force the identity-iff-two normal form for a ratio-orbit character: identity on any native prime axis is equivalent to identity on the distinguished orbit-2 axis. Native-cost uniqueness and prime-calibration arguments cite this bridge. The proof is a short case split on the 2-axis branch, using cross-equality symmetry/transitivity and the fact that a prime direction is never cross-equal to its reciprocal.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose each prime axis is sent by $\chi$ either to itself or to its reciprocal (local prime orientation), and that the branch chosen at the distinguished orbit-$2$ prime axis controls the branch on every native prime axis. Then for every native prime $p$, $\chi$ is the identity on the $p$-axis if and only if it is the identity on the orbit-$2$ axis.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed $\delta$-orbits (numerator) over a nonzero distinction-natural denominator. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits; this is the internal PRC stand-in for rational equality. Reciprocal swaps numerator and denominator (sending zero to zero).
A character $\chi$ acts on ratio orbits. Local prime orientation says that on each prime direction, $\chi$ lands either on that direction or on its reciprocal: the algebraic content of equal $J$-costs on a single prime axis. Two-prime branch control strengthens this: once the branch at the distinguished orbit-$2$ prime axis is fixed (identity or reciprocal), the same branch holds on every native prime axis.
The target normal form is identity-iff-two: identity orientation on any native prime axis is equivalent to identity orientation on orbit $2$. That normal form is the bridge from local $J$-cost matching to coherent global prime orientation in the native-cost uniqueness development.
proof idea
Fix a native prime $p$. Prove both directions of the biconditional.
($\Rightarrow$) Assume identity on the $p$-axis. Case-split local orientation at twoOrbit. If the $2$-axis is already identity, done. If instead $\chi$ sends the $2$-axis to its reciprocal, branch control forces the reciprocal branch on $p$ as well. Symmetry and transitivity of cross-equality then yield that the $p$-direction is cross-equal to its own reciprocal, contradicting primeDirection_not_crossEq_recip.
($\Leftarrow$) Assume identity on the $2$-axis. The first conjunct of two-prime branch control immediately gives identity on $p$.
why it matters
This lemma closes the gap between local prime orientation and the identity-iff-two normal form once the distinguished $2$-axis controls all prime branches. Downstream, PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_two_prime_branch_controls applies it under prime-calibration hypotheses to obtain the corresponding target-level statement. That feeds the native-cost uniqueness blocker certificate and, further out, the conditional universal-foundation certificate.
In the Recognition framework this is part of the algebraic spine behind $J$-cost uniqueness (forcing-chain T5): characters that match native cost on primes cannot mix identity and reciprocal orientations across prime axes. Coherent orientation on the $\phi$-ladder primes is a prerequisite for uniqueness of the native cost functional built from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.