PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_local_branch_agreement
plain-language theorem explainer
Prime calibration forcing global nonunit-orbit orientation coherence is equivalent to forcing local orientation plus two-branch agreement. Anyone assembling the native-cost uniqueness or universal-foundation certificates cites this bridge. The proof is a two-constructor term packaging the already-proved directions of the biconditional.
Claim. The following are equivalent: (i) every ratio character that is prime-direction calibrated has a single coherent orientation on all nonunit orbits; (ii) every such character has local nonunit orientation and the two nonunit branches agree. In other words, global nonunit orientation coherence under prime calibration is equivalent to the positive normal form "local orientation plus branch agreement."
background
In the Primitive Recognition Calculus, ratio characters assign to each ratio orbit another orbit and are constrained by multiplicative structure. Prime-direction calibration means the character respects the preferred orientation on prime generators. Nonunit orbits are those not the unit class; each carries an orientation (identity versus reciprocal).
The coherent target asserts that prime calibration forces one global orientation across every nonunit orbit direction. Once that holds, mixed product factors are ruled out by nonunit non-self-reciprocity. The local-branch-agreement target is the positive normal form of the same blocker: local orientation on each nonunit direction together with agreement of the two branches (identity and reciprocal transport).
Both targets live in the native-cost uniqueness module, which isolates the hypotheses needed to force the native cost from character data and d'Alembert-type identities on doubled traces.
proof idea
Term-mode biconditional. The forward arrow is the existing lemma that coherent target implies local-branch-agreement target (extract local orientation from coherence, then branch agreement). The reverse arrow is the existing lemma that local-branch-agreement target implies coherent target (rebuild global coherence from local orientation plus branch agreement). No new algebra is done here; the proof is the pair of those two maps.
why it matters
This equivalence lets downstream certificates choose whichever normal form is convenient. The universal-foundation conditional certificate consumes the coherent packaging of orientation control as part of the PRC foundation stack (kernel, real complete ordered field, trace logic). In the Recognition forcing chain, orientation coherence on nonunit orbits is the step that blocks mixed product factors and thereby pins the native cost character toward the unique J-cost of T5. Closing the iff means the "global coherence" and "local plus branch agreement" formulations may be swapped without changing the certificate obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.