inv_eq
plain-language theorem explainer
Multiplicative inverse on PRC rationals is definitionally the total reciprocal that swaps numerator and denominator (zero maps to zero). Anyone simplifying field-style arithmetic on the ratio-orbit quotient cites this simp fact. The proof is pure reflexivity: the Inv instance is wired directly to recip.
Claim. For every PRC rational $a$ (a nonzero-denominator ratio-orbit quotient class), the multiplicative inverse satisfies $a^{-1} = \mathrm{recip}(a)$, where $\mathrm{recip}$ is the total reciprocal on ratio orbits.
background
PRC rationals are the quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when their orbit-level numerators and denominators cross-multiply equally (K4.8). The type is Quot ratioOrbitSetoid.
The total reciprocal on ratio orbits (K4.12) swaps num and den when the numerator is nonzero, and sends the zero class to itself, matching the total convention on $\mathbb{Q}$. Upstream, the recognition framework also carries a real reciprocal involution $\iota(x)=x^{-1}$ on the positive reals, the dual-recognition symmetry the calculus is built on.
This module sits in Primitive Recognition Calculus and builds integer/rational arithmetic from signed orbits before real completion.
proof idea
One-line term proof by rfl. The Inv instance on PRC rationals is defined to be the total reciprocal, so the notation $a^{-1}$ and the function recip a are definitionally equal; no rewriting or case split is required.
why it matters
Registers the bridge between Lean’s inverse notation and the constructive reciprocal used throughout orbit arithmetic. With no recorded downstream dependents yet, it is infrastructure: simp can discharge Inv goals without unfolding the instance by hand.
It aligns the rational layer with the dual-recognition reciprocal symmetry ($ \iota(x)=x^{-1}$) that underpins J-cost identities of the form $J(x)+J(x^{-1})$ and the Recognition Composition Law. That symmetry is a prerequisite for the forcing chain’s J-uniqueness (T5) and the self-similar fixed point $\varphi$ (T6), even though this lemma itself is only a definitional glue fact at the rational stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.