intRel
plain-language theorem explainer
The definition supplies the Grothendieck equivalence on pairs of LogicNat, relating (a, b) to (c, d) exactly when a + d = c + b, so that each pair stands for the formal difference a - b. Researchers building the integers from the logic-forced naturals cite this relation as the kernel of the completion. It is realized by a direct functional definition that checks the swapped-addition equality.
Claim. The binary relation $(a, b) ∼ (c, d)$ on pairs of logic-native naturals holds if and only if $a + d = c + b$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative unit) and step (one further iteration of the generator), forming the smallest orbit closed under multiplication by the self-similar fixed point. The present definition sits inside the module that completes these naturals to integers via the Grothendieck construction. The upstream LogicNat supplies the base type whose pairs are quotiented here.
proof idea
The definition is a one-line functional wrapper that returns the proposition p.1 + q.2 = q.1 + p.2 for any input pairs p and q.
why it matters
intRel is the kernel used to install the Setoid instance on LogicNat × LogicNat, which then defines LogicInt as the quotient. It therefore supplies the missing step from logic-native naturals to integers inside the foundation, enabling all subsequent integer arithmetic. The construction mirrors the standard Grothendieck group completion and sits downstream of the forcing chain that derives the naturals from the Law of Logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.