instInv
plain-language theorem explainer
Equips PRC rationals with Lean's multiplicative inverse typeclass by packaging the total reciprocal map. Anyone assembling a field or group structure on the ratio-orbit quotient cites this instance. The construction is a one-line instance declaration: inverse is exactly recip.
Claim. The type of PRC rationals (quotient of ratio orbits by cross-multiplication equivalence, nonzero denominators) carries a multiplicative inverse operation $a \mapsto a^{-1}$ given by the total reciprocal, which sends the zero class to itself as on $\mathbb{Q}$.
background
PRC rationals are the K4.8 quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when orbit-level numerators and denominators cross-multiply equally, with nonzero denominators. They are the discrete rational layer of the Primitive Recognition Calculus before real completion.
The total reciprocal (K4.12) acts on ratio orbits by swapping numerator and denominator when the numerator is nonzero, and by sending the zero orbit to itself otherwise, matching the convention on $\mathbb{Q}$. A related dual-recognition reciprocal $\iota(x)=x^{-1}$ appears on the positive reals in the Universal Forcing layer; here the discrete version is the one being installed.
This module builds the integer and rational arithmetic scaffolding (addition, multiplication, negation, order) on signed orbits and their quotients so later continuity and completeness results can treat rationals as a concrete dense substructure.
proof idea
One-line instance: the Inv structure on PRC rationals is inhabited by the existing total reciprocal recip. No separate proof obligations; the typeclass field is definitionally that map. Adjacent simp lemmas in the same block unfold the other arithmetic operations (+, *, negation, subtraction) to their underlying constructors, but they are not part of this instance body.
why it matters
Field and division notation on PRC rationals require an Inv instance. Installing recip here lets downstream proofs write $a^{-1}$ and use Mathlib-style algebraic tactics on the ratio-orbit quotient without reintroducing the reciprocal by hand.
No downstream dependents are recorded yet on this edge list, so the instance is infrastructure rather than a cited lemma. It sits in the Foundation arithmetic stack that supports the recognition composition law and the later forcing chain (J-cost uniqueness, phi fixed point), where rational displays must invert cleanly before real and continuum layers are attached.
It does not itself force any physical constant; it only makes the discrete reciprocal available as a typeclass operation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.