neg
plain-language theorem explainer
Negation on the constructed rationals sends a representative a/b to (-a)/b. Algebraists building the phi-ring and recognition categories cite it to obtain additive inverses on the field of fractions of the logic integers. The definition lifts numerator negation through the quotient and verifies well-definedness by reduction to integer arithmetic via the toInt transfer map.
Claim. On the field of fractions of the logic integers, negation is defined by sending the class of the pair (a, b) with b nonzero to the class of (-a, b).
background
LogicRat is the quotient of PreRat (pairs of logic integers with nonzero second component) by the equivalence ratRel. LogicInt itself is the quotient of pairs of logic naturals under the relation a + d = c + b, with its own negation swapping components via the mk constructor. The upstream IntegersFromLogic module supplies the sound theorem (mk a b = mk c d when a + d = c + b) and the toInt recovery map together with eq_iff_toInt_eq, which transfers equations between the logic integers and ordinary Int.
proof idea
The definition applies Quotient.lift to the map that negates the numerator while preserving the denominator. Well-definedness is checked by assuming a * d = c * b, then showing (-a) * d = (-c) * b. The argument applies toInt to both sides, rewrites via toInt_mul and toInt_neg, and finishes with linarith.
why it matters
This supplies the additive inverse needed for the ring axioms on LogicRat. It is used to define negation on PhiInt and to verify the map_neg condition in PhiRingHom. Downstream it supports sub_eq_add in F2Power and the J_at_phi evaluation in the cost algebra. The step completes the passage from logic integers to rationals required for the phi-ladder and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.