Grace/Cumulus/Rat/Order.g17

Open in Workbench Download source

Imports

Defs · Cumulus.Order

Declarations

Source

1-- Order on rational quotient classes2-- 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.Order8import Defs9import Cumulus.Order1011-- For representatives ((a,b),m) and ((c,d),n), the intended fractions are12-- (a-b)/m and (c-d)/n. Cross multiplication uses naturals only:13--   n*a + m*d < m*c + n*b.14predicate rationalRepresentativeLess (u v : Set) :=15  ∃ a ∈ ℕ, ∃ b ∈ ℕ,16  ∃ m ∈ positiveNaturals, ∃ c ∈ ℕ,17  ∃ d ∈ ℕ, ∃ n ∈ positiveNaturals,18    u = ((a, b), m) ∧ v = ((c, d), n) ∧19    n * a + m * d < m * c + n * b2021-- On displayed representatives, rational order is exactly the familiar22-- cross-multiplication inequality. This is the arithmetic boundary used by23-- the quotient-level order proofs below.24theorem rationalRepresentativeLess.pair (a b m c d n : Nat)25  requires mNonzero : m ≠ 026  requires nNonzero : n ≠ 027  shows rationalRepresentativeLess(((a, b), m), ((c, d), n)) ↔28    n * a + m * d < m * c + n * b29proof30  constructor31  . intro less32    obtain ⟨wa, waNat, wb, wbNat, wm, wmPositive, wc, wcNat, wd, wdNat, wn, wnPositive, leftShape, rightShape, inequality⟩ := less33    obtain ⟨numeratorLeft, denominatorLeft⟩ := orderedPair.injective with leftShape34    obtain ⟨numeratorRight, denominatorRight⟩ := orderedPair.injective with rightShape35    obtain ⟨aEquals, bEquals⟩ := orderedPair.injective with numeratorLeft36    obtain ⟨cEquals, dEquals⟩ := orderedPair.injective with numeratorRight37    simpa [aEquals, bEquals, denominatorLeft, cEquals, dEquals, denominatorRight] using inequality38  . intro inequality39    have mPositive : m ∈ positiveNaturals by simp [nat.omega, positiveNaturals.membership]40    have nPositive : n ∈ positiveNaturals by simp [nat.omega, positiveNaturals.membership]41    unfold rationalRepresentativeLess42    refine ⟨a, _, b, _, m, mPositive, c, _, d, _, n, nPositive, rfl, rfl, inequality⟩43    . settle with nat.omega44    . settle with nat.omega45    . settle with nat.omega46    . settle with nat.omega4748-- Replacing the right-hand fraction by an equivalent representative preserves49-- strict comparison. The certificate scales the comparison and equivalence50-- equation, combines them additively, then cancels the positive denominator.51theorem rationalRepresentativeLess.transport_right_cross (a b m c d n e f p : Nat)52  requires mNonzero : m ≠ 053  requires nNonzero : n ≠ 054  requires pNonzero : p ≠ 055  requires less : n * a + m * d < m * c + n * b56  requires equivalent : p * c + n * f = n * e + p * d57  shows p * a + m * f < m * e + p * b58proof59  have scaledLess := Less.mul_left with pNonzero, less60  ring_nf at scaledLess61  have scaledEquivalent : m * (p * c + n * f) = m * (n * e + p * d) by linear_combination m * equivalent62  ring_nf at scaledEquivalent63  have combined := Less.replace_right with scaledLess, scaledEquivalent64  have scaledTarget : n * (p * a + m * f) < n * (m * e + p * b)65    ring_nf at combined66    ring_nf67    exact combined68  exact Less.mul_left_cancel_positive with nNonzero, scaledTarget6970-- Replacing the left-hand fraction by an equivalent representative preserves71-- strict comparison. Clearing denominators reduces this to an ordered-additive72-- replacement, followed by cancellation of the positive common factor.73theorem rationalRepresentativeLess.transport_left_cross (a b m c d n e f p : Nat)74  requires mNonzero : m ≠ 075  requires nNonzero : n ≠ 076  requires pNonzero : p ≠ 077  requires equivalent : p * a + m * f = m * e + p * b78  requires less : n * a + m * d < m * c + n * b79  shows n * e + p * d < p * c + n * f80proof81  have scaledLess := Less.mul_left with pNonzero, less82  ring_nf at scaledLess83  have scaledEquivalent : n * (p * a + m * f) = n * (m * e + p * b) by linear_combination n * equivalent84  ring_nf at scaledEquivalent85  have combined := Less.replace_left with scaledEquivalent, scaledLess86  have scaledTarget : m * (n * e + p * d) < m * (p * c + n * f)87    ring_nf at combined88    ring_nf89    exact combined90  exact Less.mul_left_cancel_positive with mNonzero, scaledTarget9192-- Strict comparison of displayed representatives is transitive. The middle93-- representative disappears by scaling both comparisons to common products,94-- composing the resulting inequalities, and cancelling positive factors.95theorem rationalRepresentativeLess.transitive_cross (a b m c d n e f p : Nat)96  requires mNonzero : m ≠ 097  requires nNonzero : n ≠ 098  requires pNonzero : p ≠ 099  requires left : n * a + m * d < m * c + n * b100  requires right : p * c + n * f < n * e + p * d101  shows p * a + m * f < m * e + p * b102proof103  have scaledLeft := Less.mul_left with pNonzero, left104  ring_nf at scaledLeft105  have scaledRight := Less.mul_left with mNonzero, right106  ring_nf at scaledRight107  have combined := Less.cross_transitive with scaledLeft, scaledRight108  have scaledTarget : n * (p * a + m * f) < n * (m * e + p * b)109    ring_nf at combined110    ring_nf111    exact combined112  exact Less.mul_left_cancel_positive with nNonzero, scaledTarget113114theorem rationalRepresentativeLess.transport_right (u v w : Set)115  requires hu : u ∈ rationalRepresentatives116  requires hv : v ∈ rationalRepresentatives117  requires hw : w ∈ rationalRepresentatives118  requires less : rationalRepresentativeLess(u, v)119  requires equivalent : relates(rationalEquivalent, v, w)120  shows rationalRepresentativeLess(u, w)121proof122  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu123  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv124  obtain ⟨e, eNat, f, fNat, p, pNat, pNonzero, wShape⟩ := rationalRepresentatives.coordinates with hw125  have displayedLess : rationalRepresentativeLess(126      ((a, b), m), ((c, d), n))127    simpa [uShape, vShape] using less128  have displayedEquivalent : relates(129      rationalEquivalent, ((c, d), n), ((e, f), p))130    simpa [vShape, wShape] using equivalent131  have crossLess := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess132  have crossEquivalent := rationalEquivalent.relates_representatives.forward with133    nNonzero, pNonzero, displayedEquivalent134  have transported := rationalRepresentativeLess.transport_right_cross with135    mNonzero, nNonzero, pNonzero, crossLess, crossEquivalent136  have displayedResult := rationalRepresentativeLess.pair.backward with mNonzero, pNonzero, transported137  simpa [uShape, wShape] using displayedResult138139theorem rationalRepresentativeLess.transport_left (u v w : Set)140  requires hu : u ∈ rationalRepresentatives141  requires hv : v ∈ rationalRepresentatives142  requires hw : w ∈ rationalRepresentatives143  requires equivalent : relates(rationalEquivalent, u, w)144  requires less : rationalRepresentativeLess(u, v)145  shows rationalRepresentativeLess(w, v)146proof147  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu148  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv149  obtain ⟨e, eNat, f, fNat, p, pNat, pNonzero, wShape⟩ := rationalRepresentatives.coordinates with hw150  have displayedEquivalent : relates(151      rationalEquivalent, ((a, b), m), ((e, f), p))152    simpa [uShape, wShape] using equivalent153  have displayedLess : rationalRepresentativeLess(154      ((a, b), m), ((c, d), n))155    simpa [uShape, vShape] using less156  have crossEquivalent := rationalEquivalent.relates_representatives.forward with157    mNonzero, pNonzero, displayedEquivalent158  have crossLess := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess159  have transported := rationalRepresentativeLess.transport_left_cross with160    mNonzero, nNonzero, pNonzero, crossEquivalent, crossLess161  have displayedResult := rationalRepresentativeLess.pair.backward with pNonzero, nNonzero, transported162  simpa [wShape, vShape] using displayedResult163164theorem rationalRepresentativeLess.transport (u v uPrime vPrime : Set)165  requires hu : u ∈ rationalRepresentatives166  requires hv : v ∈ rationalRepresentatives167  requires huPrime : uPrime ∈ rationalRepresentatives168  requires hvPrime : vPrime ∈ rationalRepresentatives169  requires leftEquivalent : relates(rationalEquivalent, u, uPrime)170  requires rightEquivalent : relates(rationalEquivalent, v, vPrime)171  requires less : rationalRepresentativeLess(u, v)172  shows rationalRepresentativeLess(uPrime, vPrime)173proof174  have movedLeft := rationalRepresentativeLess.transport_left with hu, hv, huPrime, leftEquivalent, less175  exact rationalRepresentativeLess.transport_right with huPrime, hv, hvPrime, movedLeft, rightEquivalent176177theorem rationalRepresentativeLess.transitive (u v w : Set)178  requires hu : u ∈ rationalRepresentatives179  requires hv : v ∈ rationalRepresentatives180  requires hw : w ∈ rationalRepresentatives181  requires left : rationalRepresentativeLess(u, v)182  requires right : rationalRepresentativeLess(v, w)183  shows rationalRepresentativeLess(u, w)184proof185  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu186  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv187  obtain ⟨e, eNat, f, fNat, p, pNat, pNonzero, wShape⟩ := rationalRepresentatives.coordinates with hw188  have displayedLeft : rationalRepresentativeLess(189      ((a, b), m), ((c, d), n))190    simpa [uShape, vShape] using left191  have displayedRight : rationalRepresentativeLess(192      ((c, d), n), ((e, f), p))193    simpa [vShape, wShape] using right194  have leftCross := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLeft195  have rightCross := rationalRepresentativeLess.pair.forward with nNonzero, pNonzero, displayedRight196  have cross := rationalRepresentativeLess.transitive_cross with197    mNonzero, nNonzero, pNonzero, leftCross, rightCross198  have displayedResult := rationalRepresentativeLess.pair.backward with mNonzero, pNonzero, cross199  simpa [uShape, wShape] using displayedResult200201predicate rationalLessWitness (p : Set) :=202  ∃ q ∈ ℚ, ∃ r ∈ ℚ,203    p = (q, r) ∧ ∃ u ∈ q, ∃ v ∈ r,204    rationalRepresentativeLess(u, v)205206-- This graph is bounded by rationals × rationals, hence is a set.207-- Well-definedness under rationalEquivalent is the next arithmetic theorem;208-- the definition itself already exposes the exact representative semantics.209def rationalLess : Set :=210  { p ∈ ℚ × ℚ | rationalLessWitness(p) }211212theorem rationalLess.bounded213  shows (rationalLess ⊆ ℚ × ℚ)214proof215  simp216217theorem rationalLess.relation218  shows RelationOn(rationalLess, ℚ)219proof220  unfold RelationOn221  exact rationalLess.bounded222223instance rationalLess.operation224  shows LessOperation(ℚ, rationalLess)225proof226  unfold LessOperation227  exact rationalLess.relation228229notation infix 50 "<" => relates via LessOperation(ℚ, _) for Rational230231theorem rationalLess.of_members (q r u v : Set)232  requires qRational : q ∈ ℚ233  requires rRational : r ∈ ℚ234  requires hu : u ∈ q235  requires hv : v ∈ r236  requires less : rationalRepresentativeLess(u, v)237  shows relates(rationalLess, q, r)238proof239  unfold relates240  apply rationalLess.membership.backward241  have bounded := product.pair with qRational, rRational242  constructor243  . exact bounded244  . unfold rationalLessWitness245    refine ⟨q, qRational, r, rRational, rfl, u, hu, v, hv, less⟩246247-- Equivalent rational representatives denote the same quotient point, so a248-- strict representative comparison between them is impossible.249theorem rationalRepresentativeLess.not_equivalent (u v : Set)250  requires hu : u ∈ rationalRepresentatives251  requires hv : v ∈ rationalRepresentatives252  requires equivalent : relates(rationalEquivalent, u, v)253  shows ¬rationalRepresentativeLess(u, v)254proof255  intro less256  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu257  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv258  have displayedEquivalent : relates(259      rationalEquivalent, ((a, b), m), ((c, d), n))260    simpa [uShape, vShape] using equivalent261  have displayedLess : rationalRepresentativeLess(262      ((a, b), m), ((c, d), n))263    simpa [uShape, vShape] using less264  have crossEqual := rationalEquivalent.relates_representatives.forward with265    mNonzero, nNonzero, displayedEquivalent266  have crossLess := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess267  rw crossEqual at crossLess268  exact Less.irreflexive with crossLess269270-- Elimination view for rational order. Client proofs receive representatives271-- together with their class memberships and ambient representative facts;272-- the quotient encoding stays behind this boundary.273theorem rationalLess.representatives (q r : Set)274  requires qRational : q ∈ ℚ275  requires rRational : r ∈ ℚ276  requires less : relates(rationalLess, q, r)277  shows ∃ u ∈ q, u ∈ rationalRepresentatives ∧278    ∃ v ∈ r, v ∈ rationalRepresentatives ∧ rationalRepresentativeLess(u, v)279proof280  unfold relates at less281  obtain ⟨_, left, _, right, _, shape, u, uMember, v, vMember, representativeLess⟩ := rationalLess.membership.forward with less282  obtain ⟨leftShape, rightShape⟩ := orderedPair.injective with shape283  rw ← leftShape at uMember284  rw ← rightShape at vMember285  have uRepresentative := Rational.representative with qRational, uMember286  have vRepresentative := Rational.representative with rRational, vMember287  refine ⟨u, uMember, uRepresentative, v, vMember, vRepresentative, representativeLess⟩288289theorem rationalLess.irreflexive_on290  shows IrreflexiveOn(ℚ, rationalLess)291proof292  intros q qRational less293  obtain ⟨u, uInQ, uRepresentative, v, vInQ, vRepresentative, representativeLess⟩ := rationalLess.representatives with294    qRational, qRational, less295  have equivalent := Rational.members_related with qRational, uInQ, vInQ296  exact rationalRepresentativeLess.not_equivalent with297    uRepresentative, vRepresentative, equivalent, representativeLess298299theorem rationalLess.transitive_on300  shows TransitiveOn(ℚ, rationalLess)301proof302  intros q qRational r rRational s sRational lessQR lessRS303  obtain ⟨u, uInQ, uRepresentative, v, vInR, vRepresentative, representativeLessUV⟩ := rationalLess.representatives with304    qRational, rRational, lessQR305  obtain ⟨vPrime, vPrimeInR, vPrimeRepresentative, w, wInS, wRepresentative, representativeLessVW⟩ := rationalLess.representatives with306    rRational, sRational, lessRS307  have middleEquivalent := Rational.members_related with rRational, vInR, vPrimeInR308  have aligned := rationalRepresentativeLess.transport_right with309    uRepresentative, vRepresentative, vPrimeRepresentative, representativeLessUV, middleEquivalent310  have representativeLessUW := rationalRepresentativeLess.transitive with311    uRepresentative, vPrimeRepresentative, wRepresentative, aligned, representativeLessVW312  exact rationalLess.of_members with qRational, sRational, uInQ, wInS, representativeLessUW313314theorem rationalLess.connected_on315  shows ConnectedOn(ℚ, rationalLess)316proof317  intros q qRational r rRational distinct318  obtain ⟨u, uInQ, uRepresentative⟩ := Rational.some_representative with qRational319  obtain ⟨v, vInR, vRepresentative⟩ := Rational.some_representative with rRational320  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with uRepresentative321  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with vRepresentative322  have leftCrossNat : Nat(n * a + m * d) by typecheck323  have rightCrossNat : Nat(m * c + n * b) by typecheck324  have comparison := Less.trichotomy with leftCrossNat, rightCrossNat325  rcases comparison with less | equal | greater326  . left327    have representativeLess : rationalRepresentativeLess(u, v)328      simpa [uShape, vShape] using329        rationalRepresentativeLess.pair.backward with mNonzero, nNonzero, less330    exact rationalLess.of_members with qRational, rRational, uInQ, vInR, representativeLess331  . exfalso332    have representativeEquivalent : relates(rationalEquivalent, u, v)333      simpa [uShape, vShape] using334        rationalEquivalent.relates_representatives.backward with mNonzero, nNonzero, equal335    apply distinct336    exact Rational.eq_of_related_members with qRational, rRational, uInQ, vInR, representativeEquivalent337  . right338    have representativeGreater : rationalRepresentativeLess(v, u)339      simpa [uShape, vShape] using340        rationalRepresentativeLess.pair.backward with nNonzero, mNonzero, greater341    exact rationalLess.of_members with rRational, qRational, vInR, uInQ, representativeGreater342343theorem rationalLess.strict_order344  shows StrictOrder(ℚ, rationalLess)345proof346  unfold StrictOrder347  have relation := rationalLess.relation348  refine ⟨relation, rationalLess.irreflexive_on, rationalLess.transitive_on⟩349350theorem rationalLess.strict_linear_order351  shows StrictLinearOrder(ℚ, rationalLess)352proof353  refine ⟨rationalLess.strict_order, rationalLess.connected_on⟩354355-- A strict comparison of representatives descends to a comparison of their356-- rational equivalence classes. No representative is chosen by the kernel:357-- the two displayed representatives are explicit witnesses in their classes.358theorem rationalLess.of_representatives (a b m c d n : Nat)359  requires mNonzero : m ≠ 0360  requires nNonzero : n ≠ 0361  requires crossLess : n * a + m * d < m * c + n * b362  shows relates(363    rationalLess,364    ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent],365    ⟦((c, d), n)⟧[rationalRepresentatives, rationalEquivalent])366proof367  have leftRepresentative := rationalRepresentatives.pair at a, b, m with mNonzero368  have rightRepresentative := rationalRepresentatives.pair at c, d, n with nNonzero369  have equivalence := rationalEquivalent.equivalence370  have leftRational := quotient.contains_class with equivalence, leftRepresentative371  have rightRational := quotient.contains_class with equivalence, rightRepresentative372  have leftSelf := equivalenceClass.self with equivalence, leftRepresentative373  have rightSelf := equivalenceClass.self with equivalence, rightRepresentative374  have representativeLess := rationalRepresentativeLess.pair.backward with mNonzero, nNonzero, crossLess375  exact rationalLess.of_members with leftSelf, rightSelf, representativeLess376