PRCCharacterNonunitReciprocalBranchTransport_of_coherent
plain-language theorem explainer
Coherent nonunit orbit orientation forces reciprocal branch transport: if any nonunit direction is reciprocal-oriented, every nonunit direction is. Cited when assembling two-branch agreement for native cost uniqueness. Proof is a two-case split on global identity versus global reciprocal coherence, with the identity case ruled out by a nonunit direction–reciprocal cross-equality contradiction.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose nonunit orbit orientation under $\chi$ is coherent: every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented. Then reciprocal branch transport holds: whenever one nonunit direction $p$ is reciprocal-oriented under $\chi$, every nonunit direction $r$ is reciprocal-oriented under $\chi$.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from a signed-orbit numerator and a nonzero distinction-nat denominator. Cross-equality is the internal PRC rational relation: two orbits match when scaled numerators balance under cross-multiplication. The reciprocal of a ratio orbit is the total reciprocal (zero maps to zero).
Each nonzero distinction position $p$ has an orbit direction: the ratio orbit with numerator the signed orbit of $p$ and denominator one. A character $\chi$ orients that direction either as identity or as reciprocal. Nonunit orbit orientation is coherent when the choice is uniform across all nonunit positions: all identity, or all reciprocal. That uniformity is exactly strong enough to rule out mixed product factors.
Reciprocal branch transport is the dual half of two-branch agreement: if any one nonunit direction is reciprocal-oriented, every nonunit direction must be. The companion identity-transport statement is the other half.
proof idea
Introduce a nonunit $p$ assumed reciprocal-oriented and an arbitrary nonunit $r$. Case-split the coherence hypothesis.
Identity branch: coherence gives identity orientation at $p$. Symmetry and transitivity of cross-equality then produce cross-equality between the orbit direction of $p$ and its reciprocal. That contradicts the lemma that a nonunit orbit direction is never cross-equal to its reciprocal. Eliminate.
Reciprocal branch: coherence already asserts reciprocal orientation at every nonunit, so apply it at $r$.
why it matters
This is one half of the pair that upgrades global nonunit orientation coherence into two-branch transport. The immediate parent packages identity transport and reciprocal transport into a single branch-transport pair under the same coherence hypothesis.
That pair feeds the native-cost uniqueness blocker certificate in this module, which records zero-calibrated factorization targets and refutations used to pin the unique native cost character. In the broader Recognition forcing chain, native cost uniqueness supports the J-cost identification (T5) and the Recognition Composition Law route to the self-similar fixed point $\phi$.
Pass 57 isolates this reciprocal half so mixed-branch characters cannot sneak past the uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.