mul_toRat
plain-language theorem explainer
Multiplication of rational orbits is compatible with the rational display: the display of a product equals the product of the displays. Cost and gauge-orbit authors cite this when moving native cost identities onto ℚ. The proof unfolds the orbit product and display, recovers integer and natural multiplication, clears nonzero denominators, and finishes by ring normalization.
Claim. For rational orbits $a,b$ (each an integer numerator over a nonzero orbit denominator), the rational display of the product equals the product of the displays: $(a\cdot b)_{\mathbb{Q}}=a_{\mathbb{Q}}\cdot b_{\mathbb{Q}}$.
background
In the Primitive Recognition Calculus integer/rational layer, a rational orbit is a display pair: a signed orbit numerator over a nonzero distinction-natural denominator. The map toRat sends such a pair to an ordinary rational by reading the signed integer and natural displays and forming their quotient.
Multiplication of rational orbits is defined componentwise on those internal displays (signed-orbit product in the numerator, distinction-natural product in the denominator), so the claim is that this structural product matches ordinary multiplication after display.
Upstream, toNat reads the iteration count of a logic natural, and the recovery theorem toNat_mul states that logic-natural multiplication agrees with Nat multiplication under that equivalence. The signed-orbit side contributes the matching integer-multiplication transport used in the rewrite.
proof idea
Term-mode proof by unfolding the orbit product and the rational display. Rewrite the numerator via signed-orbit integer multiplication transport and the denominator via distinction-natural multiplication recovery (toNat_mul). Record that both denominator casts to ℚ are nonzero (from the structure invariant). Apply field_simp to clear the quotient form, push_cast to align coercions, and ring_nf to finish the algebraic identity.
why it matters
This is the multiplicative half of the rational-orbit display homomorphism. Downstream cost work uses it constantly: cost_display rewrites the native doubled-trace cost into the halved-and-shifted rational trace by simp-ing through mul_toRat (with add and unit displays). The same lemma appears in zero-calibration and base hypotheses for signed-power and sign-gauge native costs, and in real-character factorization identities such as rationalTrace_dAlembert and doubledTrace_dAlembert_of_rcl.
In the Recognition stack this sits under the cost/J layer that eventually feeds T5 J-uniqueness and the RCL. Without display-homomorphism for products, gauge-orbit cost identities cannot move from orbit syntax to ordinary rationals where the analytic character work lives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.