PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_of_two_prime_branch_controls
plain-language theorem explainer
If prime calibration forces the branch chosen at orbit 2 to control every native prime branch, then it forces a single coherent orientation on all native prime axes. Orientation-blocker arguments in native-cost uniqueness cite this reduction. The proof feeds the already-proved local orientation target and the two-prime control hypothesis into the local-plus-control coherence lemma.
Claim. Assume that whenever a ratio-orbit character $\chi$ is prime-direction calibrated, the branch chosen at the distinguished orbit $2$ controls every native prime branch. Then every such calibrated $\chi$ has a single coherent orientation across all native prime axes (no mixed independent prime inversions).
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters $\chi$ assign to each ratio orbit another orbit, subject to character axioms. Prime-direction calibration means $\chi$ respects the preferred direction on each native prime axis. Two orientation blockers sit above this: coherent prime orientation (one global choice of identity vs reciprocal on every prime axis) and its distinguished-prime normal form (the branch at orbit $2$ controls every other native prime branch).
The coherent-orientation target is the sharper blocker A: calibration must rule out mixed independent prime inversions. The two-prime-branch-controls target is the same obstruction rewritten so that control propagates from the orbit-$2$ prime axis. Local orientation (identity or reciprocal on each prime axis separately) is already proved for calibrated characters.
Upstream, PRCCharacterPrimeOrientationCoherent_of_local_two_prime_branch_controls states that local orientation plus two-prime branch control yields global coherence, by case analysis on the orbit-$2$ branch.
proof idea
Short tactic proof. Introduce a calibrated ratio character $\chi$. Apply the already-proved local prime-orientation target to obtain local orientation of $\chi$. Apply the two-prime-branch-controls hypothesis at the same $\chi$ to obtain branch control from orbit $2$. Feed both facts into PRCCharacterPrimeOrientationCoherent_of_local_two_prime_branch_controls, which concludes global prime-orientation coherence.
why it matters
This is one direction of the equivalence between the coherent-orientation blocker and its distinguished-prime normal form, and is the half used by the iff theorem that identifies the two targets. Downstream, prime-pair product cost consistency reduces to coherent orientation by first reaching two-prime branch control and then applying this lemma. The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate sit further up the same stack: closing orientation coherence is part of forcing a unique native cost character before the broader foundation certificate can fire. In framework terms this is foundation work under the PRC cost calculus that feeds J-uniqueness (T5) style uniqueness of the recognition cost, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.