PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_refuted
plain-language theorem explainer
Under prime calibration, the joint claim that every nonunit orbit has a local orientation branch and that nonunit identity transport obeys finite δ-trace comparability is false. Native-cost uniqueness and universal-foundation certificates cite this as one rung in the refutation ladder. The proof is a one-step reduction through an equivalence to the already-refuted identity-comparable-trace target.
Claim. It is not the case that prime calibration forces both (i) a local orientation branch on every nonunit orbit and (ii) the finite $\delta$-trace comparability law that stands in for nonunit identity transport. Equivalently, the conjunction of the local nonunit-orbit orientation target with the nonunit identity-comparable-trace target fails.
background
In the Primitive Recognition Calculus, native cost uniqueness is organized as a ladder of candidate "targets": propositional packages that would force global nonunit coherence from prime calibration. The orbit-orientation-plus-comparable-trace target is the trace-layer packaging of the active local identity-transport target. Its second conjunct replaces identity transport by an equivalent finite $\delta$-trace comparability law on nonunit ratios.
An in-module equivalence already shows that this conjunction is logically interchangeable with the bare identity-comparable-trace target alone: the local-orientation half is absorbed once the trace law is assumed. Upstream, that bare identity-comparable-trace target has itself been refuted by reduction to a prime-floor successor-transport target that fails.
The local setting is therefore a pure elimination step inside PRCNativeCostUniqueness: close the trace-layer packaging by transporting the known refutation across the equivalence.
proof idea
Assume the conjunction target. Apply the forward direction of the in-module equivalence ..._iff_identity_comparable_trace to drop the local-orientation conjunct and obtain the bare nonunit identity-comparable-trace target. Discharge the goal by the upstream theorem that already refutes that bare target (itself a one-line reduction to the refuted prime-floor successor-transport package). No new analytic content is introduced.
why it matters
This declaration seals the trace-layer packaging of local identity transport under prime calibration. Downstream, the identity-transport form of the same target is refuted by the same pattern: reduce via its own equivalence to this comparable-trace form, then apply the present theorem. That next refutation, and this one, feed the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic passes.
In the broader Recognition forcing chain the point is negative but structural: candidate formulations that would smuggle nonunit coherence past the native J-cost and doubled-trace D'Alembert constraints are eliminated rung by rung. Closing these targets keeps the uniqueness path aligned with T5 J-uniqueness and the Recognition Composition Law rather than with ad hoc transport axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.