recip
plain-language theorem explainer
Total reciprocal on ratio-orbit displays: swap numerator and denominator when the numerator is nonzero, and send the zero class to zero, matching ordinary rationals. Cost and character packages cite it for reciprocal invariance of traces and for RCL packs without a two-point anchor. The definition is a case split on whether the signed numerator balances against zero, then either the zero orbit or the nonzero reciprocal constructor.
Claim. Define a total map $\mathrm{recip}$ on ratio-orbit displays (signed-orbit numerator over a nonzero distinction-nat denominator) by sending a display to the zero ratio orbit when its numerator is balanced against the zero signed orbit, and otherwise to the nonzero reciprocal of that display.
background
In the Primitive Recognition Calculus integer/rational layer, a ratio-orbit display packages a signed orbit (PRC integer) as numerator with a nonzero distinction-nat denominator. Two signed orbits are balanced when their positive and negative orbit lengths satisfy $a_{+} + b_{-} = b_{+} + a_{-}$; balancing against zero is the internal test that the numerator represents the zero integer.
PRC rationals are the quotient of these displays by cross-multiplication equivalence. The reciprocal is defined first on displays so that it is total (including zero), paralleling $0^{-1} := 0$ as a total convention on $\mathbb{Q}$ before quotienting. Upstream, the balanced relation and the nonzero-reciprocal constructor supply the two branches; the soundness of integer identification via additive cross-equality underwrites that the zero test is well-defined on orbit data.
proof idea
Definition by cases, not a theorem proof. Decide whether the numerator of $a$ is balanced against the zero signed orbit. If yes, return the zero ratio orbit. If no, apply the nonzero reciprocal constructor on $a$ with that non-balance witness. No further algebraic rewriting occurs at this layer.
why it matters
K4.12 supplies the total reciprocal used throughout cost and continuum character work. Downstream, BaseSansTwo requires that a native cost map $F$ satisfy cross-equality of $F(q)$ with $F(\mathrm{recip}, q)$, the reciprocal clause of the RCL pack without the two-point anchor. Trace and real-character lemmas then get $\mathrm{traceDisplay}(F,\mathrm{recip}, q)=\mathrm{traceDisplay}(F,q)$, rational-trace invariance under $x\mapsto x^{-1}$, and $\chi(\mathrm{recip}, x)=\chi(x)^{-1}$ for candidate characters.
On the continuum side, calibration is closed under reciprocals, feeding character-trace rigidity. Within the forcing chain this is bookkeeping for the Recognition Composition Law side of J-cost uniqueness (T5) and real-character factorization, not a new physical constant, but without a total reciprocal the reciprocal axioms of native cost cannot even be stated on displays that may be zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.