PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_iff_identity_comparable_trace
plain-language theorem explainer
The sharpened nonunit orbit-orientation target (local orientation plus identity-respecting comparable δ-traces) is equivalent to the identity-comparable-trace target alone. Anyone collapsing the two-branch nonunit coherence package to its identity half cites this. The proof is a two-arrow Iff term built from the projection lemma and the reverse embedding lemma.
Claim. The prime-calibration target that pairs local nonunit orbit orientation with identity orientation respecting comparability of finite $\delta$-orbit traces is logically equivalent to the identity-comparable-trace target alone: for every ratio-orbit character that is prime-direction calibrated, identity orientation respects comparable finite $\delta$-traces on nonunit directions.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio-orbit characters are maps on ratio orbits that encode admissible recognition cost structure. Prime-direction calibration restricts how those characters behave on prime generators of nonunit orbits. The identity branch is the orientation that keeps the recognition event at the J-cost minimum (ratio $1$); the reciprocal branch flips source and target and inverts the ratio.
The identity-comparable-trace target asserts that every prime-calibrated ratio character has identity orientation respecting comparability of finite $\delta$-orbit traces on nonunit directions. The orbit-orientation local comparable-trace target is the conjunction of a local nonunit orbit-orientation law with that same identity-comparable-trace law. Doc-comment: the latter is the "trace-layer version of the active local identity-transport target," with identity-transport replaced by its equivalent finite $\delta$-trace comparability law.
This declaration sits in the prime-floor successor blocker stack: adjacent nonunit orbit directions must not carry opposite identity/reciprocal orientations, and the identity half is the active obstruction.
proof idea
Term-mode Iff introduction. The forward arrow is the one-line projection ..._of_local_comparable_trace, which reads off the second conjunct of the orbit-orientation local target. The reverse arrow is ..._of_identity_comparable_trace, which rebuilds the full conjunction from the identity-comparable-trace target alone. No further tactic work; the equivalence is exactly those two lemmas packaged as $\langle\cdot,\cdot\rangle$.
why it matters
Collapses the two-conjunct nonunit orbit-orientation package to its identity-comparable-trace half, so later arguments need only attack or discharge one Prop. Downstream, PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_refuted applies the forward direction to reduce a refutation of the full target to a refutation of the identity half. The same equivalence feeds prc_native_cost_uniqueness_blocker_certificate and the conditional universal-foundation certificate in UniversalFoundation.
In the Recognition forcing picture this is bookkeeping inside native J-cost uniqueness (the T5 J-uniqueness lane), not a new physical law: it lets the prime-calibration blocker certify that the sharpened local-orientation target fails exactly when the identity-trace half fails. That keeps the native-cost uniqueness obstruction certificate honest about which conjunct is the live obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.