PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget_of_local_product_no_mixed
plain-language theorem explainer
If prime calibration already yields local nonunit orbit orientation plus the product-layer no-mixing law, then it yields local nonunit orientation plus the cross-nonunit no-mixing law. Anyone assembling the sharpened global nonunit-coherence source for native-cost uniqueness cites this reduction. The proof is a two-field pair: keep the local conjunct and convert the product conjunct by the product-to-no-mixed lemma.
Claim. Assume prime calibration forces every nonunit orbit direction to admit a local orientation branch and also forces the orbit-product no-mixing orientation law. Then prime calibration forces every nonunit orbit direction to admit a local orientation branch together with the cross-nonunit no-mixing orientation law.
background
In the primitive recognition calculus, native cost uniqueness is organized around calibration hypotheses on ratio characters and their doubled-trace D'Alembert structure. Global nonunit coherence is not taken as a single blob: it is sharpened into a local orientation obligation (every nonunit orbit direction has a local branch) plus a branch-coupling obligation that forbids mixed orientations across distinct nonunit orbits.
Two Prop packages package that sharpening. The local-no-mixed target is the conjunction of local nonunit orientation with the cross-nonunit no-mixing law. The local-product-no-mixed target keeps the same local orientation conjunct but carries the coupling obligation by the product no-mixing law instead. The product form is the easier intermediate once local orientation is already in hand.
Upstream, the product no-mixing package is known to imply the cross-nonunit no-mixing package: for each admissible character, the product-layer law specializes to the character-level no-mixed nonunit orbit orientation statement.
proof idea
Term-mode pair constructor on the two conjuncts of the conclusion. The first field is the local nonunit orientation conjunct of the hypothesis, copied unchanged. The second field applies the upstream reduction that turns any proof of the orbit-product no-mixing orientation target into a proof of the cross-nonunit no-mixing orientation target, feeding the hypothesis's second conjunct. No new analytic work occurs here; it is pure Prop packaging.
why it matters
This sits in the native-cost uniqueness spine of Primitive Recognition Calculus: it lets the development discharge the sharpened local-no-mixed coherence source from the product-layer intermediate rather than proving cross-nonunit no-mixing from scratch. Downstream it is consumed by the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization targets and signed-admissible refutations into a single certificate object. In the broader Recognition forcing picture, native cost uniqueness is the analytic gate that pins the J-cost (T5) as the unique calibrated cost before phi, the eight-tick octave, and D = 3 are forced further down the chain. The declaration closes a packaging gap between product-layer and cross-nonunit formulations of nonunit orbit coherence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.