PRCCharacterNonunitBranchTransportPair_of_coherent
plain-language theorem explainer
Global coherence of nonunit orbit orientation (every nonunit direction is identity, or every one is reciprocal) implies the split two-branch transport pair: identity-branch transport and reciprocal-branch transport both hold for a ratio-orbit character. Native-cost uniqueness arguments cite this to convert a single orientation hypothesis into the full transport package. The proof is a one-line pair constructor from the two branch lemmas.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If nonunit orbit orientation is coherent for $\chi$ (every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented), then $\chi$ satisfies the split two-branch transport pair: both identity-branch transport and reciprocal-branch transport hold on nonunit orbits.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator display over a nonzero distinction-natural denominator. Characters act on these orbits; on nonunit directions they may orient either as identity or as reciprocal.
Coherence means the orientation is uniform across all nonunit directions: either every nonunit orbit direction is identity-oriented, or every one is reciprocal-oriented. The module doc for that predicate states this is "the exact coherence statement strong enough to rule out mixed product factors."
The target predicate is the split transport form of two-branch agreement: the conjunction of identity-branch transport and reciprocal-branch transport for nonunit orbits. Each conjunct is already known to follow from coherence alone; this declaration packages them.
proof idea
One-line term proof: construct the pair by applying the two upstream lemmas PRCCharacterNonunitIdentityBranchTransport_of_coherent and PRCCharacterNonunitReciprocalBranchTransport_of_coherent to the same coherence hypothesis. No further case analysis appears here; each component theorem already cases on the disjunction in coherence and discharges the corresponding transport goal.
why it matters
Native cost uniqueness in PRC needs characters that cannot mix identity and reciprocal factors on nonunit orbits. Coherence is the clean global hypothesis; the transport pair is the form downstream uniqueness machinery consumes.
The sole recorded consumer is prc_native_cost_uniqueness_blocker_certificate, which assembles the zero-calibrated factorization target and the refutation of signed-admissible factorization. This lemma sits on the path that forces the native cost to the unique J-shape (T5 in the forcing chain: $J(x)=(x+x^{-1})/2-1$), by ensuring branch transport is available once orientation is coherent.
It does not itself prove uniqueness of $J$; it only converts coherence into the two-branch transport interface those certificates require.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.