mul
plain-language theorem explainer
The definition equips the quotient integers from logic with multiplication by lifting the bilinear rule on pairs of logic naturals. Algebraists building the ring inside the logic foundation cite it when assembling additive and multiplicative structure before moving to cost algebra. It proceeds via Quotient.lift₂ on the explicit pair formula together with a well-definedness check that reduces to a Nat polynomial identity solved by nlinarith after transfer via toNat.
Claim. Multiplication on the quotient integers is defined by lifting the operation on pairs: for representatives $(a,b)$ and $(c,d)$ of logic naturals, the product is the class of $(ac + bd, ad + bc)$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of pairs of logic naturals by the equivalence induced by addition. LogicNat is the inductive type generated by an identity element (zero-cost) and a step constructor that iterates the generator, mirroring the orbit under multiplication by the base element. Upstream results supply the recursive multiplication on LogicNat, the toNat map that extracts the underlying natural number, the recovery theorem toNat_add, and the transfer principle eq_iff_toNat_eq that equates equality in LogicNat with equality of the extracted naturals.
proof idea
The definition applies Quotient.lift₂ to the pair function that computes mk (p.1 * q.1 + p.2 * q.2) (p.1 * q.2 + p.2 * q.1). Well-definedness is shown by applying sound, rewriting the equality via eq_iff_toNat_eq, simplifying with toNat_add and toNat_mul, extracting Nat equalities from the hypotheses by congrArg, and closing the resulting polynomial identity with nlinarith using non-negativity facts.
why it matters
This multiplication supplies the ring operations on the integers constructed from logic, which downstream results in CostAlgebra and PhiRing rely upon to define shifted composition and to embed the golden ratio. It is used by J_at_phi to evaluate the J-cost at phi and by the RecognitionCategory constructions for PhiRingObj and PhiRingHom. The step completes the algebraic foundation before the phi-ladder derivations and the eight-tick octave structure in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.