PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_local_branch_agreement
plain-language theorem explainer
If prime calibration forces local nonunit orientation and two-branch agreement on every ratio character, then it forces global nonunit orbit orientation coherence. Cost-uniqueness and foundation auditors cite this to collapse the branch-coupling blocker to its positive normal form. The proof unpacks the conjunction and applies the character-level coherence lemma.
Claim. Assume that every prime-direction-calibrated ratio character $\chi$ has local nonunit orbit orientation and nonunit two-branch agreement. Then every such $\chi$ has global nonunit orbit orientation coherence (a single coherent orientation across all nonunit orbit directions).
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode multiplicative recognition data. Prime-direction calibration restricts how $\chi$ acts along prime generators. Nonunit orbit directions may be identity-oriented or reciprocal-oriented; local orientation asserts each nonunit direction is consistently one or the other, while branch agreement asserts the two branches transport coherently (identity-branch transport is the minimal positive form; reciprocal transport follows).
Global nonunit orbit orientation coherence is the stronger statement that a single orientation class holds across all nonunit directions. Mixed product factors are then impossible by nonunit non-self-reciprocity. The local-plus-agreement package is the documented positive normal form of the global branch-coupling blocker.
Upstream, the character-level lemma already shows that local orientation plus branch agreement imply coherence for a fixed $\chi$. The two target propositions lift that implication to the universal quantification over prime-calibrated characters.
proof idea
One-line unpack-and-apply. Introduce a ratio character $\chi$ with the ratio-character and prime-calibration hypotheses. Project the assumed target conjunction to obtain local orientation and branch agreement for that $\chi$. Feed both into the character-level lemma PRCCharacterNonunitOrbitOrientationCoherent_of_local_branch_agreement, which returns global nonunit orbit orientation coherence.
why it matters
This is one direction of the equivalence between the coherent-orientation target and its local-branch-agreement normal form. That equivalence lets the uniqueness stack discharge the stronger global blocker by proving only the positive local package. Downstream it is assembled into the iff theorem and consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates for the PRC foundation layer.
In the Recognition forcing chain this sits inside native cost uniqueness: coherent nonunit orientation rules out mixed product factors, clearing the path toward the unique J-cost (T5: $J(x)=(x+x^{-1})/2-1$) forced by the Recognition Composition Law. Without this reduction, the branch-coupling blocker would remain a separate global obligation rather than a consequence of local orientation plus agreement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.