PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget_refuted
plain-language theorem explainer
Prime calibration does not force the conjunction of local orientation on every nonunit orbit and a cross-nonunit no-mixing law. Native-cost uniqueness and universal-foundation certificate authors cite this as a closed blocker. The proof is a short transport: the local-no-mixed package is equivalent to global nonunit coherence, which is already refuted.
Claim. It is not the case that prime calibration forces both (i) a local orientation branch on every nonunit orbit direction and (ii) the cross-nonunit no-mixing law for orbit orientations. Equivalently, the sharpened local-plus-no-mix package for global nonunit coherence fails.
background
In the Primitive Recognition Calculus, native cost uniqueness is organized around calibration targets that would force a unique cost character from prime data. One family of targets concerns orientation of nonunit orbits: each nonunit multiplicative orbit should carry a coherent choice of branch, and distinct nonunit orbits should not mix those choices.
The local-no-mixed target packages two obligations: every nonunit orbit direction has a local orientation branch, and a product-layer no-mixing law couples those branches across nonunit orbits. The module doc for that package calls it a "sharpened source of global nonunit coherence": prove local branches first, then the cross-nonunit no-mixing law.
Upstream, that package is proved equivalent to the single coherent nonunit-orbit-orientation target. The coherent target is already refuted by reduction to a still-stronger identity-witness globalization target that fails. The present result simply closes the equivalent local-no-mixed formulation.
proof idea
Assume the local-no-mixed target. Apply the reverse direction of the equivalence between the coherent nonunit-orbit-orientation target and the local-no-mixed package, obtaining the coherent target. Discharge by the already-proved refutation of the coherent target (itself a transport to the identity-witness globalization refutation). The whole argument is a three-line intro-plus-exact chain; no new analytic content.
why it matters
This seals one sharpened formulation of global nonunit coherence under prime calibration. Downstream it feeds the native-cost uniqueness blocker certificate, which records which factorization and orientation routes are proved versus refuted, and the conditional universal-foundation certificate that assembles kernel, ordered-field, and trace-logic passes.
In the Recognition forcing picture, native cost is meant to pin the J-cost shape (T5) before phi and the eight-tick structure appear. Refuting over-strong orientation packages prevents a false uniqueness route: calibration cannot smuggle global nonunit coherence through local branches plus no-mixing alone. The open work remains on the surviving zero-calibrated factorization side of the blocker certificate, not on this orientation package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.