PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_identity_comparable_trace
plain-language theorem explainer
Prime calibration forcing product no-mixing of identity/reciprocal orientations is equivalent to forcing identity orientation to respect comparable finite δ-orbit traces on nonunit directions. Anyone chaining orientation targets toward native cost uniqueness cites this bridge. The proof is a two-direction term: one side via product-to-comparable-trace, the other via comparable-trace to branch transport then back to no-mixing.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character has no mixed identity/reciprocal factor orientations under native orbit multiplication; (ii) every such character has identity orientation that respects comparability of finite $\delta$-orbit traces on nonunit directions.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ assign orientations on ratio orbits. Prime-direction calibration constrains how $\chi$ behaves on prime generators. Two intermediate targets appear in the native-cost uniqueness ladder.
The product no-mixing target asserts that, under native multiplication of orbits, a calibrated character never mixes identity and reciprocal factor orientations. The comparable-trace target is a trace-order sharpening: on nonunit directions, identity orientation must respect comparability of finite $\delta$-orbit traces.
Between them sits nonunit identity branch transport: a coherent choice of identity branch across nonunit directions. Upstream lemmas already show product no-mixing implies branch transport implies comparable-trace (and the reverse chain through branch transport), so the two top-level targets are interchangeable once those arrows are assembled.
proof idea
Term-mode biconditional constructor. Left-to-right applies PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_product_no_mixed, which routes product no-mixing through branch transport into the comparable-trace target.
Right-to-left takes a comparable-trace hypothesis, lifts it by PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_comparable_trace to identity branch transport, then applies PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_identity_branch_transport to recover product no-mixing. No new analytic content; pure composition of already-proved one-way arrows.
why it matters
This iff collapses two named blockers on the path to native cost uniqueness into one obligation. Downstream, PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_successor_step_pair uses the reverse direction to discharge product no-mixing from a successor-step-pair hypothesis, and PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationTarget_of_identity_comparable_trace continues from the comparable-trace side toward local orientation propagation.
Both feed the native-cost uniqueness blocker certificate and, further out, the conditional universal-foundation certificate. In the Recognition forcing chain this is bookkeeping inside the J-cost uniqueness story (T5): orientation coherence on the ratio lattice is what lets the native cost match the unique $J$ solving the Recognition Composition Law, rather than a mixed-branch impostor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.