PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted
plain-language theorem explainer
Refutes the claim that prime-direction calibration of a ratio character forces reciprocal orientation to transport across every nonunit prime orbit. Cost-uniqueness and calibration auditors cite it to drop an over-strong dual-transport target. The proof is a concrete counterexample: the two-adic axis-twist character is calibrated, reciprocal at the 2-orbit, yet forced identity at the 3-orbit, contradicting nonunit directions being cross-equal to their reciprocals.
Claim. It is false that every map $\chi$ on ratio orbits that is a ratio character and is prime-direction calibrated must have nonunit reciprocal branch transport: reciprocal orientation at one nonunit prime direction need not transport to every other nonunit prime direction.
background
In the Primitive Recognition Calculus, rationals are displayed as RatioOrbit values: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is the choice-free cross-multiplication relation crossEq (K4.10): two orbits match when scaled numerators balance. Reciprocals are total on these displays (recip), sending the zero class to itself.
A ratio character $\chi$ assigns to each orbit another orbit and is constrained by calibration and branch data. Prime-direction calibration fixes how $\chi$ orients distinguished prime orbits (the 2-orbit, 3-orbit, etc.). Nonunit reciprocal branch transport is the dual-transport demand: if one nonunit prime direction is oriented reciprocally, that reciprocal orientation must hold at every other nonunit prime direction.
The module studies which of these transport targets are forced by native cost hypotheses and which are not. The two-adic axis-twist character is a concrete calibrated character whose branch data already fix reciprocal orientation at 2 and identity orientation at every other prime orbit.
proof idea
Assume the universal target and instantiate it at the two-adic axis-twist character. Upstream calibration of that character supplies prime-direction calibration, so the target yields nonunit reciprocal branch transport for it.
Branch data give reciprocal orientation at twoOrbit. Transport then forces reciprocal orientation at threeOrbit. Separately, the same branch data give identity orientation at threeOrbit (it is not the 2-orbit). Symmetry and transitivity of crossEq therefore make the 3-orbit direction cross-equal to its own reciprocal.
That contradicts orbitDirection_nonunit_not_crossEq_recip at the nonunit 3-orbit. Hence the universal target is false.
why it matters
This is one half of the dual-transport cleanup in native-cost uniqueness. Immediately downstream, PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget_refuted quotes it on the reciprocal component of the paired target, so both one-way nonunit branch transports are discharged as non-forced.
The refutation also feeds prc_universal_foundation_conditional_certificate in UniversalFoundation: the certificate packages kernel, real-field, and trace-logic facts without relying on an over-strong dual-transport axiom. In the broader Recognition chain this keeps cost uniqueness pinned to J-cost structure and monotone d'Alembert data (T5 J-uniqueness, RCL) rather than to an incorrect global reciprocal-transport law on prime orbits.
No scaffolding remains on this target: the counterexample is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.