PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_branch_uniform
plain-language theorem explainer
Branch uniformity of prime-axis identity orientation for a ratio-orbit character implies the identity-iff-two normal form: any native prime axis is identity-oriented exactly when the distinguished orbit-2 prime axis is. Cited by native-cost uniqueness and prime-calibration arguments that reduce identity transport to a single reference prime. The proof is a two-direction specialization of the uniformity hypothesis at the prime orbit of 2.
Claim. Let $\chi$ act on rational orbits. Suppose that whenever $\chi$ is identity-oriented on one native prime axis, it is identity-oriented on every native prime axis. Then for every native prime $p$, $\chi$ is identity-oriented on the $p$-axis if and only if it is identity-oriented on the distinguished orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Native prime axes are the prime directions of distinction-nats that satisfy the prime-orbit predicate; the distinguished reference is the two-step orbit (successor of one), which is itself prime.
A character $\chi$ is identity-oriented on an axis when its image of that prime direction is cross-equal to the direction itself. Branch uniformity says identity orientation on any one native prime axis forces identity orientation on all of them: the remaining obstruction is branch uniformity, not trace construction.
The identity-iff-two normal form strengthens that picture to a biconditional against the fixed orbit-2 prime axis alone. This module develops native cost uniqueness for characters built from the J-cost side of the recognition calculus.
proof idea
Term-mode proof by introducing an arbitrary native prime $p$ and splitting the desired biconditional.
Forward: assume identity on the $p$-axis; apply branch uniformity with source $(p,hp)$ and target the two-orbit (using that two is prime) to obtain identity on the orbit-2 axis.
Reverse: assume identity on the orbit-2 axis; apply the same uniformity hypothesis with source the two-orbit and target $(p,hp)$.
No extra lemmas beyond the two-orbit primality fact and the two predicate definitions.
why it matters
Closes one direction of the equivalence between branch uniformity and the identity-iff-two normal form, so the two blockers can be swapped freely in uniqueness arguments. Downstream, prime-calibration targets that already force branch uniformity immediately obtain the identity-iff-two target by applying this theorem.
It also appears in the conditional universal-foundation certificate path, tying native character orientation into the broader PRC foundation stack. In framework terms this is bookkeeping on the way to J-uniqueness (T5) and native cost uniqueness: once identity orientation is pinned to a single reference prime, calibration and trace-matching can finish the cost identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.