PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget
plain-language theorem explainer
Packages local nonunit-orbit orientation with identity-branch transport as the minimal positive normal form of the prime-calibration blocker. Reciprocal transport is claimed to follow from these two facts alone. Native-cost uniqueness proofs cite the package when reducing branch agreement or δ-trace comparability. The body is the pure conjunction of the two component targets.
Claim. The proposition asserting both (i) every prime-calibrated ratio character orients every nonunit orbit direction (not only prime axes), and (ii) if such a character leaves one nonunit direction identity-oriented, that identity branch transports to every nonunit direction.
background
In the primitive recognition calculus, ratio characters $\chi$ act on ratio orbits. Prime-direction calibration constrains $\chi$ on prime axes; the open question is what that forces on the rest of the nonunit orbit lattice. The identity event sits at the $J$-cost minimum $x=1$ (ObserverForcing), so an "identity-oriented" branch is one that still maps to that minimum.
The first conjunct says prime calibration should force local orientation of every nonunit orbit, not only primes. The second is the positive transport form of the branch-coupling blocker: once one nonunit direction remains identity-oriented, that identity branch must transport across all nonunit directions. The module packages these as the sharp local normal form before passing to branch agreement or finite $\delta$-trace comparability.
proof idea
Definitional abbreviation: the target is the conjunction of the local-orientation target and the identity-branch-transport target. No proof obligations; both conjuncts are themselves Prop-valued defs quantifying over ratio characters with the prime-calibration hypothesis.
why it matters
This is the preferred positive normal form in the prime-floor successor chain inside PRC native-cost uniqueness. Downstream, branch-agreement and local-comparable-trace targets are shown equivalent to it (iff theorems), and one-direction implications derive branch agreement and comparable-trace packages from it. A dedicated ..._refuted edge also sits on this name, so the package is the hinge between the orientation/transport formulation and the trace-layer reformulation. It sits upstream of the uniqueness argument that pins the native cost to the $J$-cost shape forced at T5, without yet invoking the full Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.