PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget
plain-language theorem explainer
Packages global nonunit orbit orientation coherence as the conjunction of two sharper obligations: every nonunit orbit direction is locally oriented under prime calibration, and identity-oriented nonunit directions never mix with reciprocal-oriented ones. Downstream uniqueness and blocker certificates cite this split. The body is a pure Prop conjunction of the two named targets.
Claim. The sharpened prime-calibration target is the conjunction of: (i) every ratio character that is prime-direction calibrated has a local orientation on every nonunit orbit direction; and (ii) no such character admits mixed identity and reciprocal orientations across distinct nonunit orbits.
background
In the Primitive Recognition Calculus, ratio characters assign to each ratio orbit a directed image orbit. Prime-direction calibration fixes orientation on prime axes; the open question is whether that forces orientation on all nonunit orbits and forbids mixed identity/reciprocal choices across them.
The first conjunct is the local-orientation target: under prime calibration, every nonunit orbit direction already carries a local branch. The second is the branch-coupling (no-mixed) target: no identity-oriented nonunit direction may coexist with a reciprocal-oriented nonunit direction. Upstream docs state that together these two are exactly global nonunit orientation coherence.
This module sits in the native-cost uniqueness development, where doubled-trace and d'Alembert structure constrain admissible cost characters. The present definition is the product-layer packaging of that coherence obligation.
proof idea
Definitional packaging only: the Prop is the literal conjunction of the local nonunit-orbit orientation target and the no-mixed nonunit-orbit orientation target. No tactics or lemmas are applied; downstream theorems project the two components or reassemble them into the coherent target.
why it matters
This is the preferred intermediate form of global nonunit coherence in the native-cost uniqueness chain. Downstream, it is proved equivalent to the coherent target via a two-way iff, and the coherent target is recovered by applying the local-and-no-mixed reconstruction lemma to the two conjuncts. A product-layer strengthening (local product no-mixed) implies this target by projecting the first factor and transporting the second through the product-to-no-mixed map.
It appears in the Pass-25 blocker certificate structure that records exactly which uniqueness obligations remain open, and in the universal-foundation open-targets list. A later theorem in the same module refutes the target (via the coherent-target refutation and the iff), so the split is now a closed negative: prime calibration alone does not force this sharpened coherence. That negative is part of narrowing the remaining path to native J-cost uniqueness (T5 landmark: J-uniqueness from the Recognition Composition Law).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.