PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_refuted
plain-language theorem explainer
The two-branch agreement target is false: prime calibration of a ratio character does not force nonunit branch choices to agree across all nonunit directions for both identity and reciprocal branches. Anyone auditing PRC native-cost uniqueness blockers or the universal-foundation certificate would cite this. The proof reduces the claim through an equivalence to the transport-pair form and applies that form's prior refutation.
Claim. It is not the case that every ratio-orbit character $\chi$ that is prime-direction calibrated necessarily satisfies nonunit branch agreement (identity and reciprocal branches agreeing across all nonunit directions).
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits encoding how recognition cost transforms under multiplicative structure. Prime-direction calibration is the constraint that the character is fixed on a preferred prime direction; nonunit branch agreement asks that, once calibrated, the identity and reciprocal branch choices at one nonunit direction match those at every other nonunit direction.
The agreement target packages that expectation as a universal Prop: every prime-calibrated ratio character should enjoy nonunit branch agreement. A sibling target restates the same demand in transport-pair language (local orientation plus two-branch coupling). An in-module equivalence identifies the two formulations.
This module sits in the native-cost uniqueness development: it isolates which calibration hypotheses actually force uniqueness of the native cost and which over-strong targets fail.
proof idea
Short reduction proof. Assume the agreement target. Apply the forward direction of the in-module equivalence relating agreement to the transport-pair target, obtaining the transport-pair form. Discharge by the already-proved refutation of that transport-pair target (itself reduced to the reciprocal-branch transport refutation). No new analytic work; pure Prop chaining.
why it matters
Closes a negative leaf in the PRC native-cost uniqueness tree: the naive hope that prime calibration alone forces global two-branch agreement is ruled out. Downstream, the universal-foundation conditional certificate in UniversalFoundation consumes this refutation among its kernel and trace-logic ingredients, so the certificate does not silently assume a false calibration lemma.
In the broader Recognition forcing chain this is housekeeping rather than a T5–T8 landmark: it prevents an over-strong branch-coupling hypothesis from contaminating uniqueness arguments for the native cost built from the J-cost and doubled-trace structure. The positive path must use weaker, actually forced coupling (local orientation plus controlled transport), not full nonunit agreement from prime calibration alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.