PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_refuted
plain-language theorem explainer
Prime calibration cannot force both local orbit orientation and identity-branch transport on nonunit orbits. Anyone tracking the PRC native-cost uniqueness cascade cites this as the identity-transport layer of the refutation tower. The proof is a one-line transfer: the target is equivalent to the already-refuted local comparable-trace target, so the negation carries over by the iff.
Claim. It is false that prime calibration forces the conjunction of local nonunit-orbit orientation and identity-branch transport (the minimal positive normal form from which reciprocal transport would follow).
background
In the Primitive Recognition Calculus (PRC) native-cost uniqueness development, several "calibration targets" encode candidate forcing claims: that prime calibration alone would pin down orientation, transport, or trace-comparability laws on nonunit orbits. The identity-transport target is the conjunction of local orbit orientation with identity-branch transport. Its doc-comment states that this pair is the minimal positive normal form, since reciprocal transport follows from those two facts.
A parallel trace-layer target replaces the identity-transport half by a finite $\delta$-trace comparability law. An in-module equivalence theorem identifies the two targets: local orientation plus identity-branch transport holds if and only if local orientation plus comparable-trace holds. The comparable-trace target has already been refuted upstream by reduction to the pure identity comparable-trace refutation.
proof idea
Term-mode one-step transfer. Assume the identity-transport target $h$. Apply the left-to-right direction of the equivalence
PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_iff_local_comparable_trace
to obtain the local comparable-trace target. Feed that into the already-proved refutation
PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_refuted.
No new analytic work occurs here; the lemma only moves the negation across the iff.
why it matters
This sits in the middle of the PRC calibration-refutation tower. Immediately downstream, the branch-agreement target is refuted by the same pattern: branch agreement implies identity transport, which is now known false. The result is also consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which packages kernel, real-complete-ordered-field, and trace-logic certificates into the conditional universal-foundation bundle.
In the broader Recognition Science forcing chain, native-cost uniqueness underwrites the J-cost uniqueness step (T5) and the Recognition Composition Law. Closing off over-strong prime-calibration claims keeps the uniqueness route honest: cost structure is forced by the composition law and self-similarity, not by an illicit local transport axiom on nonunit orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.