PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationSharpenedTarget_refuted
plain-language theorem explainer
The Pass-45 sharpened product-local orientation target is false: prime calibration does not force nonunit-orbit product-local orientation coherence. Native-cost uniqueness and floor-successor transport arguments cite this blocker. Proof is a one-line wrapper: the sharpened target is definitionally the already-refuted orientation-coherence target.
Claim. The Pass-45 sharpened claim that prime calibration forces nonunit-orbit product-local orientation coherence is false. Equivalently, $\neg$ (nonunit-orbit orientation coherence under prime calibration), since the sharpened product-local target is definitionally that coherence proposition.
background
In the Primitive Recognition Calculus native-cost uniqueness module, several calibration targets encode what prime calibration would have to force if a unique native cost character existed. Product-local orientation is one such commitment: same-orientation products should be algebraic, product-display compatibility should hold via canonical normalization, and the residual obligation is nonunit orientation coherence (which would imply product no-mixing).
Pass-45 sharpens the product-local orientation package by discharging the algebraic and display-compatibility pieces, leaving only nonunit orientation coherence. That residual is packaged as a proposition definitionally identical to the nonunit-orbit orientation-coherence target.
Upstream, that coherence target is already refuted: assuming it reduces to a globalized nonunit-identity witness target that fails. The present declaration simply records the same negative result at the sharpened product-local name.
proof idea
One-line wrapper. The sharpened product-local orientation target is definitionally equal to the nonunit-orbit orientation-coherence target, so the existing refutation of the latter applies verbatim. No new case split or algebraic work occurs here.
why it matters
This closes the Pass-45 sharpened product-local orientation branch as a dead end under prime calibration. Downstream, the floor-successor transport sharpened target is refuted by projecting to this first conjunct, so successor-transport sharpenings that still carry the product-local orientation obligation inherit the blocker.
It also feeds the native-cost uniqueness blocker certificate and, indirectly, the conditional universal-foundation certificate stack. In the Recognition forcing picture this is bookkeeping on the cost-uniqueness side of the foundation (J-cost uniqueness and native character constraints), not a new forcing step T5–T8; it records that one natural product-orientation route to uniqueness does not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.