mul
plain-language theorem explainer
Multiplication on the quotient field LogicRat of LogicInt is defined by lifting the componentwise product on PreRat pairs to respect the equivalence. Researchers building arithmetic from logical primitives would cite this to equip the rationals with ring operations before recovering the standard field. The definition uses Quotient.lift₂ together with the sound theorem and integer transfer to verify independence of representatives.
Claim. For classes $r,s$ in the quotient field of logic integers, with representatives $(a,b)$ and $(c,d)$ where $b,d$ are nonzero, define the product as the class of $(ac,bd)$.
background
LogicRat is the quotient of PreRat pairs by the setoid equivalence ratRel, which identifies fractions representing the same value. PreRat consists of pairs of logic integers with nonzero denominator; the mk constructor forms such a pair while enforcing the nonzero condition. This sits inside the module recovering rational arithmetic from logic, immediately after the integers are constructed as quotients of natural pairs.
proof idea
The definition applies Quotient.lift₂ to the map sending pairs to mk of the product numerators and denominators. Well-definedness is shown by applying sound after rewriting the cross-multiplication condition with eq_iff_toInt_eq and toInt_mul, then discharging the resulting integer identity by linear_combination on the two equivalence hypotheses.
why it matters
This supplies the multiplicative operation required for the rational field, which is used downstream in CostAlgebra for shifted composition values and in PhiRing for J_at_phi and the PhiInt structure. It completes the arithmetic layer that feeds the cost algebra and recognition category, directly supporting the J-cost definition and the phi-ladder constants in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.