setoid
plain-language theorem explainer
This instance equips pairs of logic-native naturals with the Grothendieck equivalence relation so that integers arise as the quotient. Researchers constructing arithmetic directly from the law of logic cite it when defining the type of logic-native integers. The proof is a one-line wrapper that bundles the relation with its reflexivity, symmetry, and transitivity theorems.
Claim. The setoid on pairs of logic-native natural numbers in which $(a,b)$ is equivalent to $(c,d)$ precisely when $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 subset of positive reals closed under the base multiplication and containing 1. The relation on pairs declares $(a,b)$ equivalent to $(c,d)$ exactly when $a + d = c + b$, which encodes the formal difference $a - b$ for the Grothendieck construction. This instance sits inside the IntegersFromLogic module, which builds the integers as the completion of LogicNat under addition and immediately precedes the definition of the quotient type of logic-native integers.
proof idea
One-line wrapper that supplies the relation together with the three theorems establishing reflexivity, symmetry, and transitivity.
why it matters
The setoid is the direct prerequisite for the quotient definition of logic-native integers, which in turn supports cancellation laws, the field of fractions, and all subsequent arithmetic used in the recognition framework. It completes the passage from logic-native naturals to signed quantities required for the forcing chain and for embedding physical quantities into the phi-ladder. Downstream results such as the multiplication cancellation theorem and the rational setoid instance depend on the quotient structure it induces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.