ofRat_mul
plain-language theorem explainer
The embedding of PRC rationals into the classical real boundary is multiplicative: the image of a product equals the product of the images. Anyone assembling the K4.14 real-completion boundary certificate cites this as the multiplication half of the ring homomorphism. The proof unfolds the embedding to the conservative rational display and rewrites by the already-proved multiplicativity of that display map.
Claim. For PRC rationals $a,b$, if $\iota$ embeds a PRC rational into the classical real boundary via its rational display, then $\iota(a\cdot b)=\iota(a)\cdot\iota(b)$.
background
In the Primitive Recognition Calculus, PRC rationals are nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. Each such class has a conservative rational display toRat landing in ordinary $\mathbb{Q}$.
The real boundary carrier is classical $\mathbb{R}$. The embedding ofRat sends a PRC rational to that boundary by casting its display: $\iota(q)=(q.\mathrm{toRat}:\mathbb{R})$. Upstream, multiplicativity of the display is already available: $(a\cdot b).\mathrm{toRat}=a.\mathrm{toRat}\cdot b.\mathrm{toRat}$.
This module packages the honest classical completion boundary (K4.14/A5): existence of the real boundary, a rational embedding, and preservation of addition and multiplication under that embedding.
proof idea
One short tactic proof. Unfold the embedding definition so both sides become casts of rational displays into $\mathbb{R}$. Rewrite the left-hand display of the product by the upstream lemma that the PRC-rational display preserves multiplication. Close by norm_num, which discharges the resulting equality of ordinary real multiplications of rationals.
why it matters
Feeds the parent certificate real_completion_boundary_certificate (K4.14), which packages that the classical real boundary exists and that the rational embedding preserves addition and multiplication. Without multiplicativity, the embedding would not be a ring homomorphism into the boundary, and the honest-tagging claim that the classical reals are available as a completion boundary would be incomplete.
In the broader foundation stack this is bookkeeping, not a forcing step: it does not touch T5–T8, the Recognition Composition Law, or the phi ladder. It simply closes the arithmetic interface so later continuum constructions can treat PRC rationals as a multiplicative substructure of the real boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.