PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_local_no_mixed
plain-language theorem explainer
Prime calibration forcing a single coherent orientation on all nonunit ratio-orbit directions is equivalent to local branch existence on every nonunit direction plus a cross-nonunit no-mixing law. Native-cost uniqueness and foundation-certificate authors cite this to swap the coherent formulation for the local-plus-no-mixed split (or conversely). The proof is a pure bidirectional Iff constructor from the two already-proved one-way implications.
Claim. The claim that every prime-direction-calibrated ratio character has one coherent nonunit-orbit orientation is equivalent to the conjunction of (i) every nonunit orbit direction admitting a local identity/reciprocal branch and (ii) no mixed identity-versus-reciprocal orientations across distinct nonunit directions, all under prime calibration.
background
In the Primitive Recognition Calculus, ratio characters assign orbit data along ratio orbits. Prime-direction calibration constrains character behaviour on prime generators. Nonunit orbits sit away from the identity ratio (the J-cost minimum at $x=1$) and admit two reciprocal branches: the identity orientation and the reciprocal-automorphism orientation.
Global nonunit orientation coherence demands that every nonunit direction share one common branch. The coherent target packages that demand as a single universal quantification over characters. The local-no-mixed target splits the same demand into local branch existence plus a product-layer no-mixing law forbidding identity-oriented and reciprocal-oriented nonunit directions from coexisting. As the coherent-target doc states, once coherence is available "mixed product factors are impossible by nonunit non-self-reciprocity."
The module develops native cost uniqueness through these orientation constraints; the two targets are alternative phrasings of the same intermediate obligation on the path to locking the native cost.
proof idea
Term-mode Iff introduction with no new arithmetic. The left-to-right direction is the already-proved implication from coherent target to local-no-mixed target. The right-to-left direction is the companion implication: unpack the conjunction (local orientation target and no-mixed target), apply both halves at a fixed prime-calibrated character, and reassemble global coherence via the lemma that local orientation plus no-mixing yields nonunit-orbit orientation coherence.
why it matters
This equivalence is the bridge used when the local-no-mixed target is refuted: the refutation reduces local-no-mixed to the coherent target via the reverse direction of this Iff, then invokes the coherent-target refutation. It also feeds the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate.
Within Recognition Science, orientation coherence is part of locking the native J-cost (forcing-chain T5 J-uniqueness, with $J(x)=(x+x^{-1})/2-1$) against competing character factorizations on the ratio-orbit lattice. The equivalence lets authors work at whichever granularity is convenient without changing the logical strength of the uniqueness obligation, and it is the precise hinge that turns a coherent-side refutation into a local-no-mixed-side refutation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.