PRCCharacterTwoPrimeBranchControlsPrimes_of_coherent
plain-language theorem explainer
Coherent prime-axis orientation of a ratio-orbit character forces the two-prime branch-control property: the identity or reciprocal choice at the orbit of 2 propagates to every native prime direction. Anyone calibrating native cost characters or discharging prime-orientation targets cites this. The proof is a short case split on the coherent disjunction, with the mixed cases ruled out by non-self-reciprocity of prime directions under cross-equivalence.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose prime-axis orientation is coherent: either $\chi$ fixes every native prime direction up to cross-equivalence, or $\chi$ sends every native prime direction to its reciprocal up to cross-equivalence. Then the branch at the two-prime direction controls all primes: if $\chi$ fixes the two-prime direction, it fixes every prime direction; if $\chi$ sends the two-prime direction to its reciprocal, it does so for every prime direction.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed numerator orbits over nonzero distinction-nat denominators. Cross-equivalence crossEq is the internal PRC rational relation: two orbits match when scaled numerators balance under cross-multiplication of denominators (K4.10). Reciprocal swaps numerator and denominator (sending zero to zero).
A character $\chi$ acts on ratio orbits. Prime directions are the ratio-orbit axes associated to native prime distinction-nats; twoOrbit is the two-step orbit, and twoPrimeDirection is its prime axis. Coherent prime orientation means $\chi$ chooses one global orientation on every such axis: all identity, or all reciprocal, each up to cross-equivalence.
Two-prime branch control is the one-axis form of that coherence: knowing whether $\chi$ fixes or reciprocates the two-prime direction already determines the same choice on every native prime axis. The present theorem says full coherence implies that weaker control property.
proof idea
Term-mode proof by constructor on the two implications in branch control.
First implication: assume $\chi$ fixes the two-prime direction. Case on coherent orientation. If all primes are identity, done. If all primes are reciprocal, specialize to twoOrbit to get that $\chi$ also reciprocates the two-prime direction; transitively (via crossEq_symm and crossEq_trans) the two-prime direction is cross-equivalent to its own reciprocal, contradicting primeDirection_not_crossEq_recip.
Second implication is symmetric: assume $\chi$ reciprocates the two-prime direction; the all-identity coherent case yields the same self-reciprocal contradiction at two, while the all-reciprocal case is immediate.
why it matters
Native cost uniqueness needs a clean reduction from global prime-orientation coherence to a single calibration axis at 2. This lemma is that reduction: it turns the coherent disjunction into the two-prime branch-control interface used by calibration targets.
Downstream, PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_coherent_prime_orientation is a one-line application of this theorem under the prime-calibration coherence target. The result also feeds prc_native_cost_uniqueness_blocker_certificate and, further out, the conditional universal-foundation certificate in UniversalFoundation.
In the Recognition forcing picture this sits under native J-cost uniqueness (T5-adjacent): characters on ratio orbits must lock orientation consistently before the cost functional can be forced. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.