PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentSharpenedTarget_refuted
plain-language theorem explainer
Refutes the sharpened claim that prime calibration, via local nonunit orientation plus prime-floor successor transport, forces every nonunit orbit direction onto one coherent identity/reciprocal branch. Native-cost uniqueness blockers and the universal-foundation conditional certificate cite this negative result. The proof is a one-line transfer: the unsharpened coherence target is already refuted, and an iff equates the two formulations.
Claim. The conjunction of local nonunit-orbit orientation under prime calibration with prime-floor successor transport does not hold: it is false that these two conditions force every nonunit orbit direction onto a single coherent identity/reciprocal branch.
background
In the Primitive Recognition Calculus (PRC), native cost uniqueness is organized around calibration targets that would pin the cost character on ratio orbits. One family of targets concerns orientation coherence on nonunit orbits: the claim that prime calibration forces every nonunit orbit direction onto a single identity-versus-reciprocal branch.
The sharpened target packages that claim as a conjunction of two more local sources: a local nonunit orientation target, and a prime-floor successor-transport target. The module records an equivalence between this sharpened conjunction and the unsharpened nonunit-orbit orientation-coherence target.
Upstream, the unsharpened coherence target is already refuted by reduction to a still weaker identity-witness globalization target that fails. The present declaration simply closes the sharpened packaging under that same negative result.
proof idea
Term-mode one-liner after intro. Assume the sharpened conjunction. Apply the reverse direction of the iff equating the unsharpened orientation-coherence target with the sharpened conjunction, obtaining the unsharpened target. Discharge by the already-proved refutation of that unsharpened target (itself a reduction to the refuted identity-witness globalization target). No new arithmetic or orbit analysis is performed here.
why it matters
This seals the sharpened packaging of nonunit orientation coherence as false, matching the unsharpened refutation. Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which assembles proved and refuted factorization targets into the native-cost uniqueness blocker record, and prc_universal_foundation_conditional_certificate in UniversalFoundation, which bundles kernel, real-complete ordered field, and trace-logic certificates.
In the Recognition forcing picture, native cost is meant to be the unique J-cost (T5: $J(x)=(x+x^{-1})/2-1$) once calibration and orbit structure are fixed. Refuting over-strong orientation-coherence targets prevents a false uniqueness route that would force every nonunit orbit onto one reciprocal branch by prime-floor transport alone. The blocker certificate records what remains open versus what is ruled out on the path to PRC native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.