Grace/Cumulus/Rat/OrderedOperations.g17

Open in Workbench Download source

Imports

Density

Declarations

Source

1-- Order compatibility of rational operations2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Rat.OrderedOperations8import Density910-- The mainstream typed interface to the set-level transitivity certificate.11theorem rationalLess.transitive (x y z : Rational)12  requires xy : x < y13  requires yz : y < z14  shows x < z15proof16  have transitive := rationalLess.transitive_on17  exact transitive with x, y, z, xy, yz1819-- Adding the same displayed rational preserves strict order.  The quotient20-- calculation is isolated here so clients can use the ordered-group21-- law without exposing representatives.22-- No rational is below itself.23theorem rationalLess.irreflexive (x : Rational)24  shows ¬(x < x)25proof26  intro less27  have irreflexive := rationalLess.irreflexive_on28  exact irreflexive with x, less2930-- Two rationals compare one way, are equal, or compare the other way.31theorem rationalLess.trichotomy (x y : Rational)32  shows x < y ∨ x = y ∨ y < x33proof34  by_contra none35  have distinct : x ≠ y36    intro equal37    apply none38    right39    left40    exact equal41  have connected := rationalLess.connected_on42  have comparison := connected with x, y, distinct43  apply none44  cases comparison with xy | yx45  . left46    exact xy47  . right48    right49    exact yx5051theorem rationalLess.add_right_classes (a b m c d n e f k : Nat)52  requires mNonzero : m ≠ 053  requires nNonzero : n ≠ 054  requires kNonzero : k ≠ 055  requires less : relates(rationalLess,56    rationalClass(a, b, m), rationalClass(c, d, n))57  shows relates(rationalLess,58    rationalAddValue(rationalClass(a, b, m), rationalClass(e, f, k)),59    rationalAddValue(rationalClass(c, d, n), rationalClass(e, f, k)))60proof61  have crossLess := rationalLess.classes.forward with mNonzero, nNonzero, less62  have squareNatural := mul.closed at k, k with *63  have squareNonzero := mul.nonzero with kNonzero, kNonzero64  have leftNatural : Nat(n * a + m * d) by simp [mul.closed, add.closed]65  have rightNatural : Nat(m * c + n * b) by simp [mul.closed, add.closed]66  have scaled := Less.mul_left with squareNonzero, crossLess67  have commonNatural : Nat(((m * n) * k) * e + ((m * n) * k) * f) by simp [mul.closed, add.closed]68  have commonReflexive := LessEqual.reflexive with commonNatural69  have augmented := Less.add_LessEqual at70    (k * k) * (n * a + m * d), (k * k) * (m * c + n * b),71    ((m * n) * k) * e + ((m * n) * k) * f,72    ((m * n) * k) * e + ((m * n) * k) * f with73    *{2}, commonNatural, commonNatural, scaled, commonReflexive74  have leftShape : (k * k) * (n * a + m * d) + (((m * n) * k) * e + ((m * n) * k) * f) = (n * k) * (k * a + m * e) + (m * k) * (k * d + n * f)75    ring76  have rightShape : (k * k) * (m * c + n * b) + (((m * n) * k) * e + ((m * n) * k) * f) = (m * k) * (k * c + n * e) + (n * k) * (k * b + m * f)77    ring78  rw [leftShape, rightShape] at augmented79  have leftSum := rationalAddValue.classes at80    a, b, m, e, f, k with mNonzero, kNonzero81  have rightSum := rationalAddValue.classes at82    c, d, n, e, f, k with nNonzero, kNonzero83  rw [leftSum, rightSum]84  have mkNonzero := mul.nonzero with mNonzero, kNonzero85  have nkNonzero := mul.nonzero with nNonzero, kNonzero86  unfold rationalClassSum87  exact rationalLess.classes.backward with mkNonzero, nkNonzero, augmented8889-- Translation invariance stated at the public rational boundary.90theorem rationalLess.add_right (x y z : Rational)91  requires less : x < y92  shows x + z < y + z93proof94  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=95    Rational.coordinates at x with assumption96  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=97    Rational.coordinates at y with assumption98  obtain ⟨e, eNatural, f, fNatural, k, kNatural, kNonzero, zShape⟩ :=99    Rational.coordinates at z with assumption100  rw [xShape, yShape] at less101  rw [xShape, yShape, zShape, rationalAddValue.notation, rationalAddValue.notation]102  exact rationalLess.add_right_classes with mNonzero, nNonzero, kNonzero, less103104-- Commutativity turns right translation into the corresponding left law.105theorem rationalLess.add_left (x y z : Rational)106  requires less : x < y107  shows z + x < z + y108proof109  have translated := rationalLess.add_right at x, y, z with less110  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=111    Rational.coordinates at x with assumption112  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=113    Rational.coordinates at y with assumption114  obtain ⟨e, eNatural, f, fNatural, k, kNatural, kNonzero, zShape⟩ :=115    Rational.coordinates at z with assumption116  have xzCommutative := rationalClassSum.commutative at117    a, b, m, e, f, k with mNonzero, kNonzero118  have yzCommutative := rationalClassSum.commutative at119    c, d, n, e, f, k with nNonzero, kNonzero120  have xzLeft := rationalAddValue.classes at121    a, b, m, e, f, k with mNonzero, kNonzero122  have zxRight := rationalAddValue.classes at123    e, f, k, a, b, m with kNonzero, mNonzero124  have yzLeft := rationalAddValue.classes at125    c, d, n, e, f, k with nNonzero, kNonzero126  have zyRight := rationalAddValue.classes at127    e, f, k, c, d, n with kNonzero, nNonzero128  rw [xShape, yShape, zShape] at translated129  rw [xShape, yShape, zShape]130  rw [rationalAddValue.notation, rationalAddValue.notation] at translated131  rw [rationalAddValue.notation, rationalAddValue.notation]132  rw [xzLeft, yzLeft] at translated133  rw [zxRight, zyRight]134  rwa [xzCommutative, yzCommutative] at translated135136theorem rationalLess.of_add_right (x y z : Rational)137  requires translated : x + z < y + z138  shows x < y139proof140  have leftRational := rationalAddValue.rational at x, z with141    *{2}142  have rightRational := rationalAddValue.rational at y, z with143    *{2}144  have negativeZ := rationalNegValue.rational at z145  have shiftedBack := rationalLess.add_right with leftRational, rightRational, negativeZ, translated146  have leftCancel := rationalAddValue.add_sub_cancel_right at x, z with147    *{2}148  have rightCancel := rationalAddValue.add_sub_cancel_right at y, z with149    *{2}150  unfold rationalSubValue at leftCancel151  unfold rationalSubValue at rightCancel152  rwa [leftCancel, rightCancel] at shiftedBack153154-- The product of two positive rationals is positive.  At displayed155-- representatives, positivity says b<a and d<c; normalization isolates the156-- positive remainder (a-b)(c-d) without introducing integer subtraction.157theorem rationalLess.mul_positive (x y : Rational)158  requires positiveX : rationalZero < x159  requires positiveY : rationalZero < y160  shows rationalZero < x * y161proof162  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=163    Rational.coordinates at x with assumption164  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=165    Rational.coordinates at y with assumption166  have oneNonzero : 1 ≠ 0167    intro oneZero168    arith169  have displayedX := positiveX170  have displayedY := positiveY171  rw xShape at displayedX172  rw yShape at displayedY173  unfold rationalZero at displayedX174  unfold rationalZero at displayedY175  have bLessA : b < a176    have cross := rationalLess.classes.forward with oneNonzero, mNonzero, displayedX177    simpa [mul.left_zero, mul.right_zero, mul.left_unit,178      mul.right_unit, add.left_unit, add.right_unit] using cross179  have dLessC : d < c180    have cross := rationalLess.classes.forward with oneNonzero, nNonzero, displayedY181    simpa [mul.left_zero, mul.right_zero, mul.left_unit,182      mul.right_unit, add.left_unit, add.right_unit] using cross183  obtain ⟨k, kNatural, aShape⟩ := bLessA184  obtain ⟨l, lNatural, cShape⟩ := dLessC185  have succKNonzero : succ(k) ≠ 0186    intro succKZero187    have zeroNotSuccK := Naturals.disjoint.zero.succ at k188    apply zeroNotSuccK189    rw succKZero190    rfl191  have succLNonzero : succ(l) ≠ 0192    intro succLZero193    have zeroNotSuccL := Naturals.disjoint.zero.succ at l194    apply zeroNotSuccL195    rw succLZero196    rfl197  have remainderNonzero := mul.nonzero with succKNonzero, succLNonzero198  have positiveRemainder := Less.add_positive at199    a * d + b * c, succ(k) * succ(l) with200    remainderNonzero201  have productGap : a * d + b * c + succ(k) * succ(l) = a * c + b * d202    rw [← aShape, ← cShape]203    ring204  rw productGap at positiveRemainder205  rw [xShape, yShape, rationalMulValue.notation, rationalMulValue.classes]206  unfold rationalClassMul207  unfold rationalZero208  have mnNonzero := mul.nonzero with mNonzero, nNonzero209  apply rationalLess.classes.backward with oneNonzero, mnNonzero210  ring_nf211  exact positiveRemainder212213theorem rationalLess.sub_positive (x y : Rational)214  requires less : x < y215  shows rationalZero < y - x216proof217  have negX := rationalNegValue.rational at x218  have shifted := rationalLess.add_right at x, y, -x with219    *{2}, negX, less220  have inverse := rationalAddValue.neg_right at x221  rw inverse at shifted222  unfold rationalSubValue223  exact shifted224225-- Multiplication by a positive rational preserves strict order.  The proof is226-- the textbook difference argument z(y-x)>0, with distributivity supplying227-- z*y = z*x + z*(y-x).228theorem rationalLess.mul_left (x y z : Rational)229  requires positiveZ : rationalZero < z230  requires less : x < y231  shows z * x < z * y232proof233  have gapRational := rationalSubValue.rational at y, x with234    *{2}235  have positiveGap := rationalLess.sub_positive with less236  have positiveProduct := rationalLess.mul_positive with positiveZ, positiveGap237  have zxRational := rationalMulValue.rational at z, x with238    *{2}239  have productRational := rationalMulValue.rational at z, y - x with240    assumption, gapRational241  have shifted := rationalLess.add_left with242    rationalZero.rational, productRational, zxRational, positiveProduct243  have leftIdentity := rationalAddValue.zero_right with zxRational244  rw leftIdentity at shifted245  have gapCloses := rationalAddValue.add_sub_cancel_left at x, y with246    *{2}247  have decomposition : z * x + z * (y - x) = z * y248    have distributed := rationalMulValue.distributive_left at z, x, y - x with249      *{2}, gapRational250    rw gapCloses at distributed251    rw ← distributed252    rfl253  rwa decomposition at shifted254255theorem rationalLess.mul_right (x y z : Rational)256  requires positiveZ : rationalZero < z257  requires less : x < y258  shows x * z < y * z259proof260  have scaled := rationalLess.mul_left with positiveZ, less261  have leftCommutative := rationalMulValue.commutative at z, x with262    *{2}263  have rightCommutative := rationalMulValue.commutative at z, y with264    *{2}265  rwa [leftCommutative, rightCommutative] at scaled266267-- Cancellation by a positive rational.  Together with mul_left this says268-- that positive scaling is an order embedding.269theorem rationalLess.of_mul_left (x y z : Rational)270  requires positiveZ : rationalZero < z271  requires scaled : z * x < z * y272  shows x < y273proof274  have xDistinctY : x ≠ y275    intro equal276    rw equal at scaled277    have irreflexive := rationalLess.irreflexive_on278    exact irreflexive with z * y, scaled279  have connected := rationalLess.connected_on280  have comparison := connected with x, y, xDistinctY281  cases comparison with xLessY | yLessX282  . exact xLessY283  . have reverse := rationalLess.mul_left at y, x, z with284      *{3}, positiveZ, yLessX285    have cycle := rationalLess.transitive with scaled, reverse286    have irreflexive := rationalLess.irreflexive_on287    exfalso288    exact irreflexive with z * x, cycle289290theorem rationalLess.neg_reverse (x y : Rational)291  requires less : x < y292  shows -y < -x293proof294  have negX := rationalNegValue.rational at x295  have negY := rationalNegValue.rational at y296  have translated := rationalLess.add_right at x, y, -x with297    *{2}, negX, less298  have inverseX := rationalAddValue.neg_right at x299  rw inverseX at translated300  have sumRational := rationalAddValue.rational at y, -x with assumption, negX301  have shifted := rationalLess.add_left with rationalZero.rational, sumRational, negY, translated302  have leftIdentity := rationalAddValue.zero_right with negY303  rw leftIdentity at shifted304  have associative := rationalAddValue.associative at -y, y, -x with305    negY, assumption, negX306  rw ← associative at shifted307  have inverseY := rationalAddValue.neg_left at y308  rw inverseY at shifted309  have rightIdentity := rationalAddValue.zero_left with negX310  rwa rightIdentity at shifted311312-- A positive gap y-x has the expected sign, stated without exposing quotient313-- representatives.  This is the witness-selection lemma used by open real314-- cuts: if x < y, then x-y belongs to the rational cut at zero.315theorem rationalLess.sub_self_negative (x y : Rational)316  requires less : x < y317  shows x - y < rationalZero318proof319  have translated := rationalLess.add_right at x, y, -y with less320  have inverse := rationalAddValue.neg_right at y321  rw inverse at translated322  unfold rationalSubValue323  exact translated324325theorem rationalLess.sub_left (x y z : Rational)326  requires less : x < y + z327  shows x - y < z328proof329  have translated := rationalLess.add_right at x, y + z, -y with less330  have cancellation := rationalAddValue.sum_sub_left at y, z with331    *{2}332  unfold rationalSubValue at cancellation333  rw cancellation at translated334  unfold rationalSubValue335  exact translated336337theorem rationalLess.add_left_of_sub_left (x y z : Rational)338  requires less : x - y < z339  shows x < y + z340proof341  have translated := rationalLess.add_left at x - y, z, y with less342  have cancellation := rationalAddValue.add_sub_cancel_left at y, x with343    *{2}344  rwa cancellation at translated345346-- The rational arithmetic progression beginning at (a-b)/n with mesh 1/D.347-- It is kept as a quotient-level helper so the Archimedean proof can reason348-- about a finite grid without introducing a new coercion primitive.349def rationalGrid (a b n D k : Nat) : Set :=350  rationalClass(D * a + k * n, D * b, n * D)351352theorem rationalGrid.rational (a b n D k : Nat)353  requires nNonzero : n ≠ 0354  requires DNonzero : D ≠ 0355  shows Rational(rationalGrid(a, b, n, D, k))356proof357  unfold rationalGrid358  apply rationalClass.rational359  . exact mul.nonzero with nNonzero, DNonzero360361theorem rationalGrid.zero (a b n D : Nat)362  requires nNonzero : n ≠ 0363  requires DNonzero : D ≠ 0364  shows rationalGrid(a, b, n, D, 0) = rationalClass(a, b, n)365proof366  unfold rationalGrid367  apply rationalClass.eq368  . exact mul.nonzero with nNonzero, DNonzero369  . exact nNonzero370  . settle with mul.left_zero, mul.right_zero, add.right_unit, mul.associative371372theorem rationalGrid.successor (a b n D k : Nat)373  requires nNonzero : n ≠ 0374  requires DNonzero : D ≠ 0375  shows rationalGrid(a, b, n, D, succ(k)) =376    rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D))377proof378  have nDNonzero := mul.nonzero with nNonzero, DNonzero379  have gridComputed := rationalAddValue.classes at380    D * a + k * n, D * b, n * D, 1, 0, D with381    nDNonzero, DNonzero382  have stepEquality : rationalGrid(a, b, n, D, succ(k)) =383      rationalClassSum(D * a + k * n, D * b, n * D, 1, 0, D)384    unfold rationalGrid385    unfold rationalClassSum386    apply rationalClass.eq387    . exact nDNonzero388    . exact mul.nonzero with nDNonzero, DNonzero389    . simp with mul.right_zero, mul.left_zero, add.right_unit,390        mul.right_unit, mul.left_unit391      ring392  have computedReverse : rationalClassSum(393      D * a + k * n, D * b, n * D, 1, 0, D) =394      rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D))395    unfold rationalGrid396    simp397  calc398    rationalGrid(a, b, n, D, succ(k)) =399        rationalClassSum(D * a + k * n, D * b, n * D, 1, 0, D) := stepEquality400    _ = rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D)) := computedReverse401402theorem rationalGrid.natural_step (a b n D k : Nat)403  requires nNonzero : n ≠ 0404  requires DNonzero : D ≠ 0405  shows rationalGrid(a, b, n, D, D * k) =406    rationalAddValue(rationalClass(a, b, n), rationalClass(k, 0, 1))407proof408  have oneNonzero : 1 ≠ 0409    intro oneZero410    arith411  have sumComputed := rationalAddValue.classes at412    a, b, n, k, 0, 1 with nNonzero, oneNonzero413  rw sumComputed414  unfold rationalGrid415  unfold rationalClassSum416  apply rationalClass.eq417  . exact mul.nonzero with nNonzero, DNonzero418  . exact mul.nonzero with nNonzero, oneNonzero419  . ring420421-- Every rational lies below a displayed natural number.  The witness is422-- canonical: for (a-b)/m we may take a+1.  This is the first423-- Archimedean boundary lemma; clients need not inspect representatives.424theorem Rational.below_natural (x : Rational)425  shows ∃ n, Nat(n) ∧426    x < rationalClass(n, 0, 1)427proof428  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=429    Rational.coordinates with assumption430  witness succ(a)431  rw xShape432  have oneNonzero : 1 ≠ 0433    intro oneZero434    arith435  have cross : Less(a, add(mul(m, succ(a)), b))436    have shape := natural.zero_or_successor with mNatural437    cases shape with zero | successor438    . exfalso439      apply mNonzero440      exact zero441    . obtain ⟨j, jNatural, mShape⟩ := successor442      rw mShape443      have successorNatural := Naturals.constructor.succ with aNatural444      have productStep := mul.succ_left with jNatural, successorNatural445      rw productStep446      have jProductNatural : Nat(mul(j, succ(a))) by typecheck447      have aLessSuccessor : a < succ(a)448        apply Less.of_membership449        . exact membership.self_successor with aNatural450      have productNonnegative := Grace.Core.Nat.Order.LessEqual.zero with jProductNatural451      have first := Less.add_LessEqual with452        aNatural, successorNatural, Naturals.constructor.zero, jProductNatural, aLessSuccessor, productNonnegative453      have aZero := add.right_unit with aNatural454      rw aZero at first455      have bNonnegative := Grace.Core.Nat.Order.LessEqual.zero with bNatural456      have sumNatural : Nat(add(succ(a), mul(j, succ(a)))) by typecheck457      have final := Less.add_LessEqual with458        aNatural, sumNatural, Naturals.constructor.zero, bNatural, first, bNonnegative459      rwa aZero at final460  have classLaw := rationalLess.classes at461    a, b, m, succ(a), 0, 1 with mNonzero, oneNonzero462  have leftShape : add(mul(1, a), mul(m, 0)) = a by ring463  have rightShape : add(mul(m, succ(a)), mul(1, b)) =464      add(mul(m, succ(a)), b)465    ring466  rw [leftShape, rightShape] at classLaw467  exact classLaw.backward with cross468469-- The symmetric half of rational unboundedness: every rational lies above a470-- negative displayed natural.  Negation transports the preceding witness,471-- so no second representative calculation is needed.472theorem Rational.above_negative_natural (x : Rational)473  shows ∃ n, Nat(n) ∧474    rationalClass(0, n, 1) < x475proof476  have negativeRational := rationalNegValue.rational at x477  obtain ⟨n, nNatural, below⟩ := Rational.below_natural with negativeRational478  witness n479  have oneNatural := Naturals.constructor.succ with Naturals.constructor.zero480  have oneNonzero : 1 ≠ 0481    intro oneZero482    arith483  have naturalRational := rationalClass.rational with484    nNatural, Naturals.constructor.zero, oneNatural, oneNonzero485  have reversed := rationalLess.neg_reverse with below486  have involutive := rationalNegValue.involutive at x487  rw [involutive, rationalNegValue.notation] at reversed488  have negativeClass := rationalNegValue.classes with489    nNatural, Naturals.constructor.zero, oneNatural, oneNonzero490  rw negativeClass at reversed491  unfold rationalClassNeg at reversed492  exact reversed493494theorem rationalLess.natural_successor (n : Nat)495  shows relates(rationalLess,496    rationalClass(n, 0, 1), rationalClass(succ(n), 0, 1))497proof498  have oneNonzero : 1 ≠ 0499    intro oneZero500    arith501  apply rationalLess.classes.backward with oneNonzero, oneNonzero502  have succNatural := Naturals.constructor.succ at n503  have nUnit := mul.left_unit at n504  have zeroUnit := mul.left_unit with Naturals.constructor.zero505  have succUnit := mul.left_unit with succNatural506  have nZero := add.right_unit at n507  have succAddZero := add.right_unit with succNatural508  rw [nUnit, zeroUnit, succUnit, nZero, succAddZero]509  apply Less.of_membership510  . exact membership.self_successor at n511512theorem rationalLess.positive_natural_successor (n : Nat)513  shows relates(rationalLess, rationalZero, rationalClass(succ(n), 0, 1))514proof515  have oneNonzero : 1 ≠ 0516    intro oneZero517    arith518  unfold rationalZero519  apply rationalLess.classes.backward with oneNonzero, oneNonzero520  have succNatural := Naturals.constructor.succ at n521  have zeroUnit := mul.left_unit with Naturals.constructor.zero522  have succUnit := mul.left_unit with succNatural523  have zeroZero := add.right_unit with Naturals.constructor.zero524  have succAddZero := add.right_unit with succNatural525  rw [zeroUnit, succUnit, zeroZero, succAddZero]526  have succNonzero : succ(n) ≠ 0527    intro succZero528    have zeroNotSucc := Naturals.disjoint.zero.succ at n529    apply zeroNotSucc530    rw succZero531    rfl532  have positive := Less.add_positive at 0, succ(n) with succNonzero533  simpa [add.left_unit] using positive534535-- Every positive rational dominates a positive unit fraction.  This is the536-- mesh-selection form of the Archimedean property used for finite rational537-- grids; clients never need to inspect the chosen denominator.538theorem rationalZero.lt_one539  shows rationalZero < rationalOne540proof541  have step := rationalLess.positive_natural_successor at 0 with *542  unfold rationalOne543  exact step544545theorem rationalLess.exists_positive_unit_fraction (x : Rational)546  requires positive : rationalZero < x547  shows ∃ D, Nat(D) ∧ D ≠ 0 ∧548    rationalZero < rationalClass(1, 0, D) ∧549    rationalClass(1, 0, D) < x550proof551  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=552    Rational.coordinates with assumption553  have oneNatural := Naturals.constructor.succ with Naturals.constructor.zero554  have oneNonzero : 1 ≠ 0555    intro oneZero556    arith557  have displayedPositive := positive558  rw xShape at displayedPositive559  unfold rationalZero at displayedPositive560  have numeratorPositive := rationalLess.classes.forward with oneNonzero, mNonzero, displayedPositive561  have bLessA : b < a562    simpa [mul.left_zero, mul.right_zero, mul.left_unit,563      mul.right_unit, add.left_unit, add.right_unit] using numeratorPositive564  witness 2 * m565  have twoNonzero : 2 ≠ 0566    intro twoZero567    arith568  have denominatorNonzero := mul.nonzero with twoNonzero, mNonzero569  constructor570  . exact denominatorNonzero571  constructor572  . unfold rationalZero573    apply rationalLess.classes.backward with oneNonzero, denominatorNonzero574    have zeroLessOne : 0 < 1575      apply Less.of_membership576      . exact membership.self_successor with Naturals.constructor.zero577    ring_nf578    exact zeroLessOne579  . rw xShape580    apply rationalLess.classes.backward with denominatorNonzero, mNonzero581    have oneLessTwo : 1 < 2582      apply Less.of_membership583      . exact membership.self_successor with oneNatural584    have scaled := Less.mul_left with mNonzero, oneLessTwo585    have unit : m * 1 = m by ring586    have twoMComm : m * 2 = 2 * m by ring587    rw [unit, twoMComm] at scaled588    have mLessTwoM := scaled589    have productNatural : Nat((2 * m) * b) by typecheck590    have productReflexive := LessEqual.reflexive with productNatural591    have lower := Less.add_LessEqual with mLessTwoM, productReflexive592    have succBLeA := bLessA593    have upper := LessEqual.mul_left at succ(b), a, 2 * m with594      succBLeA595    have lowerShape : m + (2 * m) * b = m * 1 + (2 * m) * b by ring596    have middleShape : (2 * m) + (2 * m) * b = (2 * m) * succ(b) by ring597    have upperShape : (2 * m) * a = (2 * m) * a + m * 0 by ring598    rw [lowerShape, middleShape] at lower599    rw upperShape at upper600    exact Less.transitive_LessEqual with lower, upper601602-- Given positive rationals a and g, choose a positive rational delta below603-- one whose product with a is smaller than g.  This is the reusable604-- Archimedean approximation step behind multiplication of open real cuts.605theorem rationalLess.exists_small_positive_multiplier (a g : Rational)606  requires positiveA : rationalZero < a607  requires positiveG : rationalZero < g608  shows ∃ delta ∈ ℚ,609    rationalZero < delta ∧ delta < rationalOne ∧ a * delta < g610proof611  obtain ⟨D, dNatural, dNonzero, unitPositive, unitBelowG⟩ := rationalLess.exists_positive_unit_fraction with612    positiveG613  obtain ⟨N, nNatural, aBelowN⟩ :=614    Rational.below_natural at a with assumption615  have oneNatural : Nat(1) by typecheck616  have oneNonzero : 1 ≠ 0617    intro oneZero618    arith619  have twoNonzero : 2 ≠ 0620    intro twoZero621    arith622  have nNonzero : N ≠ 0623    intro nZero624    have aBelowZero := aBelowN625    rw nZero at aBelowZero626    have zeroShape : rationalClass(0, 0, 1) = rationalZero627      unfold rationalZero628      rfl629    rw zeroShape at aBelowZero630    have cycle := rationalLess.transitive with positiveA, aBelowZero631    have impossible := rationalLess.irreflexive_on632    exact impossible with rationalZero, cycle633  have dnNonzero := mul.nonzero with dNonzero, nNonzero634  have eNonzero := mul.nonzero with twoNonzero, dnNonzero635  have deltaRational := rationalClass.rational at 1, 0, 2 * (D * N) with636    eNonzero637  have naturalRational := rationalClass.rational at N, 0, 1 with638    oneNonzero639  have deltaPositive : rationalZero < rationalClass(1, 0, 2 * (D * N))640    unfold rationalZero641    apply rationalLess.classes.backward with oneNonzero, eNonzero642    have zeroLessOne : 0 < 1643      apply Less.of_membership644      . exact membership.self_successor at 0 with Naturals.constructor.zero645    ring_nf646    exact zeroLessOne647  have oneLessTwo : 1 < 2648    apply Less.of_membership649    . exact membership.self_successor at 1 with oneNatural650  have dnPositive := Less.add_positive at 0, D * N with dnNonzero651  have oneLeDN : 1 ≤ D * N652    unfold Less at dnPositive653    simpa [add.left_unit] using dnPositive654  have dnLessE := Less.mul_left with dnNonzero, oneLessTwo655  have eShape : (D * N) * 2 = 2 * (D * N) by ring656  rw eShape at dnLessE657  simp [mul.right_unit] at dnLessE658  have oneLessE : 1 < 2 * (D * N) by exact LessEqual.transitive_Less with oneLeDN, dnLessE659  have deltaBelowOne : rationalClass(1, 0, 2 * (D * N)) < rationalOne660    unfold rationalOne661    apply rationalLess.classes.backward with eNonzero, oneNonzero662    ring_nf663    ring_nf at oneLessE664    exact oneLessE665  have scaled := rationalLess.mul_right with deltaPositive, aBelowN666  have naturalTimesDelta : rationalClass(N, 0, 1) *667      rationalClass(1, 0, 2 * (D * N)) = rationalClass(1, 0, 2 * D)668    rw [rationalMulValue.notation, rationalMulValue.classes]669    unfold rationalClassMul670    apply rationalClass.eq671    . exact mul.nonzero at 1, 2 * (D * N) with oneNonzero, eNonzero672    . exact mul.nonzero at 2, D with twoNonzero, dNonzero673    . ring674  rw naturalTimesDelta at scaled675  have dLessTwoD := Less.mul_left with dNonzero, oneLessTwo676  ring_nf at dLessTwoD677  have twoDNonzero := mul.nonzero with twoNonzero, dNonzero678  have halfUnitRational := rationalClass.rational at 1, 0, 2 * D with679    twoDNonzero680  have unitRational := rationalClass.rational at 1, 0, D with dNonzero681  have halfUnitBelowUnit : rationalClass(1, 0, 2 * D) < rationalClass(1, 0, D)682    apply rationalLess.classes.backward with twoDNonzero, dNonzero683    ring_nf684    exact dLessTwoD685  have productBelowG : a * rationalClass(1, 0, 2 * (D * N)) < g686    calc687      a * rationalClass(1, 0, 2 * (D * N)) < rationalClass(1, 0, 2 * D) := scaled688      _ < rationalClass(1, 0, D) := halfUnitBelowUnit689      _ < g := unitBelowG690  witness rationalClass(1, 0, 2 * (D * N))691  constructor692    exact deltaRational693  . refine ⟨deltaPositive, deltaBelowOne, productBelowG⟩694695-- If q < a with a positive, a multiplier can be chosen strictly between zero696-- and one while keeping q below the scaled value.  Written this way, clients697-- of open cuts can use the lemma without inspecting its Archimedean witness.698theorem rationalLess.exists_scale_below_one (q a : Rational)699  requires positiveA : rationalZero < a700  requires qLessA : q < a701  shows ∃ b ∈ ℚ,702    rationalZero < b ∧ b < rationalOne ∧ q < a * b703proof704  have gapRational := rationalSubValue.rational at a, q with705    *{2}706  have gapPositive := rationalLess.sub_positive with qLessA707  obtain ⟨delta, deltaInQ, deltaPositive, deltaBelowOne, productSmall⟩ :=708    rationalLess.exists_small_positive_multiplier at a, a - q with709      assumption, gapRational, positiveA, gapPositive710  have deltaRational : Rational(delta) by typecheck711  have oneRational := rationalOne.rational712  have bRational := rationalSubValue.rational with oneRational, deltaRational713  have bPositive := rationalLess.sub_positive with deltaBelowOne714  have translatedDelta := rationalLess.add_right with715    rationalZero.rational, deltaRational, bRational, deltaPositive716  have zeroAtB := rationalAddValue.zero_left with bRational717  have deltaCancel := rationalAddValue.add_sub_cancel_left with deltaRational, oneRational718  rw [zeroAtB, deltaCancel] at translatedDelta719  have bBelowOne : rationalOne - delta < rationalOne by exact translatedDelta720  have productRational := rationalMulValue.rational at a, delta with721    assumption, deltaRational722  have shifted := rationalLess.add_left at723    a * delta, a - q, q with724      productRational, gapRational, assumption, productSmall725  have gapCloses := rationalAddValue.add_sub_cancel_left at q, a with726    *{2}727  rw gapCloses at shifted728  have sumRational := rationalAddValue.rational at q, a * delta with729    assumption, productRational730  have negProductRational := rationalNegValue.rational with productRational731  have shiftedBack := rationalLess.add_right at732    q + a * delta, a, -(a * delta) with733      sumRational, assumption, negProductRational, shifted734  have leftCancel := rationalAddValue.add_sub_cancel_right at q, a * delta with735    assumption, productRational736  unfold rationalSubValue at leftCancel737  rw leftCancel at shiftedBack738  have productShape : a * (rationalOne - delta) = a - a * delta739    unfold rationalSubValue740    have distributed := rationalMulValue.distributive_left at741      a, rationalOne, -delta with742        assumption, oneRational,743        rationalNegValue.rational at delta with deltaRational744    have oneProduct := rationalMulValue.one_right at a745    have negProduct := rationalMulValue.neg_right at a, delta with746      assumption, deltaRational747    rwa [oneProduct, negProduct] at distributed748  have shiftedBackSub : q < a - a * delta749    unfold rationalSubValue750    exact shiftedBack751  rw ← productShape at shiftedBackSub752  witness rationalOne - delta753  constructor754    exact bRational755  . refine ⟨bPositive, bBelowOne, shiftedBackSub⟩756