PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget_of_branch_agreement
plain-language theorem explainer
Prime calibration that forces nonunit branch agreement also forces the paired one-way nonunit branch transports (identity and reciprocal). Anyone wiring the native-cost uniqueness ladder or the agreement↔transport equivalence cites this packaging step. The proof is a term-mode pair constructor that applies the two one-direction transport-from-agreement lemmas.
Claim. Assume the two-branch agreement target: for every ratio character $\chi$ that is prime-direction calibrated, nonunit branch choices agree across directions on both the identity and reciprocal branches. Then the split transport-pair target holds: both the identity-branch nonunit transport target and the reciprocal-branch nonunit transport target are forced by the same prime calibration.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a structure-preserving map on ratio orbits. Prime-direction calibration pins how $\chi$ behaves on a distinguished prime direction. Nonunit directions then carry two branch choices: an identity orientation and a reciprocal orientation.
The agreement target asserts that, once prime calibration is in force, a nonunit branch choice fixed in one direction must match every other nonunit direction, for both branches. The transport-pair target splits that global coupling into two one-way obligations: identity-branch transport and reciprocal-branch transport (each a trace-order sharpening that orientation respect comparability of finite $\delta$-orbit traces).
Locally this module builds native-cost uniqueness from character and doubled-trace hypotheses. The agreement and transport-pair props are intermediate blockers on the path from prime calibration to unique native cost.
proof idea
Term-mode And-introduction. Feed the agreement hypothesis into the identity transport-from-agreement lemma and into the reciprocal transport-from-agreement lemma; the resulting pair is exactly the transport-pair target. No new quantification or character reasoning occurs here; both one-way lemmas already unpack agreement into the corresponding transport prop.
why it matters
This is the forward half of the in-module equivalence between the two-branch agreement target and the split transport-pair target. That iff lets later steps treat agreement and paired transport as interchangeable normal forms of the same nonunit branch-coupling blocker.
Downstream it is consumed by the universal-foundation conditional certificate, which packages kernel, real-complete ordered field, and trace-logic certificates into the PRC foundation stack. In the broader Recognition chain this sits under native-cost uniqueness for the J-cost forced at T5 ($J(x)=(x+x^{-1})/2-1$), before phi self-similarity and the eight-tick octave. It does not itself close uniqueness; it only collapses two formulations of the branch-coupling obligation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.