PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget
plain-language theorem explainer
Packages the two one-way nonunit branch-transport obligations under prime calibration into a single Prop: identity-branch transport and reciprocal-branch transport must both hold for every ratio character that is prime-direction calibrated. Downstream uniqueness and agreement lemmas cite this pair as the transport half of an equivalence with nonunit branch agreement. The body is a pure conjunction of the two existing target Props.
Claim. The nonunit branch-transport pair target is the conjunction of: (i) every prime-direction-calibrated ratio character forces identity orientation on one nonunit direction to transport to all nonunit directions, and (ii) every such character forces reciprocal orientation on one nonunit direction to transport to all nonunit directions.
background
In the Primitive Recognition Calculus, ratio characters assign orientations on ratio orbits. Prime-direction calibration is the single-anchor constraint that pins character behaviour on prime generators. Nonunit directions are orbits away from the identity event (the J-cost minimum at state $1$).
Two one-way transport targets already exist. The identity-branch target says: if prime calibration leaves one nonunit direction identity-oriented, that identity branch must transport to every nonunit direction. The reciprocal-branch target is the dual statement for reciprocal orientation. Finite traces (empty or extended by distinction acts) supply the underlying ordered data those transports compare.
This module packages native-cost uniqueness blockers and repaired interfaces. The pair target is the split form of the two one-way transports, kept separate so each leg can be proved, transported, or refuted independently before reassembly into branch agreement.
proof idea
Definitional abbreviation only: the Prop is the conjunction of the identity-branch transport target and the reciprocal-branch transport target. No tactics, no lemmas applied at this site. Consumers project with .1 / .2 or rebuild the pair from branch-agreement hypotheses via the sibling of-transport and of-agreement bridges.
why it matters
Gives a single named surface for both one-way nonunit transports under prime calibration, which is exactly what the agreement↔transport equivalence needs. Downstream, branch agreement is recovered from the pair, the pair is recovered from agreement, and the two are proved equivalent. A later theorem refutes the pair by refuting its reciprocal conjunct, so this definition also pins the exact negative entry on the universal-foundation open-target ledger.
In the Recognition forcing picture this sits inside native-cost uniqueness for PRC characters (the J-cost / RCL layer that feeds T5 J-uniqueness), not a new physical constant. It records which transport route cannot force the final uniqueness surface once prime calibration is assumed, while keeping the identity leg available for repaired interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.