PRCCharacterTwoPrimeBranchControlsPrimes_of_local_prime_identity_iff_two
plain-language theorem explainer
Local orientation on every prime axis plus the identity-iff-two normal form force the orbit-2 branch to dictate the branch on all native primes. Anyone proving coherent prime orientation or the native-cost uniqueness blocker cites this. The proof is a two-conjunct case split: the identity arm is the iff, the reciprocal arm rules out mixed identity by a crossEq contradiction on the 2-axis.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose every native prime axis is sent by $\chi$ either to itself or to its reciprocal, and that identity orientation on any native prime axis is equivalent to identity orientation on the distinguished orbit-$2$ prime axis. Then the branch at orbit $2$ controls all primes: identity (resp. reciprocal) at $2$ implies identity (resp. reciprocal) on every native prime axis.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed $\delta$-orbits (numerator) over nonzero distinction-nat denominators. Equivalence of two ratio orbits is crossEq: cross-multiplication balance of scaled signed orbits, the internal PRC stand-in for rational equality. Reciprocals of ratio orbits are total (zero maps to zero).
A ratio character $\chi$ acts on these orbits. Local prime orientation says that on each prime direction $p$, $\chi$ lands either on that direction or on its reciprocal; that is the algebraic content of equal $J$-cost on a single prime axis. The identity-iff-two normal form ties identity on any native prime axis to identity on the distinguished two-prime direction (the orbit of $2$).
Distinguished-prime branch control is the one-axis form of coherent prime orientation: once the branch at orbit $2$ is known, the same branch holds on every native prime. The present theorem packages local orientation plus the iff into that global control statement.
proof idea
Construct the two conjuncts of branch control.
Identity arm: assume $\chi$ is identity at the two-prime direction. For any prime $p$, the reverse direction of the identity-iff-two hypothesis immediately yields identity at $p$.
Reciprocal arm: assume $\chi$ is reciprocal at the two-prime direction. Local orientation gives, for each prime $p$, either identity or reciprocal at $p$. The identity case, fed through the forward direction of the iff, forces identity at $2$. Transitivity of crossEq on the symmetric of that identity with the assumed reciprocal at $2$ produces crossEq of the two-prime direction with its own reciprocal, contradicting that a prime direction is never cross-equivalent to its reciprocal (primeDirection_not_crossEq_recip on twoOrbit). Hence only the reciprocal case survives.
why it matters
Branch control is the one-axis version of coherent prime orientation, which is required to pin native cost characters to a single global orientation rather than independent prime-axis inversions. Downstream, PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_prime_identity_iff_two lifts this lemma to the calibration-target level, and PRCCharacterPrimeOrientationCoherent_of_admissible uses the same local-plus-iff package on the way to full prime-orientation coherence for admissible characters.
That coherence feeds the native-cost uniqueness blocker certificate (prc_native_cost_uniqueness_blocker_certificate), which is the formal gate on uniqueness of the PRC native cost. In the broader Recognition chain this sits under J-uniqueness (T5) and the Recognition Composition Law: characters that preserve the cost structure cannot flip prime axes independently, so the cost is forced rather than chosen per prime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.