PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_of_nonunit_coherent
plain-language theorem explainer
If prime calibration forces a single coherent orientation on all nonunit orbit directions, then it forces local orientation of every nonunit direction (not only prime axes). Workers on the prime-floor successor blocker and native-cost uniqueness cite this reduction. The proof is a one-line pointwise application of the coherence-implies-local lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has a single coherent orientation across all nonunit orbit directions. Then every such $\chi$ orients every nonunit orbit direction locally (identity or reciprocal on each nonunit class).
background
In the Primitive Recognition Calculus, a ratio character $\chi$ maps ratio orbits to ratio orbits and encodes how multiplicative structure is read by a candidate cost. Prime-direction calibration means $\chi$ is already oriented correctly on prime axes. Nonunit orbits are the directions away from the unit class; each may be oriented as identity or as reciprocal.
Local orientation asks only that every nonunit direction receive some orientation. Coherent orientation is stronger: all nonunit directions share one global choice (all identity, or all reciprocal). The coherent target is the documented stronger replacement for product no-mixing: once coherence holds, mixed product factors are ruled out by nonunit non-self-reciprocity.
Upstream, the pointwise lemma states that any single character with coherent nonunit orientation already has local nonunit orientation (by case-splitting the global all-identity versus all-reciprocal alternative). The two targets here are the quantified, prime-calibrated packages of those properties.
proof idea
One-line wrapper. Introduce a ratio character $\chi$ together with the character and prime-calibration hypotheses. Apply the coherent-target hypothesis at $\chi$ to obtain coherent nonunit orientation for that character. Feed the result into the upstream lemma that coherence implies local orientation, and conclude the local-orientation target.
why it matters
This is the first component of the prime-floor successor blocker: local orientation of every nonunit direction, not only prime axes. Downstream it is packed into the sharpened coherent target (local orientation plus prime-floor successor transport), into the local-adjacent transport target, and into the identity-witness local-exclusion target once identity witnesses globalize. Those pieces feed the native-cost uniqueness blocker certificate, which certifies the factorization and signed-admissible refutation legs of uniqueness for the native PRC cost. In the broader Recognition chain this supports uniqueness of the J-cost (T5) once characters are forced into the calibrated, non-mixing regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.