toRat_mul
plain-language theorem explainer
The canonical map from the logic-constructed rationals to the standard rationals preserves multiplication. Researchers building the rational field inside the Recognition Science foundation cite this to confirm that ring operations transport faithfully. The proof applies double Quotient.inductionOn, reduces via the integer multiplication lemma, and finishes with field simplification after checking nonzero denominators.
Claim. Let $Q_L$ be the field of fractions of the logic integers and let $phi : Q_L to Q$ be the canonical map sending a representative pair to the ratio of recovered integers. Then $phi(a b) = phi(a) phi(b)$ for all $a, b in Q_L$.
background
LogicRat is the quotient of PreRat pairs by the setoid ratRel, constructed as the field of fractions of LogicInt. The map toRat sends a class mk a b hb to (toInt a : Q) / (toInt b : Q), where toInt recovers the underlying integer via the bijection established upstream. The local module constructs rationals directly from the integers derived in IntegersFromLogic, preparing the algebraic carrier for later Recognition Science structures such as the J-cost and phi-ladder.
proof idea
Double induction via Quotient.inductionOn on both arguments reduces to representatives p = mk a b hb and q = mk c d hd. After rcases and simp [toRat_mk, toInt_mul], push_cast is applied; the nonzero conditions hbq and hdq are obtained from eq_iff_toInt_eq together with toInt_zero; field_simp then closes the equality.
why it matters
The result is invoked by add_mul', mul_add', mul_assoc', mul_comm', mul_one' and one_mul' to transport the standard field identities onto LogicRat via eq_iff_toRat_eq. It supplies the multiplicative half of the ring-homomorphism property needed to identify LogicRat with Q, completing a foundational step before the J-uniqueness and eight-tick octave constructions in the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.