PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalProductNoMixedTarget_refuted
plain-language theorem explainer
The product-layer sharpening of nonunit orbit orientation under prime calibration is false: one cannot obtain global nonunit coherence by pairing local nonunit orientation with a product no-mixing law. Anyone tracking native-cost uniqueness blockers or the universal foundation certificate will cite this. The proof is a two-step reduction: the sharpened target implies the coherent target, which is already refuted.
Claim. It is not the case that prime calibration forces both (i) local nonunit orbit orientation and (ii) product-level no-mixed orientation on orbits. Equivalently, the conjunction of those two obligations fails as a global target.
background
In the Primitive Recognition Calculus, native cost uniqueness is organized around calibration targets: propositions asserting that prime calibration forces a stated structural property of ratio characters and their orbit orientations. The coherent nonunit-orbit-orientation target asks for a global orientation law on nonunit orbits. A product-layer sharpening splits that demand into local nonunit orientation plus a product no-mixing law that couples branches without mixed orientations.
The module develops these targets as named propositions so that each can be proved or refuted independently, then assembled into blocker certificates. Upstream, the sharpened conjunction is shown to imply the coherent target: if local orientation and product no-mixing both hold under prime calibration, global coherence follows. Separately, the coherent target itself has already been refuted by reduction to a failed identity-witness globalization obligation.
proof idea
Term-mode reductio. Assume the local-product-no-mixed target. Apply the implication theorem that turns that sharpened conjunction into the coherent nonunit-orbit-orientation target. Feed the resulting coherent target into the existing coherent-target refutation, which yields falsehood. No new analytic work: pure target-lattice composition of two prior results.
why it matters
Closes one remaining product-layer escape route in the native-cost uniqueness program: after global coherence fails, one might hope local orientation plus product no-mixing still salvage the story. This theorem kills that hope. It feeds prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted factorization targets into a single blocker record, and appears in the conditional universal-foundation certificate chain. Within Recognition Science, native cost uniqueness sits under the J-cost forcing story (T5 J-uniqueness and the Recognition Composition Law); clearing false sharpenings keeps the uniqueness ledger honest rather than leaving open product-layer loopholes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.