Lemma·L48
The integer order is well defined on representatives
Comparing representative cross-sums gives the same answer no matter which representatives are chosen.
Let
with
and
(∼). Then
In words
If two pairs each represent the same integer as another pair, then a + d is at most c + b exactly when a' + d' is at most c' + b'.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1The hypotheses say (i) and (ii). Rearranging the four terms by commutativity/associativity and substituting first (i), then (ii) in the commuted form (substitutivity): call this identity (E): .
- 2Forward direction. Suppose ; by the gap fact, for some . Substituting into (E): using commutativity/associativity to move to the front on the right. Cancellation strips from both sides: so by the gap fact, .
- 3Reverse direction. Suppose ; by the gap fact, for some . Substituting into (E): Rearranging the left side with commutativity/associativity to move to the front: Cancellation strips from both sides: , so by the gap fact, .
∎