PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_local_product_no_mixed
plain-language theorem explainer
If prime calibration already forces local nonunit orbit orientation and product no-mixing, then it forces a single coherent orientation on every nonunit orbit direction. Cited by the native-cost uniqueness blocker path and by the refutation of the local/product sharpening. Short term proof: unpack the conjunction and apply the local-plus-no-mixed coherence lemma.
Claim. Assume prime calibration forces both (i) local nonunit orbit orientation and (ii) product no-mixing of orientations. Then, for every ratio character $\chi$ that is prime-direction calibrated, $\chi$ has a single coherent orientation across all nonunit orbit directions.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit either the identity or the reciprocal branch. Nonunit orbits are those away from the unit class. Local nonunit orientation means each such orbit is oriented consistently with itself; product no-mixing forbids pairing an identity-oriented nonunit factor with a reciprocal-oriented one in a product; global coherence is the stronger demand that one orientation covers every nonunit direction at once.
The coherent target asserts that prime-direction calibration alone already yields that global coherence. The local/product target is a product-layer sharpening: it packages local orientation with the product no-mixing law, so the remaining branch-coupling work sits on the product side. Upstream, local orientation plus no-mixed nonunit orientation already imply coherence, and product no-mixing specializes to the no-mixed nonunit predicate.
proof idea
Term-mode reduction. Introduce a ratio character $\chi$ with the prime-calibration hypotheses. From the conjunction hypothesis, the first conjunct supplies local nonunit orientation at $\chi$; the second supplies product no-mixing, which the conversion lemma turns into no-mixed nonunit orientation. Feed both into the upstream lemma that local orientation plus no-mixed nonunit orientation yield global nonunit coherence. That is the coherent target at $\chi$.
why it matters
Closes the implication from the product-layer sharpening to the coherent orientation target inside PRC native-cost uniqueness. Downstream, the local/product target is refuted by composing this implication with the already-refuted coherent target, so the sharpening cannot hold. That refutation feeds the native-cost uniqueness blocker certificate, which records which factorization and orientation obligations remain open or closed. In the broader RS forcing picture this sits under uniqueness of the native cost (the J-cost side of T5), not under the geometric T6–T8 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.