intRel_trans
plain-language theorem explainer
Transitivity of the Grothendieck relation on pairs of logic-native naturals completes the equivalence axioms needed for the quotient that yields logic-native integers. Researchers constructing number systems from the forced naturals in the Recognition Science foundation cite this when verifying setoid instances. The proof unpacks the three pairs, transfers both relations and the goal to Nat equations via the embedding lemmas, derives the component additions, and closes with linear arithmetic.
Claim. Let $a,b,c,d,e,f$ be logic-native natural numbers. Define the relation $(a,b) R (c,d)$ to hold precisely when $a + d = c + b$. Then $R$ is transitive: if $(a,b) R (c,d)$ and $(c,d) R (e,f)$, then $(a,b) R (e,f)$.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, representing the smallest subset of positive reals closed under multiplication by the generator and containing 1. The function toNat reads off the iteration count, sending identity to 0 and step n to the successor of toNat n. The relation intRel on LogicNat × LogicNat is defined by (a,b) intRel (c,d) iff a + d = c + b; the pair (a,b) represents the formal difference a - b.
proof idea
The tactic proof begins with rintro to decompose the three pairs into components a,b,c,d,e,f. It rewrites the goal and the two hypotheses using eq_iff_toNat_eq together with toNat_add, moving everything to equations on Nat. Two auxiliary statements are obtained by applying congrArg toNat to the original relations and rewriting the additions again. The final omega tactic solves the resulting system of linear equations on natural numbers.
why it matters
This lemma supplies the missing transitivity axiom for the setoid instance on LogicNat × LogicNat, which defines LogicInt as the Grothendieck completion of LogicNat. It therefore sits at the base of the integer construction that feeds ArithmeticFromLogic and all subsequent arithmetic in the foundation. Within the Recognition Science chain it ensures the integers are available without external set-theoretic assumptions before the phi-ladder and mass formulas are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.