mul_mk
plain-language theorem explainer
Multiplication of rational orbits obtained by embedding signed orbits equals the embedding of the signed-orbit product. Anyone rewriting RatioOrbit arithmetic under simp will hit this lemma. The proof is pure reflexivity: both sides are definitionally the same constructor application.
Claim. For signed orbits $a$ and $b$, if $\iota$ embeds a signed orbit as a rational orbit, then $\mathrm{mul}(\iota(a),\iota(b))=\iota(a\cdot_{\mathrm{SO}} b)$, where $\cdot_{\mathrm{SO}}$ is signed-orbit multiplication.
background
In the primitive recognition calculus, integers are displayed as signed orbit differences. A SignedOrbit is a pair of distinction naturals (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$ (K4.6).
Rationals are then displayed as RatioOrbit: a signed numerator over a nonzero distinction-natural denominator (K4.7). The constructor mk embeds a signed orbit as a rational orbit (unit denominator). Multiplication is defined on both layers: SignedOrbit.mul on differences, and mul on rational orbits.
This module sits under Foundation.PrimitiveRecognitionCalculus and builds integer/rational arithmetic on orbit displays rather than on bare $\mathbb{Z}$ or $\mathbb{Q}$, so that later cost and ladder constructions stay native to recognition data.
proof idea
One-line rfl proof. After unfolding mul and mk, both sides reduce to the same RatioOrbit constructor term built from SignedOrbit.mul a b and the unit denominator, so definitional equality closes the goal. Marked @[simp] for automatic rewriting.
why it matters
Keeps the integer-to-rational embedding a monoid homomorphism at the display layer: products computed before or after embedding agree. That is bookkeeping for K4.6–K4.7 orbit arithmetic, which underpins later PRC cost uniqueness and ladder constructions in the foundation stack.
No downstream theorems currently list this lemma as a direct dependency in the graph; its role is simp infrastructure so RatioOrbit goals do not stall on trivial mk/mul commutation. It does not itself touch T5–T8 forcing, the RCL, or physical constants; it only stabilizes the integer/rational substrate those layers will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.