PRCCharacterNonunitReciprocalBranchTransport
plain-language theorem explainer
Property of a ratio-orbit map: if any single nonzero nonunit orbit direction is reciprocal-oriented, then every nonzero nonunit orbit direction is reciprocal-oriented. Isolates the dual half of two-branch agreement (Pass 57). Downstream uniqueness and calibration targets cite it as one conjunct of split transport. Pure definitional packaging of a universal quantification; no proof content.
Claim. For a map $\chi$ from ratio orbits to ratio orbits, the following holds: whenever a nonzero nonunit distinction orbit $p$ has reciprocal orientation under $\chi$ (i.e. $\chi$ sends the $p$-direction to its reciprocal), every nonzero nonunit distinction orbit $r$ likewise has reciprocal orientation under $\chi$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successors). A native unit is exactly the one-step orbit. Ratio orbits package a signed numerator over a nonzero distinction denominator.
A character here is a map $\chi$ on ratio orbits. Reciprocal orientation at a nonzero orbit direction $p$ means $\chi$ of that direction is cross-equal to the reciprocal of the direction: the character flips the branch rather than fixing it.
This module isolates native-cost uniqueness blockers. The present definition packages the reciprocal half of nonunit coherence: orientation type, once seen on one nonunit direction, transports to all nonunit directions. Its dual is the identity-branch transport form; together they form the split transport pair.
proof idea
Definitional, not a proved theorem. The body is the raw $\forall$-statement: for every nonzero nonunit $p$, if reciprocal orientation holds at $p$, then for every nonzero nonunit $r$ reciprocal orientation holds at $r$. It reuses the upstream reciprocal-orientation predicate (cross-equality of $\chi$ on the orbit direction with the reciprocal of that direction). No tactics or lemmas are applied.
why it matters
Pass 57 isolates this as the dual half of two-branch agreement. It is one conjunct of the split transport pair (identity branch transport and reciprocal branch transport). Downstream, branch-agreement and nonunit-orientation-coherence each imply this property by projecting the reciprocal half.
It appears in the native-cost uniqueness blocker certificate as an exact Lean target, and as the conclusion of the prime-calibration forces-reciprocal-transport target. That target is separately refuted (a two-adic axis twist character is prime-calibrated yet fails full reciprocal transport), so the definition marks a precise obstruction rather than a closed uniqueness step. In the broader forcing chain it sits under native $J$-cost uniqueness work feeding T5-style cost rigidity, without yet forcing the unique cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.