PRCPrimeCalibrationForcesNonunitBranchAgreementTarget
plain-language theorem explainer
Packages the claim that every prime-calibrated ratio character automatically satisfies two-branch nonunit agreement: identity (resp. reciprocal) orientation at one nonunit direction transports to every other nonunit direction. Cited by the native-cost uniqueness chain when reducing global branch-coupling blockers to prime calibration. Pure definitional packaging of a universal quantification over characters; no proof content.
Claim. The target proposition asserts: for every map $\chi$ from ratio orbits to ratio orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), $\chi$ satisfies nonunit branch agreement (any nonunit identity-oriented direction transports identity to every nonunit direction, and likewise for the reciprocal branch).
background
In the Primitive Recognition Calculus, costs are recovered from ratio characters via a d'Alembert factorization. A ratio orbit is an integer numerator over a nonzero orbit denominator. A ratio character $\chi$ is a map on ratio orbits that sends the unit orbit to itself and is multiplicative, both up to cross-equivalence (the quotient-native equality used throughout PRC).
Prime-direction calibration means that the cost built from $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. Nonunit branch agreement is the two-branch form of the global branch-coupling law: once a nonunit direction is identity-oriented (resp. reciprocal-oriented), that orientation transports to every other nonunit direction.
This module studies which calibration hypotheses force uniqueness of the native cost. The present definition is the named target proposition for the claim that prime calibration alone already yields full nonunit branch agreement.
proof idea
No proof. The declaration is a bare Prop abbreviation: universal quantification over maps $\chi$, with hypotheses that $\chi$ is a ratio character and is prime-direction calibrated, concluding nonunit branch agreement. Downstream lemmas unpack or refute this packaged statement; nothing is proved at this site.
why it matters
This target is the positive normal form of the global nonunit branch-coupling blocker in the native-cost uniqueness program (local orientation plus two-branch agreement). It sits between prime calibration of characters and the full coupling law needed to pin the cost to canonical $J$.
Downstream, it is shown equivalent to a transport-pair target, implied by orbit-orientation coherence and by local identity transport, and used to derive identity and reciprocal branch-transport targets. Critically, the module also proves the target is false: prime calibration does not force nonunit branch agreement. That refutation closes a false path in the uniqueness forcing chain and forces stronger hypotheses (coherence or local transport) rather than bare prime calibration.
In the broader RS forcing picture this is local scaffolding around T5 $J$-uniqueness: characters that match $J$ on primes need extra structure before the Recognition Composition Law and global cost uniqueness follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.