PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_of_local_identity_transport
plain-language theorem explainer
Prime calibration that forces local orientation of every nonunit orbit, together with identity-branch transport, already yields the equivalent finite δ-trace comparability law on those orbits. Anyone assembling the local normal-form package for native cost uniqueness cites this implication. The proof keeps the orientation half and converts the transport half by the branch-to-comparable-trace lemma.
Claim. If prime calibration forces every nonunit orbit to be locally oriented and the identity branch transports across nonunits, then the same calibration forces local orientation together with the finite $\delta$-trace comparability law on nonunit identity data.
background
In the Primitive Recognition Calculus native-cost uniqueness module, prime calibration is asked to pin down how nonunit ratio orbits sit relative to the identity. Two local packages appear. The identity-transport target is local orientation of every nonunit orbit plus identity-branch transport; the doc-comment calls this the minimal positive normal form, from which reciprocal transport follows. The comparable-trace target keeps the same orientation half and replaces the transport half by its finite $\delta$-trace comparability law.
Upstream, branch transport already implies the character respects comparable trace: given a character $\chi$ with nonunit identity-branch transport, the corresponding respect-comparable-trace predicate holds by specializing the transport hypothesis. That one-step conversion is the only bridge needed between the two packages.
proof idea
Term proof that builds the conjunction directly. The orientation conjunct is copied from the hypothesis. For the comparable-trace conjunct, introduce a character $\chi$ satisfying the prime-calibration hypotheses and apply PRCCharacterNonunitIdentityRespectsComparableTrace_of_branch_transport to the identity-branch-transport half supplied by the hypothesis. No further algebraic work.
why it matters
Closes one direction of the local equivalence between the identity-transport normal form and its trace-layer restatement. The sibling iff theorem packages both directions, so either formulation may be used when discharging the active local target. Downstream, the Universal Foundation conditional certificate consumes this layer as part of the PRC foundation stack (kernel, real complete ordered field, trace logic). In the broader Recognition forcing chain this sits inside native cost uniqueness for the J-cost, the T5 uniqueness step that forces $J(x)=(x+x^{-1})/2-1$ from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.