recip_mk
plain-language theorem explainer
Reciprocal commutes with the embedding of a rational orbit: taking recip after mk equals mk after RatioOrbit.recip. Anyone simplifying arithmetic on embedded ratio orbits cites this simp lemma. The proof is pure definitional equality (rfl).
Claim. For every rational orbit $a$ (integer numerator over a nonzero orbit denominator), the total reciprocal of its embedding equals the embedding of the total reciprocal of $a$. Zero is sent to zero, matching the convention on $\mathbb{Q}$.
background
In the primitive recognition calculus, a rational orbit (K4.7) packages a signed orbit numerator with a nonzero distinction-nat denominator. The total reciprocal on such orbits (K4.12) mirrors $\mathbb{Q}$: if the numerator is balanced with zero the result is zero; otherwise one applies the nonzero reciprocal constructor.
The ambient dual-recognition symmetry is the involution $\iota(x)=x^{-1}$ on the positive reals, the generator of reciprocal structure in the universal forcing layer. Here that symmetry is realized discretely on ratio orbits and then pushed through the embedding mk into the integer-rational display.
The local module builds integer and rational arithmetic on orbit data (imports Orbit and OrbitArithmetic), so commuting diagrams between orbit-level operations and their embedded forms are the natural simp infrastructure.
proof idea
One-line definitional proof: rfl. By construction the outer reciprocal on an embedded ratio orbit is exactly the embedding of RatioOrbit.recip, so the two sides are definitionally equal and no rewriting or case split is required.
why it matters
Closes the reciprocal half of the embedding interface for rational orbits inside the primitive recognition calculus. That interface lets later layers treat ratio-orbit arithmetic as if it were ordinary rational arithmetic while staying native to distinction/orbit data.
Framework-wise it is the discrete shadow of the dual-recognition involution $\iota(x)=x^{-1}$ from ReciprocalGenerator, which underpins the Recognition Composition Law and the J-cost uniqueness step (T5) in the forcing chain. No downstream theorems are recorded yet; the lemma is infrastructure for simp-driven rational identities on the orbit ladder rather than a named paper proposition.
It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only keeps reciprocal structure coherent at the rational-orbit layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.