PRCCharacterNonunitBranchAgreement_of_local_identity_branch_transport
plain-language theorem explainer
Local identity-or-reciprocal orientation of every nonunit orbit direction, plus one-way identity branch transport, already forces the full two-branch coupling law: identity (resp. reciprocal) orientation at any nonunit direction propagates to every other nonunit direction. Cited by the prime-calibration-to-branch-agreement target and the native-cost uniqueness blocker certificate. Term proof: identity half is transport; reciprocal half uses local orientation and a crossEq self-reciprocal contradiction.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose every nonunit orbit direction is locally oriented (identity or reciprocal), and suppose identity orientation at any one nonunit direction transports to identity at every nonunit direction. Then full nonunit branch agreement holds: for any nonunit directions $p,r$, identity at $p$ implies identity at $r$, and reciprocal at $p$ implies reciprocal at $r$.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed numerator orbits over nonzero denominators. Cross-equivalence crossEq is the internal PRC rational equality (balanced cross-multiplication of signed orbits); it is symmetric and transitive. Each nonzero distinction position $p$ has an associated ratio direction orbitDirection $p$ (numerator the signed orbit of $p$, denominator one). Reciprocal is the total reciprocal on ratio orbits.
A character $\chi$ on ratio orbits orients each nonunit direction as identity-type or reciprocal-type relative to $\chi$. Local orientation asserts that every nonunit direction is one or the other. Identity branch transport is the one-way coupling: if any nonunit direction is identity-oriented, all are. Branch agreement is the two-sided global law: identity transports identity and reciprocal transports reciprocal across all nonunit pairs.
The module develops native-cost uniqueness for PRC characters. The nonunit branch law is the nonprime analogue of already-proved prime-axis orientation coupling, needed before cost-from-character uniqueness can close.
proof idea
Term-mode proof of the two conjuncts for arbitrary nonunit $p,r$.
Identity half: apply identity branch transport directly from $p$ to $r$.
Reciprocal half: case-split local orientation at $r$. If $r$ is reciprocal-oriented, done. If $r$ is identity-oriented, transport identity from $r$ back to $p$. Combined with the reciprocal hypothesis at $p$, symmetry and transitivity of crossEq yield that orbitDirection $p$ is cross-equivalent to its own reciprocal. That contradicts orbitDirection_nonunit_not_crossEq_recip (a nonunit direction cannot equal its reciprocal under crossEq). Hence the identity case at $r$ is impossible under a reciprocal hypothesis at $p$, and only the reciprocal branch at $r$ survives.
why it matters
Branch agreement is the global no-mixing law for nonunit orbit directions under a PRC character. Without it, identity and reciprocal orientations could mix across factors and the doubled-trace / native-cost reconstruction would not be forced to a single branch.
Downstream, PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_local_identity_transport reduces the prime-calibration target to this lemma once local identity transport is known. That feeds the native-cost uniqueness blocker certificate, which packages the proved factorization and refutation targets for the uniqueness program.
In the broader Recognition Science chain this sits under T5 J-uniqueness: native cost must be the unique character compatible with the Recognition Composition Law and calibration. Closing nonunit branch coupling is a structural step toward forcing $J(x)=(x+x^{-1})/2-1$ as the only admissible cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.