reciprocal_character_prime_calibrated
plain-language theorem explainer
The reciprocal map on rational orbits is calibrated on every native prime direction: the cost it generates agrees with canonical J-cost on each prime orbit. Anyone assembling admissible ratio characters or closing native-cost uniqueness blockers cites this. The proof is a short reduction through reciprocal symmetry of the PRC cost and symmetry of cross-equality.
Claim. Let $\chi$ send each rational orbit $q$ to its reciprocal $q^{-1}$. Then $\chi$ is prime-direction calibrated: for every native prime $p$ (with prime-orbit witness), the cost generated by $\chi$ at the prime direction of $p$ is cross-equal to the canonical cost of that same prime direction.
background
In the Primitive Recognition Calculus, rational quantities live as RatioOrbit displays: a signed integer numerator over a nonzero distinction-natural denominator. Reciprocal is total on these orbits (zero maps to zero, as on $\mathbb{Q}$). The canonical PRC cost on ratio orbits is written onRatioOrbit; a general character $\chi$ generates a cost by composing, costFromCharacter(\chi,q) = onRatioOrbit(\chi(q)).
Prime-direction calibration asks that this generated cost match the canonical cost, up to cross-equality of orbits, on every native prime direction. Cross-equality is the balanced identification of signed orbits; it is symmetric. Upstream, reciprocal symmetry of the PRC rational cost already gives that the canonical cost of $q$ is cross-equal to the canonical cost of $q^{-1}$.
The local module develops uniqueness and obstruction structure for native costs built from ratio characters, with calibration on primes as a sharp intermediate target.
proof idea
Fix a native prime $p$ with prime-orbit witness. The goal is cross-equality between costFromCharacter of the reciprocal character at the prime direction and the canonical cost of that direction. Unfolding the character cost, this is cross-equality of the canonical cost of the reciprocal of the prime direction with the canonical cost of the prime direction itself. Apply reciprocal symmetry of the PRC cost at that prime direction, then reverse the equality by symmetry of cross-equality. A simpa closes the definitional match.
why it matters
This is the calibration half of the reciprocal admissible ratio character: downstream reciprocal_admissible_ratio_character packages reciprocal as a ratio character that is prime-calibrated (and carries the remaining admissibility fields). The same fact is the witness fed into the refutation that prime calibration forces orbit-successor additive compatibility: the reciprocal character is prime-calibrated yet fails successor-additive compatibility, so that forcing target is false.
Both feed the native-cost uniqueness blocker certificate, which records what is proved versus refuted on the uniqueness surface. In the broader RS chain this sits under J-cost uniqueness (T5): characters that generate costs agreeing with canonical $J$ on prime axes are the candidates one must control before claiming a unique native cost. Reciprocal is the basic nontrivial involution that still matches $J$ on primes via reciprocal symmetry of $J$ itself (equivalently of onRatioOrbit).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.