PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_refuted
plain-language theorem explainer
Refutes the corrected successor-transport target: prime-direction calibration of a ratio character does not force identity successor transport above the self-reciprocal unit floor. Cited by the native-cost uniqueness blocker certificate and by later refutations in the same chain. Proof is a one-step reduction through an equivalence to a previously refuted identity-witness globalization target.
Claim. It is false that every ratio-orbit character $\chi$ that is prime-direction calibrated has prime-floor orbit identity successor transport (successor transport above the self-reciprocal unit floor, not additive transport out of the unit orbit).
background
In the Primitive Recognition Calculus, cost uniqueness is probed by ratio-orbit characters: maps $\chi$ on ratio orbits that obey the PRC character axioms and can be calibrated along prime directions. After the reciprocal-character check, the natural corrected target is that such calibration should force successor transport above the self-reciprocal unit floor, rather than additive transport leaving the unit orbit itself.
That corrected target is packaged as a universal quantification: every prime-direction-calibrated ratio character has prime-floor orbit identity successor transport. An in-module equivalence rewrites the same claim as a witness-globalization statement: if any calibrated prime axis picks identity, then every nonunit orbit direction must pick identity.
The sibling refutation of that globalization form is already available; the present result closes the equivalent floor-successor packaging.
proof idea
Term-mode one-step reduction. Assume the floor-successor transport target. Apply the left-to-right direction of the in-module equivalence that identifies it with the prime-identity-witness globalization target on nonunits. Feed the resulting hypothesis into the already-proved refutation of that globalization target, yielding a contradiction. No new arithmetic or character analysis is performed here.
why it matters
This is one link in the PRC native-cost uniqueness blocker chain. Downstream, it is applied directly to refute the nonunit-identity comparable-trace target and the prime-floor identity successor-step-pair target, each by the same equivalence-then-refute pattern. It also contributes to the native-cost uniqueness blocker certificate and is visible from the universal-foundation conditional certificate in UniversalFoundation.
In framework terms it narrows which prime-calibration consequences can be forced on characters before native cost is unique. It does not itself establish J-uniqueness (T5) or the Recognition Composition Law; it only eliminates one corrected successor-transport packaging that would have over-constrained calibrated characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.