PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_iff_comparable_trace
plain-language theorem explainer
Equates two formulations of the same branch-coupling blocker under prime calibration: identity-branch transport across all nonunit directions is equivalent to identity orientation respecting comparable finite δ-orbit traces. Cited when refuting the blocker or assembling native-cost uniqueness certificates. Proof is the bidirectional pair of the already-proved one-way implications.
Claim. Under prime direction calibration of a ratio character, the following are equivalent: (i) if any nonunit direction is identity-oriented, that identity branch transports to every nonunit direction; (ii) identity orientation respects comparability of finite $\delta$-orbit traces on nonunit directions.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit, subject to algebraic constraints that encode admissible cost structure. Prime direction calibration restricts how $\chi$ may act on prime-generated directions. Nonunit directions are those away from the unit orbit; an identity-oriented branch keeps the character fixed rather than reciprocal on such a direction.
The branch-transport target says that if prime calibration leaves even one nonunit direction identity-oriented, that orientation must propagate to every nonunit direction. The comparable-trace target sharpens the same demand in trace order: identity orientation must respect comparability of finite $\delta$-orbit traces among nonunit directions. Both are blocker-shaped hypotheses in the native-cost uniqueness development: they name what would have to hold for certain non-unique cost characters to survive prime calibration.
The two one-way implications between these targets are already proved in-module; this declaration packages them as a single equivalence.
proof idea
Term-mode Iff introduction. The forward direction applies the existing lemma that branch transport yields the comparable-trace target; the reverse applies the lemma that the comparable-trace target yields branch transport. Each of those lemmas is itself a short intro-and-specialize argument reducing to the corresponding character-level implication. No new algebraic content is introduced here.
why it matters
This equivalence is the hinge used to refute the branch-transport blocker: the refutation theorem assumes the transport target, converts via the forward direction of this iff, and invokes the already-established refutation of the comparable-trace target. That refutation feeds the native-cost uniqueness blocker certificate and, upstream of the universal foundation stack, the conditional PRC foundation certificate.
In the Recognition Science forcing picture, native cost uniqueness is the local uniqueness step that pins the J-cost (T5) once ratio characters and prime calibration are fixed. Closing or refuting these branch-coupling targets removes residual freedom in how identity versus reciprocal branches can sit on nonunit directions, which is required before the mass ladder and constant normalizations can be treated as forced rather than optional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.