neg
plain-language theorem explainer
Negation on LogicInt, the Grothendieck completion of LogicNat, is realized by swapping the pair of logic naturals that represents each integer. Algebraists building ring and group structures from the logic layer cite this to obtain additive inverses. The definition lifts the swap through the quotient via Quotient.lift, with well-definedness reduced to Nat arithmetic by toNat_add and eq_iff_toNat_eq followed by omega.
Claim. For an equivalence class $[(m,n)]$ in the quotient of logic naturals by the setoid, negation is defined by $-[(m,n)] = [(n,m)]$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, formed as the quotient of LogicNat × LogicNat by the equivalence relation intRel. LogicNat is the inductive type generated by the constructors identity (corresponding to zero) and step, whose toNat embedding recovers ordinary natural numbers. The upstream theorem eq_iff_toNat_eq transfers equations from LogicNat to Nat, while toNat_add shows that addition is preserved under this embedding.
proof idea
The definition applies Quotient.lift to the representative map that swaps the pair and reconstructs via mk. Well-definedness is proved by rintro on the relation h, applying sound to obtain the Nat equation b + c = d + a, rewriting both sides with toNat_add, and closing with omega after a congrArg step.
why it matters
This declaration equips LogicInt with the additive inverse required for the ring axioms in PhiRing and the group law in F2Power. It is used by canonicalPhiRingObj, PhiRingHom, and J_at_phi, placing it directly in the chain that builds the cost algebra and the phi-ladder from the logic foundation. The construction supports the eight-tick octave and D = 3 downstream in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.