PRCCharacterPrimeIdentityBranchUniform_of_identity_iff_two
plain-language theorem explainer
If a ratio-orbit character equates identity orientation on every native prime axis with identity on the distinguished orbit-2 axis, then identity on any one prime axis forces identity on all of them. Native-cost uniqueness and prime-calibration arguments cite this to collapse the branch-uniformity blocker to the two-axis normal form. The proof is a three-line transport through the biconditional at p and at r via the orbit-2 pivot.
Claim. Let $\chi$ be a map on rational orbits. Suppose that for every native prime axis $p$, $\chi$ is identity-oriented at $p$ if and only if it is identity-oriented at the distinguished orbit-$2$ prime axis. Then whenever $\chi$ is identity-oriented at any native prime axis $p$, it is identity-oriented at every native prime axis $r$.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-natural denominator). Native prime axes are the prime directions in that orbit language; orientation is recorded by RatioOrbit.crossEq of $\chi$ against the axis itself.
Two normal forms package the remaining prime-identity obstruction. Identity-iff-two says identity at any calibrated prime axis is equivalent to identity at the distinguished orbit-2 axis. Branch uniformity says identity at any one native prime axis forces identity at every other: the trace-free content of the prime identity transport blocker, with the name stressing branch uniformity rather than trace construction.
This lemma sits in the native-cost uniqueness module, where characters are constrained so that cost extracted from the character matches the doubled-trace d'Alembert data used downstream in the forcing chain toward J-uniqueness.
proof idea
Pure logical transport through the given biconditional. Fix primes $p$ and $r$ and assume identity orientation at $p$. Apply the forward direction of identity-iff-two at $p$ to obtain identity at the orbit-2 axis; apply the reverse direction at $r$ to push that identity onto $r$. No orbit arithmetic or cost identities are invoked.
why it matters
Closes one half of the equivalence between branch uniformity and the identity-iff-two normal form; the sibling converse and the combined iff theorem sit immediately downstream. That equivalence lets prime-calibration targets that only force identity-iff-two upgrade to full branch-uniformity targets (PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_identity_iff_two). The same fact is wired into the conditional universal-foundation certificate, so the prime-identity transport blocker reduces to a single distinguished axis rather than a family of independent branches. In the broader RS forcing picture this is bookkeeping on the way to unique native cost (and ultimately T5 J-uniqueness), not a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.