PRCPrimeCalibrationForcesOrbitSuccessorAdditiveCompatibilityTarget_refuted
plain-language theorem explainer
Prime calibration of a ratio character does not force additive successor compatibility on nonzero orbit directions; that universal target is false. Native-cost uniqueness work cites this as a closed negative. The proof is a short counterexample: the reciprocal map on ratio orbits is a prime-calibrated ratio character that fails successor-additive compatibility.
Claim. It is false that every map $\chi$ from rational orbits to rational orbits which is a ratio character and prime-direction calibrated must be orbit-successor additive compatible. In particular, prime calibration does not force $\chi$ to respect additive successor on nonzero orbit directions.
background
In the primitive recognition calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). The total reciprocal on these orbits mirrors $q\mapsto 1/q$ on $\mathbb{Q}$, sending the zero orbit to itself (K4.12).
A ratio character is a structure-preserving map on these orbits used to build native costs via costFromCharacter. Prime-direction calibration asks that the character act correctly on prime orbit directions. Orbit-successor additive compatibility is the stronger demand that the character intertwine the additive successor operation on nonzero orbit directions.
The target proposition packages the hope that the first two properties already force the third for every character. Upstream work already shows the reciprocal character is a ratio character, is prime-calibrated, and is not successor-additive compatible (the last by reducing a one-step successor identity to a false rational equality via crossEq_iff_toRat_eq).
proof idea
Term-mode reductio. Assume the universal target. Instantiate it at the reciprocal map $\chi(q)=\mathrm{recip}(q)$, feeding the known facts that this map is a ratio character and is prime-direction calibrated. The target then yields successor-additive compatibility of reciprocal. Discharge by the prior lemma that reciprocal is not successor-additive compatible. No further case analysis.
why it matters
This closes a false branch in the native-cost uniqueness program: the "sharper additive successor target" overclaimed what prime calibration can force. The module doc after the reciprocal check records the corrected aim: prime calibration should force successor transport above the self-reciprocal unit floor, not additive transport out of the unit orbit itself.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, the sharpened replacement for the opaque native uniqueness blocker. In the Recognition forcing chain this sits under foundation work that isolates which character axioms can pin the J-cost (T5) rather than merely constrain orbit arithmetic. Refuting the over-strong target keeps the uniqueness ledger honest: blockers must be real, not wishful universal claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.