PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_iff_transport_pair
plain-language theorem explainer
Prime calibration forces global nonunit two-branch agreement if and only if it forces the pair of one-way identity and reciprocal branch transports. Anyone tracking the nonunit branch-coupling blocker in native cost uniqueness will cite this equivalence. The proof is a pure Iff constructor from the two already-proved one-way implications.
Claim. The following are equivalent: (i) every ratio-orbit character that is prime-direction calibrated has nonunit branch agreement (identity and reciprocal branches agree across all nonunit directions); (ii) every such character satisfies both one-way nonunit branch transports (identity-branch transport and reciprocal-branch transport).
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi$ assign orbit data on ratio orbits. Prime-direction calibration is the hypothesis that $\chi$ is fixed on a preferred prime direction. Nonunit directions are those away from the unit orbit; each carries an identity branch and a reciprocal branch.
The agreement target asserts that, under prime calibration, a nonunit branch choice at one direction must match every other nonunit direction for both branches. The transport-pair target splits that demand into two one-way statements: identity-branch transport and reciprocal-branch transport. The module treats the pair as the positive normal form of the global nonunit branch-coupling blocker.
Upstream, each direction of the equivalence is already available: transport pair implies agreement via the character-level transport-to-agreement lemma, and agreement implies the transport pair by projecting onto the identity and reciprocal transport targets.
proof idea
Term-mode Iff introduction. The forward arrow is PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget_of_branch_agreement (agreement yields both one-way transports). The reverse arrow is PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_transport_pair (the pair of transports yields agreement by applying the character-level transport-pair lemma pointwise). No new algebra; pure packaging of the two implications.
why it matters
This bridge lets the development refute the agreement target by refuting the transport pair. Downstream, PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_refuted applies the forward direction of the iff and then the transport-pair refutation. The same packaging feeds the conditional universal-foundation certificate path in prc_universal_foundation_conditional_certificate, which assembles kernel, real-complete ordered field, and trace-logic certificates.
In the Recognition forcing chain this sits inside native J-cost uniqueness infrastructure (T5 J-uniqueness and the Recognition Composition Law background): branch coupling on nonunit directions is part of locking the cost character before phi and the eight-tick structure are forced. The declaration itself closes no open physics claim; it only equates two blocker formulations so a single refutation discharges both.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.