ofRat_inv
plain-language theorem explainer
The embedding of PRC rationals into the real boundary intertwines inversion: the image of an inverse is the inverse of the image. Anyone simplifying field identities on the K4.14 real boundary cites this as a simp rule. The proof unfolds the embedding to Lean's rationals-to-reals cast, rewrites by the PRC-level inverse law, and closes by numeric normalization.
Claim. For every PRC rational $a$, the real-boundary embedding satisfies $\iota(a^{-1}) = \iota(a)^{-1}$, where $\iota$ sends a PRC rational to the real obtained from its conservative rational display.
background
In the Primitive Recognition Calculus, PRC rationals are nonzero-denominator ratio-orbit quotient classes (K4.8), identified by cross-multiplication. Each such class has a conservative display toRat into ordinary $\mathbb{Q}$.
The real boundary (K4.14/A5) is the completion carrier built so that rationals sit inside Lean's reals. The embedding ofRat is the composite of that display with the standard cast $\mathbb{Q}\to\mathbb{R}$: it is the constant rational point viewed on the boundary.
Upstream, toRat_inv' already records that inversion on PRC rationals matches inversion after display: $(a^{-1}).\mathrm{toRat}=(a.\mathrm{toRat})^{-1}$. The present lemma lifts that identity through the boundary embedding.
proof idea
Unfold the embedding definition so both sides become casts of ordinary rationals into $\mathbb{R}$. Rewrite the left-hand display of the inverse by the PRC-level law toRat_inv', which replaces $(a^{-1}).\mathrm{toRat}$ by $(a.\mathrm{toRat})^{-1}$. A final norm_num discharges the remaining equality of real inverses under the standard rational cast. No Cauchy or completeness machinery is touched.
why it matters
K4.14 equips the real boundary with Lean's complete-space structure and needs the rational embedding to be a field homomorphism on the nose. Sibling lemmas already cover addition, multiplication, and negation; this closes inversion, so the full field operations on PRC rationals transport to the boundary by simp.
Downstream use is presently empty in the graph, but the lemma is the missing inverse half of the ofRat_* simp suite that any later real-boundary algebra (completeness certificates, null-distance quotients, or strength comparisons) will fire automatically. In the broader forcing chain it is pure foundation scaffolding: it does not force $\phi$, the eight-tick octave, or $D=3$, but it keeps the rational spine of the real completion algebraically honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.