intRel
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove reflexivity, symmetry or transitivity.
- Does not construct the quotient type LogicInt.
- Does not connect the relation to physical constants or spatial dimensions.
Lean usage
instance setoid : Setoid (LogicNat × LogicNat) := ⟨intRel, intRel_refl, intRel_symm, intRel_trans⟩formal statement (Lean)
42def intRel : (LogicNat × LogicNat) → (LogicNat × LogicNat) → Prop :=
proof body
Definition body.
43 fun p q => p.1 + q.2 = q.1 + p.2
44