PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_iff_two_prime_branch_controls
plain-language theorem explainer
Equates two formulations of the prime-orientation blocker for native cost uniqueness: coherent orientation on every native prime axis versus control of all prime branches by the distinguished orbit-2 branch. Anyone transferring a refutation or certificate between those blocker shapes cites this. The proof is the term pairing of the two already-proved one-way implications.
Claim. The assertion that every prime-direction-calibrated ratio character is forced to a single coherent orientation on all native prime axes is equivalent to the assertion that every such character is forced so that the branch chosen at the distinguished orbit $2$ controls every native prime branch.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode admissible cost orientations. Prime-direction calibration means the character has been fixed along each native prime axis up to a binary branch choice (identity versus inversion). Coherent prime orientation then demands that those branch choices agree globally: mixed independent inversions on different primes are forbidden.
The sibling target restates the same demand in distinguished-prime normal form. Orbit $2$ is singled out; the claim is that the branch chosen there propagates to every other native prime branch. Both targets sit inside the native-cost uniqueness module, whose job is to isolate which calibration hypotheses would force the cost functional to the unique $J$-shape.
Upstream, each direction is already a proved implication: coherent orientation yields two-prime branch control, and two-prime branch control (via a local-control lemma) yields coherent orientation.
proof idea
Pure term-mode Iff introduction. The forward arrow is the existing theorem that coherent prime orientation implies two-prime branch control of all primes; the reverse arrow is the existing theorem that two-prime branch control implies coherent orientation (by reducing through the proved local prime-orientation target and the local-to-global coherence lemma). No new algebra is done here.
why it matters
This bridge lets the module refute one blocker shape by refuting the other. Downstream, the coherent-orientation target is refuted by transporting the two-prime-branch-control refutation across the mp direction of this equivalence. The same linkage feeds the native-cost uniqueness blocker certificate and, farther up, the conditional universal-foundation certificate.
In the Recognition forcing chain the native cost is the unique $J$ of T5, $J(x)=(x+x^{-1})/2-1$. Orientation coherence is exactly the place where independent prime inversions would otherwise produce non-$J$ characters. Closing or refuting these blockers therefore decides whether prime calibration alone already forces the RCL cost, or whether further hypotheses remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.