recip_toRat
plain-language theorem explainer
For any rational orbit display, the verifier rational of its reciprocal equals the field inverse of its verifier rational. Cost and character authors cite this to move reciprocal identities between the internal PRC ratio layer and ordinary ℚ. The proof is a two-branch case split on whether the numerator balances zero, then simp with the nonzero reciprocal lemma.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). Writing $\mathrm{toRat}$ for the verifier map into $\mathbb{Q}$ and $\mathrm{recip}$ for the internal reciprocal on ratio orbits, one has $(\mathrm{recip}\, a).\mathrm{toRat} = (a.\mathrm{toRat})^{-1}$ in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus integer/rational layer, a ratio orbit is a display with signed-orbit numerator and nonzero distinction-nat denominator (K4.7). The verifier map toRat sends such a display to an ordinary rational; the internal reciprocal swaps and renormalizes numerator and denominator on δ-orbit positions.
Two signed orbits are balanced when their positive and negative orbit lengths match crosswise: $a.pos + b.neg = b.pos + a.neg$ (K4.9). The bridge lemma balanced_iff_toInt_eq states that this internal relation is equivalent to equality of verifier integers, so balance against the zero signed orbit detects a zero numerator without leaving the PRC vocabulary.
The local module builds rationals from orbits after the integer arithmetic of Orbit/OrbitArithmetic, keeping all relations choice-free and δ-position native before any continuum or cost layer is attached.
proof idea
Unfold the reciprocal. Case on whether the numerator is balanced with the zero signed orbit.
If balanced, apply balanced_iff_toInt_eq to obtain verifier-integer zero, then simp through toRat and the zero display: both sides become the zero rational's inverse convention as coded in toRat.
If not balanced, the numerator is nonzero in the verifier sense; discharge by simp with the already-proved nonzero reciprocal identity recipNonzero_toRat, which handles the genuine inversion case on ratio orbits.
why it matters
Reciprocal compatibility between the PRC ratio display and ℚ is the bridge every later reciprocal symmetry needs. Downstream, character_recip_toRat quotes it to get $(\chi(\mathrm{recip}, x)).\mathrm{toRat} = (\chi x).\mathrm{toRat}^{-1}$ for any PRC ratio character; calibrated_recip closes calibration under reciprocals the same way.
In the cost layer it appears inside the reciprocal fields of signedPowerNativeCost_base and signGaugeNativeCost_base_sans_two, and in realCharacterCandidate_recip / rationalTrace_recip when factoring real characters through rational traces. Without this identity, native-cost hypotheses and character rigidity cannot move inverse laws from ℚ back onto orbit displays.
It is pure foundation bookkeeping (K4 rational display), not a forcing-chain step, but it is load-bearing for any argument that treats J-cost or real characters as reciprocal on the rational skeleton before continuum extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.