PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_branch_agreement
plain-language theorem explainer
Under prime calibration of a ratio character, full two-branch agreement on nonunit directions implies identity-branch transport to every nonunit direction. Cited by anyone assembling native-cost uniqueness targets or the conditional universal-foundation certificate. Proof is a one-line lift of the character-level implication through the quantified target hypotheses.
Claim. Assume that prime calibration forces nonunit branch agreement for every ratio character $\chi$. Then prime calibration also forces identity-branch transport: if any nonunit direction remains identity-oriented, that identity branch extends to every other nonunit direction.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how recognition cost orients along multiplicative directions. Nonunit directions are those not fixed as the unit orbit; each such direction carries an identity or reciprocal branch choice.
Two-branch agreement says that a branch choice fixed at one nonunit direction must match the corresponding branch at every other nonunit direction (both identity and reciprocal sides). Identity-branch transport is the one-sided positive form: if one nonunit direction is identity-oriented, that orientation is forced everywhere nonunit.
The targets here quantify those properties over all ratio characters that are prime-direction calibrated. Upstream, the character-level lemma already shows that branch agreement implies identity transport for a fixed $\chi$; this declaration only packages that implication at target level.
proof idea
One-line term wrapper. Introduce a calibrated ratio character $\chi$ from the identity-transport target. Apply the branch-agreement target hypothesis to obtain nonunit branch agreement for $\chi$. Feed that into PRCCharacterNonunitIdentityBranchTransport_of_branch_agreement, which projects the identity half of two-branch agreement and yields identity-branch transport for $\chi$.
why it matters
Closes the identity half of the branch-coupling blocker under prime calibration, the positive normal form used when native cost uniqueness is assembled from orientation data. Downstream, the pair-transport target theorem pairs this with the reciprocal twin; the local-orbit orientation theorem reuses it under a sharper local-agreement hypothesis. It also appears in the conditional universal-foundation certificate in UniversalFoundation, so any audit of the PRC foundation stack that tracks branch-coupling hypotheses lands here. Framework role is local to native-cost uniqueness scaffolding rather than a T0–T8 landmark, but it is on the path that makes the recognition cost uniquely the J-cost once calibration and orientation are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.