PRCCharacterNonunitBranchAgreement_of_coherent
plain-language theorem explainer
Global coherence of nonunit orbit orientations (all identity or all reciprocal) implies the two-branch transport law: identity at one nonunit forces identity everywhere nonunit, and likewise for reciprocal. Anyone proving native cost uniqueness or prime-calibration branch targets cites this. The proof is a two-case split on the coherence disjunction, with the mixed branch ruled out by nonunit directions never equaling their reciprocal under cross-multiplication.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If nonunit orbit orientation under $\chi$ is coherent (every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented), then $\chi$ satisfies nonunit branch agreement: for any two nonunit positions $p,r$, identity orientation at $p$ implies identity at $r$, and reciprocal orientation at $p$ implies reciprocal at $r$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit displays (signed numerator over nonzero distinction denominator). Cross-multiplication equivalence crossEq is the internal rational equality on those displays; it is symmetric and transitive. Each nonzero orbit position $p$ has a canonical direction orbitDirection p (the ratio with numerator the signed orbit of $p$ and denominator one). Reciprocal is the total involution on ratio orbits sending zero to zero.
A character $\chi$ orients each such direction as identity or reciprocal. Coherence means the choice is uniform on all nonunit positions: either every nonunit direction is identity-oriented, or every one is reciprocal-oriented. The doc-comment states this is "the exact coherence statement strong enough to rule out mixed product factors."
Branch agreement is the transport form of the same idea: identity at any one nonunit forces identity at every nonunit, and reciprocal likewise. The module develops native cost uniqueness from character and doubled-trace structure; this lemma converts a global orientation hypothesis into the pairwise coupling law used downstream.
proof idea
Term-mode case split on the coherence disjunction.
If every nonunit is identity-oriented: the identity-transport half is immediate by applying the global identity hypothesis at the target $r$. The reciprocal-transport half is impossible: assuming reciprocal at $p$ together with identity at $p$ yields, via crossEq_symm and crossEq_trans, that orbitDirection p is crossEq its own reciprocal; orbitDirection_nonunit_not_crossEq_recip contradicts that for nonunits.
If every nonunit is reciprocal-oriented: symmetric. Reciprocal transport is immediate; identity transport produces the same self-reciprocal crossEq and the same contradiction.
No external analytic lemmas; only orbit cross-equivalence algebra and the nonunit non-self-reciprocal fact.
why it matters
Native cost uniqueness in PRC needs characters that cannot mix identity and reciprocal factors on nonunit orbits. This theorem is the pure logical bridge from the global coherence predicate to the two-branch agreement law that downstream targets quote.
It feeds three parents: the local-orientation iff relating branch agreement to coherence; PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_coherent, a one-line wrapper that applies this result under prime calibration; and the native-cost uniqueness blocker certificate chain that packages factorization targets. In the Recognition forcing picture this sits under J-uniqueness and the Recognition Composition Law: characters that respect the cost must pick a single branch on nonunits so the doubled-trace d'Alembert structure stays consistent with the unique J-cost.
No open scaffold here; the claim is fully proved and closes the coherence-to-agreement step of the uniqueness pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.