PRCCharacterNonunitIdentityBranchTransport_of_comparable_trace
plain-language theorem explainer
From the assumption that identity orientation of a nonunit orbit direction transports along comparable δ-orbit traces, one obtains global nonunit identity-branch transport: identity at any single nonunit direction forces identity at every nonunit direction. Anyone closing native-cost uniqueness for ratio characters would cite this. The argument is a one-line reduction that inserts structural comparability of all orbit-position traces.
Claim. Let $\chi$ be a map on rational orbits. Suppose that whenever two nonunit orbit directions have comparable finite $\delta$-orbit traces (one extends the other), identity orientation of $\chi$ at the first direction transports to the second. Then identity orientation of $\chi$ at any one nonunit direction forces identity orientation at every nonunit direction.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-natural denominator. Characters act as maps $\chi$ on these orbits. Local orientation data record whether a given nonunit orbit direction is identity-oriented under $\chi$.
Two formulations of nonunit coherence appear. Global identity-branch transport says: if one nonunit direction is identity-oriented, every nonunit direction is. The comparable-trace form weakens the quantifiers: transport is required only when the two finite $\delta$-orbit position traces are comparable under the extension order. The module treats the latter as the next proof obligation because it exposes a pure trace-order law.
Upstream, every pair of orbit-position traces is already known to be comparable: for any distinction-naturals $p,r$, one of $\mathrm{orbitPositionTrace},p$ and $\mathrm{orbitPositionTrace},r$ extends the other. That structural fact is what collapses the two formulations.
proof idea
Term-mode reduction after introducing the branch-transport quantifiers. Given a nonunit identity-oriented source $p$ and an arbitrary nonunit target $r$, apply the comparable-trace hypothesis to $p$ and $r$. The missing comparability premise is discharged by orbitPositionTrace_comparable, which supplies the disjunction of trace extensions for every pair. The identity hypothesis at $p$ then yields identity at $r$. No further character algebra is used.
why it matters
This is one half of the equivalence between the trace-order and global forms of nonunit identity transport. The sibling iff theorem packages both directions and is the clean interface for later steps.
Downstream, prime-calibration forcing targets are rewritten from the comparable-trace shape into the branch-transport shape by applying this lemma. The native-cost uniqueness blocker certificate sits further along the same chain: uniqueness of the native cost character needs nonunit coherence, and this transport law is the form that certificate infrastructure consumes.
In the broader Recognition forcing picture, native-cost uniqueness is the PRC-side route toward the unique $J$-cost (T5) and the Recognition Composition Law. Closing branch transport removes a named blocker between local orientation data and global character rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.