ratRel_trans
plain-language theorem explainer
Transitivity of the cross-multiplication relation on pre-rationals ensures equivalence classes are well-defined for the quotient construction. Researchers assembling the field of fractions from logic integers cite this step to obtain a setoid. The proof unpacks the pairs, builds an auxiliary equality via a calculation chain that rearranges products using associativity and commutativity, then cancels the nonzero middle denominator.
Claim. Let $(a,b)$, $(c,d)$, $(e,f)$ be pre-rationals with nonzero denominators. If $a d = c b$ and $c f = e d$, then $a f = e b$.
background
A pre-rational is a pair consisting of a logic integer numerator and a nonzero logic integer denominator. The relation identifies two such pairs precisely when their cross products are equal. This sits inside the module that constructs logic-native rationals as the quotient of pre-rationals by the relation, importing integer arithmetic from the preceding module on logic integers.
proof idea
The tactic unpacks the three pre-rationals together with the two hypotheses. A calc block rewrites $(a f) d$ into $(e b) d$ by successive applications of associativity and commutativity on the integer multiplication. Right cancellation with the nonzero middle denominator then concludes the goal.
why it matters
Transitivity supplies the final piece needed to instantiate the setoid on pre-rationals, which defines the type of logic rationals as the quotient. The construction appears directly before the field operations and the embedding of logic integers, forming the rational layer that later supports the real numbers in the Recognition Science foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.