Grace/Cumulus/Rat/Density.g17

Open in Workbench Download source

Imports

Operations

Declarations

• rationalLess.exists_below theorem derivation
• rationalLess.dense theorem derivation

Source

1-- Density and unboundedness of the rational order2-- 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.Density8import Operations910-- Every rational has a strictly smaller rational.  On a displayed fraction11-- (a-b)/m, increasing the negative numerator by one gives (a-(b+1))/m.12theorem rationalLess.exists_below (q : Set)13  requires qRational : Rational(q)14  shows ∃ p ∈ ℚ, p < q15proof16  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates with qRational17  have bSuccNat : Nat(succ(b)) by exact Naturals.constructor.succ at b with bNat18  have bLess : b < succ(b)19    apply Less.of_membership20    . exact membership.self_successor at b with bNat21  have scaled := Less.mul_left with mNonzero, bLess22  have maNat : Nat(m * a) by typecheck23  have leftReflexive := LessEqual.reflexive with maNat24  have cross := LessEqual.add_Less with leftReflexive, scaled25  have belowRational := rationalClass.rational with aNat, bSuccNat, mNat, mNonzero26  have crossNormalized : m * a + m * b < m * a + m * succ(b)27    ring_nf at cross28    ring_nf29    exact cross30  have below := rationalLess.of_representatives with mNonzero, mNonzero, crossNormalized31  witness rationalClass(a, succ(b), m)32  constructor33    exact belowRational34  . unfold rationalClass at qShape35    rw qShape36    unfold rationalClass37    exact below3839-- Between two displayed fractions we use their midpoint.  The proof40-- below exposes the two positive scaling certificates: density41-- is arithmetic, while descent to quotient classes is handled by the existing42-- rational-order boundary theorem.43theorem rationalLess.dense (q r : Set)44  requires qRational : Rational(q)45  requires rRational : Rational(r)46  requires less : relates(rationalLess, q, r)47  shows ∃ s ∈ ℚ, q < s ∧ s < r48proof49  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates with qRational50  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, rShape⟩ := Rational.coordinates with rRational51  have displayedLess : relates(52      rationalLess, rationalClass(a, b, m), rationalClass(c, d, n))53    simpa [qShape, rShape] using less54  have crossLess := rationalLess.classes.forward with mNonzero, nNonzero, displayedLess5556  have twoNonzero : 2 ≠ 057    intro twoZero58    arith59  have mnNonzero := mul.nonzero with mNonzero, nNonzero60  have mnNat : Nat(m * n) by typecheck61  have denominatorShape := mul.two_left with mnNat62  have denominatorNonzero := mul.nonzero with twoNonzero, mnNonzero63  have midpointRational := rationalClass.rational at64    n * a + m * c, n * b + m * d,65    2 * (m * n) with denominatorNonzero6667  have scaledLeft := Less.mul_left with mNonzero, crossLess68  have leftCommonNat : Nat((m * n) * a + (m * n) * b) by typecheck69  have leftCommonReflexive := LessEqual.reflexive with leftCommonNat70  have augmentedLeft := Less.add_LessEqual with scaledLeft, leftCommonReflexive71  have leftCross : (2 * (m * n)) * a + m * (n * b + m * d) < m * (n * a + m * c) + (2 * (m * n)) * b72    ring_nf at augmentedLeft73    rw denominatorShape74    ring_nf75    exact augmentedLeft76  have qMid := rationalLess.of_representatives with mNonzero, denominatorNonzero, leftCross7778  have scaledRight := Less.mul_left with nNonzero, crossLess79  have rightCommonNat : Nat((m * n) * c + (m * n) * d) by typecheck80  have rightCommonReflexive := LessEqual.reflexive with rightCommonNat81  have augmentedRight := Less.add_LessEqual with scaledRight, rightCommonReflexive82  have rightCross : n * (n * a + m * c) + (2 * (m * n)) * d < (2 * (m * n)) * c + n * (n * b + m * d)83    ring_nf at augmentedRight84    rw denominatorShape85    ring_nf86    exact augmentedRight87  have midR := rationalLess.of_representatives with denominatorNonzero, nNonzero, rightCross8889  witness rationalClass(n * a + m * c,90    n * b + m * d, 2 * (m * n))91  constructor92    exact midpointRational93  . constructor94    . unfold rationalClass at qShape95      rw qShape96      unfold rationalClass97      exact qMid98    . unfold rationalClass at rShape99      rw rShape100      unfold rationalClass101      exact midR102