Grace/Cumulus/Real/PositiveInverse.g17

Open in Workbench Download source

Imports

Ring

Declarations

Source

1-- Multiplicative inverses of Dedekind real numbers2-- 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.Real.PositiveInverse8import Ring910-- For a positive cut A, this is the usual lower cut of 1/A.  The extra11-- rational s records openness: q belongs when q < s and some12-- positive r outside A still satisfies s*r < 1.13def positiveRealInvCut (A : Set) : Set :=14  { q ∈ ℚ |15    ¬(rationalZero < q) ∨16    ∃ s ∈ ℚ, q < s ∧17      ∃ r ∈ ℚ, ¬(r ∈ A) ∧ rationalZero < r ∧18        rationalMulValue(s, r) < rationalOne }1920theorem positiveRealInvCut.subset_rationals (A : Set)21  shows positiveRealInvCut(A) ⊆ ℚ22proof23  intros q member24  obtain ⟨qInQ, condition⟩ := positiveRealInvCut.membership.forward with member25  exact qInQ2627theorem positiveRealInvCut.of_nonpositive (A q : Set)28  requires qRational : Rational(q)29  requires nonpositive : ¬(rationalZero < q)30  shows q ∈ positiveRealInvCut(A)31proof32  apply positiveRealInvCut.membership.backward33  constructor34  . exact qRational35  . left36    exact nonpositive3738theorem positiveRealInvCut.of_witness (A : Set, q s r : Rational)39  requires below : q < s40  requires outside : ¬(r ∈ A)41  requires positive : rationalZero < r42  requires productBelowOne : rationalMulValue(s, r) < rationalOne43  shows q ∈ positiveRealInvCut(A)44proof45  apply positiveRealInvCut.membership.backward46  have qInQ : q ∈ ℚ by simp [Rational]47  have sInQ : s ∈ ℚ by simp [Rational]48  have rInQ : r ∈ ℚ by simp [Rational]49  constructor50  . exact qInQ51  . right52    witness s53    refine ⟨sInQ, below, r, rInQ, outside, positive, productBelowOne⟩5455theorem positiveRealInvCut.zero_mem (A : Set)56  shows rationalZero ∈ positiveRealInvCut(A)57proof58  apply positiveRealInvCut.of_nonpositive with rationalZero.rational59  intro zeroLessZero60  have irreflexive := rationalLess.irreflexive_on61  exact irreflexive with rationalZero, zeroLessZero6263theorem positiveRealInvCut.nonempty (A : Set)64  shows Nonempty(positiveRealInvCut(A))65proof66  witness rationalZero67  exact positiveRealInvCut.zero_mem6869theorem positiveRealInvCut.downward (A : Set, p q : Rational)70  requires qMember : q ∈ positiveRealInvCut(A)71  requires less : p < q72  shows p ∈ positiveRealInvCut(A)73proof74  obtain ⟨qInQ, condition⟩ := positiveRealInvCut.membership.forward with qMember75  cases condition with qNonpositive | witness76  . apply positiveRealInvCut.of_nonpositive at A, p77    intro pPositive78    have qPositive := rationalLess.transitive with rationalZero.rational, pPositive, less79    exact qNonpositive with qPositive80  . obtain ⟨s, sInQ, qLessS, r, rInQ, outside, positiveR,81      productBelowOne⟩ := witness82    have sRational : Rational(s) by exact sInQ83    have rRational : Rational(r) by exact rInQ84    have pLessS := rationalLess.transitive at p, q, s with85      *{2}, sRational, less, qLessS86    exact positiveRealInvCut.of_witness with87      assumption, sRational, rRational, pLessS, outside, positiveR, productBelowOne8889theorem rationalZero.lt_one90  shows rationalZero < rationalOne91proof92  have positive := rationalLess.positive_natural_successor with Naturals.constructor.zero93  simpa [rationalOne] using positive9495-- A positive displayed fraction (a-b)/m has the positive reciprocal96-- m/(a-b).  We expose only the field statement; coordinates are97-- confined to this proof so later analysis can reason entirely with *.98theorem rationalMulValue.exists_positive_inverse (x : Rational)99  requires positive : rationalZero < x100  shows ∃ y ∈ ℚ, rationalZero < y ∧ x * y = rationalOne101proof102  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=103    Rational.coordinates with assumption104  have oneNonzero : 1 ≠ 0105    intro oneZero106    arith107  have displayedPositive := positive108  rw xShape at displayedPositive109  unfold rationalZero at displayedPositive110  have bLessA : b < a111    have cross := rationalLess.classes.forward with oneNonzero, mNonzero, displayedPositive112    simpa [mul.left_zero, mul.right_zero, mul.left_unit,113      mul.right_unit, add.left_unit, add.right_unit] using cross114  obtain ⟨k, kNatural, aShape⟩ := bLessA115  have gapNonzero : succ(k) ≠ 0116    intro gapZero117    have zeroNotGap := Naturals.disjoint.zero.succ at k118    apply zeroNotGap119    rw gapZero120    rfl121  have inverseRational := rationalClass.rational at m, 0, succ(k) with122    gapNonzero123  have inversePositive : rationalZero < rationalClass(m, 0, succ(k))124    unfold rationalZero125    apply rationalLess.classes.backward with oneNonzero, gapNonzero126    ring_nf127    have mPositive := Less.add_positive at 0, m with mNonzero128    simpa [add.left_unit] using mPositive129  have productOne : rationalMulValue(rationalClass(a, b, m), rationalClass(m, 0, succ(k))) = rationalOne130    rw rationalMulValue.classes131    unfold rationalClassMul132    unfold rationalOne133    apply rationalClass.eq134    . exact mul.nonzero with mNonzero, gapNonzero135    . exact oneNonzero136    . rw ← aShape137      ring138  witness rationalClass(m, 0, succ(k))139  refine ⟨_, inversePositive, _⟩140    exact inverseRational141  . rw [rationalMulValue.notation, xShape]142    exact productOne143144-- Strictly separate two reciprocal bounds.  This is the approximation move145-- used by the real inverse proof: from q*r<a we choose b<s with q<a*b and146-- s*r<1.  The statement is coordinate-free and reads as plain algebra.147theorem rationalLess.exists_reciprocal_interval (q a r : Rational)148  requires positiveQ : rationalZero < q149  requires positiveA : rationalZero < a150  requires positiveR : rationalZero < r151  requires below : q * r < a152  shows ∃ b ∈ ℚ, ∃ s ∈ ℚ,153    rationalZero < b ∧ q < a * b ∧ b < s ∧ s * r < rationalOne154proof155  obtain ⟨u, uInQ, positiveU, auOne⟩ := rationalMulValue.exists_positive_inverse with positiveA156  obtain ⟨v, vInQ, positiveV, rvOne⟩ := rationalMulValue.exists_positive_inverse with positiveR157  have uRational : Rational(u) by exact uInQ158  have vRational : Rational(v) by exact vInQ159  have scaledBelow := rationalLess.mul_right at q * r, a, u with160    *{2}, uRational, positiveU, below161  rw auOne at scaledBelow162  have rquAssociative := rationalMulValue.associative at r, q, u with163    *{2}, uRational164  have rqCommutative := rationalMulValue.commutative at r, q with165    *{2}166  have productReassociate : r * (q * u) = (q * r) * u167    rw [← rqCommutative, rquAssociative]168    rfl169  rw ← productReassociate at scaledBelow170  have quBelowV : q * u < v171    apply rationalLess.of_mul_left with positiveR172    rwa rvOne173  obtain ⟨b, bInQ, quBelowB, bBelowV⟩ := rationalLess.dense at q * u, v with174    assumption, vRational, quBelowV175  have bRational : Rational(b) by exact bInQ176  have quPositive := rationalLess.mul_positive with positiveQ, positiveU177  have bPositive := rationalLess.transitive at rationalZero, q * u, b with178    rationalZero.rational, assumption, bRational, quPositive, quBelowB179  obtain ⟨s, sInQ, bBelowS, sBelowV⟩ := rationalLess.dense with bBelowV180  have qBelowABScaled := rationalLess.mul_left at q * u, b, a with181    assumption, bRational, assumption, positiveA, quBelowB182  have aquAssociative := rationalMulValue.associative at a, q, u with183    *{2}, uRational184  have aqCommutative := rationalMulValue.commutative at a, q with185    *{2}186  have qauAssociative := rationalMulValue.associative at q, a, u with187    *{2}, uRational188  have aqUShape : a * (q * u) = q189    rw [← aquAssociative, aqCommutative, qauAssociative, auOne]190    exact rationalMulValue.one_right with assumption191  rw aqUShape at qBelowABScaled192  have srBelowVR := rationalLess.mul_right with positiveR, sBelowV193  have vrOne : v * r = rationalOne194    have commutative := rationalMulValue.commutative at v, r with195      vRational, assumption196    rwa commutative197  rw vrOne at srBelowVR198  witness b199  refine ⟨bInQ, s, sInQ, bPositive, qBelowABScaled, bBelowS, srBelowVR⟩200201-- A positive cut can be crossed by positive rationals a<r so tightly that202-- q*r<a, for any fixed 0<q<1.  This is the multiplicative form of the203-- Archimedean boundary approximation theorem.204theorem RealLess.exists_multiplicative_boundary (A : Real) (q : Rational)205  requires positiveA : 0 < A206  requires positiveQ : rationalZero < q207  requires qBelowOne : q < rationalOne208  shows ∃ a ∈ ℚ, a ∈ A ∧ rationalZero < a ∧209    ∃ r ∈ ℚ, ¬(r ∈ A) ∧ rationalZero < r ∧ q * r < a210proof211  have cutA := Real.characterization.forward with assumption212  obtain ⟨c, cInA, cPositive⟩ := RealLess.exists_positive_member with positiveA213  have subsetA := DedekindCut.subset_rationals with cutA214  have cInQ := subsetA with c, cInA215  have cRational : Rational(c) by exact cInQ216  have gapRational := rationalSubValue.rational at rationalOne, q with217    rationalOne.rational, assumption218  have gapPositive := rationalLess.sub_positive with qBelowOne219  have gapTimesCPositive := rationalLess.mul_positive with gapPositive, cPositive220  obtain ⟨epsilon, epsilonInQ, epsilonPositive, epsilonSmall⟩ := rationalLess.dense with221    rationalZero.rational, assumption, gapTimesCPositive222  have epsilonRational : Rational(epsilon) by exact epsilonInQ223  obtain ⟨p, pRational, pInA, shiftedOutside⟩ := DedekindCut.exists_boundary_within with cutA, epsilonPositive224  rw ← rationalAddValue.notation at shiftedOutside225  have shiftedRational := rationalAddValue.rational with pRational, epsilonRational226  have pInQ : p ∈ ℚ by simp [Rational]227  have shiftedInQ : p + epsilon ∈ ℚ by simp [Rational]228  have cDistinctShifted : c ≠ p + epsilon229    intro equal230    rw equal at cInA231    exact shiftedOutside with cInA232  have connected := rationalLess.connected_on233  have comparison := connected with234    c, cInQ, p + epsilon, shiftedInQ, cDistinctShifted235  have cBelowShifted : c < p + epsilon236    cases comparison with below | shiftedBelowC237    . exact below238    . have shiftedInA := DedekindCut.downward at A, p + epsilon, c with239        cutA, cInA, shiftedInQ, shiftedBelowC240      exfalso241      exact shiftedOutside with shiftedInA242  have gapBelowOne : rationalOne - q < rationalOne243    have translated := rationalLess.add_right at244      rationalZero, q, rationalOne - q with245        rationalZero.rational, assumption, gapRational, positiveQ246    have zeroPlusGap := rationalAddValue.zero_left with gapRational247    have gapCloses := rationalAddValue.add_sub_cancel_left at248      q, rationalOne with assumption, rationalOne.rational249    rwa [zeroPlusGap, gapCloses] at translated250  have gapCBelowC := rationalLess.mul_right with251    gapRational, rationalOne.rational, cRational, cPositive, gapBelowOne252  have oneTimesC := rationalMulValue.one_left with cRational253  rw oneTimesC at gapCBelowC254  have epsilonBelowC := rationalLess.transitive at255    epsilon, (rationalOne - q) * c, c with256      epsilonRational, assumption, cRational, epsilonSmall, gapCBelowC257  have cMinusEpsilonPositive := rationalLess.sub_positive with epsilonBelowC258  have shiftedCommutative := rationalAddValue.commutative with pRational, epsilonRational259  have cBelowEpsilonPlusP := cBelowShifted260  rw shiftedCommutative at cBelowEpsilonPlusP261  have cMinusEpsilonBelowP := rationalLess.sub_left with cBelowEpsilonPlusP262  have pPositive := rationalLess.transitive at263    rationalZero, c - epsilon, p with264      rationalZero.rational, assumption, pRational,265      cMinusEpsilonPositive, cMinusEpsilonBelowP266  have gapCBelowGapShifted := rationalLess.mul_left with267    cRational, shiftedRational, gapRational, gapPositive, cBelowShifted268  have epsilonBelowGapShifted := rationalLess.transitive with269    epsilonRational, *{2}, epsilonSmall, gapCBelowGapShifted270  have translatedProduct := rationalLess.add_left at271    epsilon, (rationalOne - q) * (p + epsilon), q * (p + epsilon) with272      epsilonRational, *{2}, epsilonBelowGapShifted273  have gapCloses := rationalAddValue.add_sub_cancel_left at274    q, rationalOne with assumption, rationalOne.rational275  have combinedProduct : q * (p + epsilon) +276      (rationalOne - q) * (p + epsilon) = p + epsilon277    have distributed := rationalMulValue.distributive_right at278      q, rationalOne - q, p + epsilon with279        assumption, gapRational, shiftedRational280    rw [← distributed, gapCloses]281    have oneTimesShifted := rationalMulValue.one_left with shiftedRational282    rw oneTimesShifted283    rfl284  rw combinedProduct at translatedProduct285  have productBelowP := rationalLess.of_add_right with translatedProduct286  witness p287  refine ⟨pInQ, pInA, pPositive, p + epsilon, shiftedInQ,288    shiftedOutside, _, productBelowP⟩289  exact rationalLess.transitive with290    rationalZero.rational, cRational, shiftedRational, cPositive, cBelowShifted291292theorem rationalLess.exists_large_positive_multiplier (a : Rational)293  requires positive : rationalZero < a294  shows ∃ q ∈ ℚ, rationalZero < q ∧ rationalOne < q * a295proof296  obtain ⟨D, dNatural, dNonzero, unitPositive, unitBelowA⟩ := rationalLess.exists_positive_unit_fraction with297    positive298  have oneNonzero : 1 ≠ 0299    intro oneZero300    arith301  have qRational := rationalClass.rational at D, 0, 1 with oneNonzero302  have qPositivePlain : rationalZero < rationalClass(D, 0, 1)303    have dPositive := Less.add_positive at 0, D with dNonzero304    simp [add.left_unit] at dPositive305    unfold rationalZero306    apply rationalLess.classes.backward with oneNonzero, oneNonzero307    ring_nf308    exact dPositive309  have productShape : rationalMulValue(310      rationalClass(D, 0, 1), rationalClass(1, 0, D)) = rationalOne311    rw rationalMulValue.classes312    unfold rationalClassMul313    unfold rationalOne314    apply rationalClass.eq315    . exact mul.nonzero at 1, D with oneNonzero, dNonzero316    . exact oneNonzero317    . ring318  have unitRational := rationalClass.rational at 1, 0, D with dNonzero319  have scaled := rationalLess.mul_left at320    rationalClass(1, 0, D), a, rationalClass(D, 0, 1) with321      unitRational, assumption, qRational, qPositivePlain, unitBelowA322  rw [rationalMulValue.notation, productShape] at scaled323  witness rationalClass(D, 0, 1)324  refine ⟨_, qPositivePlain, scaled⟩325  exact qRational326327theorem positiveRealInvCut.no_greatest (A : Set, q : Rational)328  requires cut : DedekindCut(A)329  requires member : q ∈ positiveRealInvCut(A)330  shows ∃ t ∈ positiveRealInvCut(A), q < t331proof332  obtain ⟨qInQ, condition⟩ := positiveRealInvCut.membership.forward with member333  cases condition with qNonpositive | witness334  . obtain ⟨r, rInQ, positiveR, outside⟩ :=335      DedekindCut.exists_positive_upper with cut336    have rRational : Rational(r) by exact rInQ337    obtain ⟨delta, deltaInQ, deltaPositive, deltaBelowOne, productSmall⟩ := rationalLess.exists_small_positive_multiplier with338      rRational, rationalOne.rational, positiveR, rationalZero.lt_one339    have deltaRational : Rational(delta) by exact deltaInQ340    have productCommutative := rationalMulValue.commutative with deltaRational, rRational341    rw [← productCommutative, rationalMulValue.notation] at productSmall342    obtain ⟨t, tInQ, zeroLessT, tLessDelta⟩ := rationalLess.dense with343      rationalZero.rational, deltaRational, deltaPositive344    have tRational : Rational(t) by exact tInQ345    have tMember := positiveRealInvCut.of_witness with346      tRational, deltaRational, rRational, tLessDelta, outside, positiveR, productSmall347    have distinct : q ≠ t348      intro equal349      rw ← equal at zeroLessT350      exact qNonpositive with zeroLessT351    have connected := rationalLess.connected_on352    have comparison := connected with q, qInQ, t, tInQ, distinct353    cases comparison with qLessT | tLessQ354    . refine ⟨t, tMember, qLessT⟩355    . have qPositive := rationalLess.transitive at rationalZero, t, q with356        rationalZero.rational, tRational, assumption, zeroLessT, tLessQ357      exfalso358      exact qNonpositive with qPositive359  . obtain ⟨s2, s2InQ, qLessS2, r2, r2InQ, outside2, positiveR2,360      productBelowOne2⟩ := witness361    have s2Rational : Rational(s2) by exact s2InQ362    have r2Rational : Rational(r2) by exact r2InQ363    obtain ⟨t2, t2InQ, qLessT2, tLessS2⟩ := rationalLess.dense at q, s2 with364      assumption, s2Rational, qLessS2365    have t2Rational : Rational(t2) by exact t2InQ366    have t2Member := positiveRealInvCut.of_witness with367      t2Rational, s2Rational, r2Rational, tLessS2, outside2, positiveR2, productBelowOne2368    refine ⟨t2, t2Member, qLessT2⟩369370theorem positiveRealInvCut.proper (A : Real)371  requires positive : 0 < A372  shows positiveRealInvCut(A) ≠ ℚ373proof374  obtain ⟨zeroReal, realA, properA⟩ := realLess.characterization.forward with positive375  obtain ⟨a, aInA, aMissingZero⟩ := ProperSubset.missing with properA376  have cutA := Real.characterization.forward at A with assumption377  have subsetQ := DedekindCut.subset_rationals with cutA378  have aInQ := subsetQ with a, aInA379  have aRational : Rational(a) by exact aInQ380  obtain ⟨b, bInA, aLessB⟩ := DedekindCut.no_greatest with cutA, aInA381  have bInQ := subsetQ with b, bInA382  have bRational : Rational(b) by exact bInQ383  have bDistinctZero : b ≠ rationalZero384    intro equal385    have aLessZero := aLessB386    rw equal at aLessZero387    have aInZeroCut : a ∈ rationalCut(rationalZero) := rationalCut.membership.backward with ⟨aInQ, aLessZero⟩388    unfold realZero at aMissingZero389    exact aMissingZero with aInZeroCut390  have connected := rationalLess.connected_on391  have zeroInQ := rationalZero.rational392  have zeroDistinctB : rationalZero ≠ b393    intro equal394    apply bDistinctZero395    rw equal396    rfl397  have signB := connected with398    rationalZero, zeroInQ, b, bInQ,399    zeroDistinctB400  have positiveB : rationalZero < b401    cases signB with zeroLessB | bLessZero402    . exact zeroLessB403    . have aLessZero := rationalLess.transitive at a, b, rationalZero with404        aRational, bRational, rationalZero.rational, aLessB, bLessZero405      have aInZeroCut : a ∈ rationalCut(rationalZero) := rationalCut.membership.backward with ⟨aInQ, aLessZero⟩406      exfalso407      unfold realZero at aMissingZero408      exact aMissingZero with aInZeroCut409  obtain ⟨q, qInQ, positiveQ, oneBelowProduct⟩ := rationalLess.exists_large_positive_multiplier with410    bRational, positiveB411  rw rationalMulValue.notation at oneBelowProduct412  have qRational : Rational(q) by exact qInQ413  intro equalAll414  have qMember : q ∈ positiveRealInvCut(A) by rwa equalAll415  obtain ⟨qInQAgain, condition⟩ := positiveRealInvCut.membership.forward with qMember416  cases condition with qNonpositive | witness417  . exact qNonpositive with positiveQ418  . obtain ⟨s, sInQ, qLessS, r, rInQ, outside, positiveR,419      productBelowOne⟩ := witness420    have sRational : Rational(s) by exact sInQ421    have rRational : Rational(r) by exact rInQ422    have bDistinctR : b ≠ r423      intro equal424      rw ← equal at outside425      exact outside with bInA426    have comparison := connected with b, bInQ, r, rInQ, bDistinctR427    have bLessR : b < r428      cases comparison with below | rLessB429      . exact below430      . have rInA := DedekindCut.downward at A, r, b with431          cutA, bInA, rInQ, rLessB432        exfalso433        exact outside with rInA434    have qbLessQr := rationalLess.mul_left with positiveQ, bLessR435    have qrLessSr := rationalLess.mul_right with positiveR, qLessS436    rw [rationalMulValue.notation, rationalMulValue.notation] at qbLessQr437    rw [rationalMulValue.notation, rationalMulValue.notation] at qrLessSr438    have qbRational := rationalMulValue.rational_raw with qRational, bRational439    have qrRational := rationalMulValue.rational_raw with qRational, rRational440    have srRational := rationalMulValue.rational_raw with sRational, rRational441    have oneBelowQr := rationalLess.transitive with442      rationalOne.rational, qbRational, qrRational, oneBelowProduct, qbLessQr443    have oneBelowSr := rationalLess.transitive with444      rationalOne.rational, qrRational, srRational, oneBelowQr, qrLessSr445    have cycle := rationalLess.transitive with446      rationalOne.rational, srRational, rationalOne.rational, oneBelowSr, productBelowOne447    have irreflexive := rationalLess.irreflexive_on448    exact irreflexive with rationalOne, cycle449450theorem positiveRealInvCut.cut (A : Real)451  requires positive : 0 < A452  shows DedekindCut(positiveRealInvCut(A))453proof454  have cutA := Real.characterization.forward with assumption455  constructor456  . exact positiveRealInvCut.subset_rationals at A457  constructor458  . exact positiveRealInvCut.nonempty at A459  constructor460  . exact positiveRealInvCut.proper with positive461  constructor462  . intros q qMember p pInQ pLessQ463    have qInQ := positiveRealInvCut.subset_rationals at A with q, qMember464    have qRational : Rational(q) by exact qInQ465    exact positiveRealInvCut.downward with qMember, pLessQ466  . intros q qMember467    have qInQ := positiveRealInvCut.subset_rationals at A with q, qMember468    exact positiveRealInvCut.no_greatest with cutA, qMember469470theorem positiveRealInvCut.real (A : Real)471  requires positive : 0 < A472  shows Real(positiveRealInvCut(A))473proof474  apply Real.characterization.backward475  exact positiveRealInvCut.cut with positive476477theorem positiveRealInvCut.positive (A : Real)478  requires positive : 0 < A479  shows realZero < positiveRealInvCut(A)480proof481  have inverseReal := positiveRealInvCut.real with positive482  have zeroSubset : realZero ⊆ positiveRealInvCut(A)483    intros q qInZero484    unfold realZero at qInZero485    obtain ⟨qInQ, qNegative⟩ := rationalCut.membership.forward with qInZero486    have qRational : Rational(q) by exact qInQ487    apply positiveRealInvCut.of_nonpositive with qRational488    intro qPositive489    have cycle := rationalLess.transitive with490      rationalZero.rational, qRational, rationalZero.rational, qPositive, qNegative491    have irreflexive := rationalLess.irreflexive_on492    exact irreflexive with rationalZero, cycle493  obtain ⟨t, tInInverse, zeroLessT⟩ :=494    positiveRealInvCut.no_greatest at A, rationalZero with495      Real.characterization.forward at A with assumption,496      positiveRealInvCut.zero_mem at A497  have tMissingZero : ¬(t ∈ realZero)498    intro tInZero499    unfold realZero at tInZero500    obtain ⟨tInQ, tNegative⟩ := rationalCut.membership.forward with tInZero501    have tRational : Rational(t) by exact tInQ502    have cycle := rationalLess.transitive with503      rationalZero.rational, tRational, rationalZero.rational, zeroLessT, tNegative504    have irreflexive := rationalLess.irreflexive_on505    exact irreflexive with rationalZero, cycle506  have unequal : realZero ≠ positiveRealInvCut(A)507    intro equal508    apply tMissingZero509    rwa equal510  apply realLess.characterization.backward511  unfold RealLess512  refine ⟨realZero.real, inverseReal, _⟩513  constructor514  . exact zeroSubset515  . exact unequal516517theorem positiveRealInvCut.product_subset_one (A : Real)518  requires positive : 0 < A519  shows realPosMulCut(A, positiveRealInvCut(A)) ⊆ realOne520proof521  have cutA := Real.characterization.forward with assumption522  have subsetA := DedekindCut.subset_rationals with cutA523  intros q qInProduct524  obtain ⟨qInQ, condition⟩ := realPosMulCut.membership.forward with qInProduct525  have qRational : Rational(q) by exact qInQ526  unfold realOne527  apply rationalCut.membership.backward528  constructor529  . exact qInQ530  . cases condition with qNegative | product531    . exact rationalLess.transitive at q, rationalZero, rationalOne with532        qRational, rationalZero.rational, rationalOne.rational,533        qNegative, rationalZero.lt_one534    . obtain ⟨a, aInQ, aInA, b, bInQ, bInInverse,535        positiveA, positiveB, qLessProduct⟩ := product536      have aRational : Rational(a) by exact aInQ537      have bRational : Rational(b) by exact bInQ538      obtain ⟨bInQAgain, inverseCondition⟩ := positiveRealInvCut.membership.forward with bInInverse539      cases inverseCondition with bNonpositive | witness540      . exfalso541        exact bNonpositive with positiveB542      . obtain ⟨s, sInQ, bLessS, r, rInQ, outside, positiveR,543          productBelowOne⟩ := witness544        have sRational : Rational(s) by exact sInQ545        have rRational : Rational(r) by exact rInQ546        have distinct : a ≠ r547          intro equal548          rw ← equal at outside549          exact outside with aInA550        have connected := rationalLess.connected_on551        have comparison := connected with a, aInQ, r, rInQ, distinct552        have aLessR : a < r553          cases comparison with below | rLessA554          . exact below555          . have rInA := DedekindCut.downward at A, r, a with556              cutA, aInA, rInQ, rLessA557            exfalso558            exact outside with rInA559        have abLessRb := rationalLess.mul_right with positiveB, aLessR560        have rbLessRs := rationalLess.mul_left with positiveR, bLessS561        rw rationalMulValue.notation at qLessProduct562        rw [rationalMulValue.notation, rationalMulValue.notation] at abLessRb563        rw [rationalMulValue.notation, rationalMulValue.notation] at rbLessRs564        have abRational := rationalMulValue.rational_raw with aRational, bRational565        have rbRational := rationalMulValue.rational_raw with rRational, bRational566        have rsRational := rationalMulValue.rational_raw with rRational, sRational567        have qLessRb := rationalLess.transitive with qRational, abRational, rbRational, qLessProduct, abLessRb568        have qLessRs := rationalLess.transitive with qRational, rbRational, rsRational, qLessRb, rbLessRs569        have productCommutative := rationalMulValue.commutative with rRational, sRational570        rw [rationalMulValue.notation, rationalMulValue.notation] at productCommutative571        rw ← productCommutative at productBelowOne572        exact rationalLess.transitive with573          qRational, rsRational, rationalOne.rational, qLessRs, productBelowOne574575theorem positiveRealInvCut.one_subset_product (A : Real)576  requires positive : 0 < A577  shows realOne ⊆ realPosMulCut(A, positiveRealInvCut(A))578proof579  have inverseReal := positiveRealInvCut.real with positive580  have inversePositive := positiveRealInvCut.positive with positive581  intros q qInOne582  unfold realOne at qInOne583  obtain ⟨qInQ, qBelowOne⟩ := rationalCut.membership.forward with qInOne584  apply realPosMulCut.membership.backward585  constructor586  . exact qInQ587  . by_contra noCondition588    have noNegative : ¬(q < rationalZero)589      intro qNegative590      apply noCondition591      left592      exact qNegative593    have noProduct : ¬(∃ a ∈ ℚ, a ∈ A ∧594        ∃ b ∈ ℚ, b ∈ positiveRealInvCut(A) ∧595          rationalZero < a ∧ rationalZero < b ∧ q < a * b)596      intro product597      apply noCondition598      right599      exact product600    have qPositive : rationalZero < q601      by_contra notPositive602      have qEqualZero : q = rationalZero603        by_contra qNotZero604        have qDistinctZero : q ≠ rationalZero by exact qNotZero605        have connected := rationalLess.connected_on606        have zeroInQ := rationalZero.rational607        have comparison := connected with608          q, qInQ, rationalZero, zeroInQ, qDistinctZero609        cases comparison with qBelowZero | zeroBelowQ610        . exact noNegative with qBelowZero611        . exact notPositive with zeroBelowQ612      obtain ⟨a0, a0InA, a0Positive⟩ := RealLess.exists_positive_member with positive613      obtain ⟨b0, b0InInverse, b0Positive⟩ := RealLess.exists_positive_member with614        inverseReal, inversePositive615      have cutA := Real.characterization.forward at A with assumption616      have cutInverse := Real.characterization.forward with inverseReal617      have subsetA := DedekindCut.subset_rationals with cutA618      have subsetInverse := DedekindCut.subset_rationals with cutInverse619      have a0InQ := subsetA with a0, a0InA620      have b0InQ := subsetInverse with b0, b0InInverse621      have productPositive := rationalLess.mul_positive with a0Positive, b0Positive622      rw ← qEqualZero at productPositive623      apply noProduct624      refine ⟨a0, a0InQ, a0InA, b0, b0InQ, b0InInverse,625        a0Positive, b0Positive, productPositive⟩626    obtain ⟨a, aInQ, aInA, aPositive, r, rInQ, rOutside, rPositive, qrBelowA⟩ := RealLess.exists_multiplicative_boundary with627      positive, qPositive, qBelowOne628    have rRational : Rational(r) by exact rInQ629    obtain ⟨b, bInQ, s, sInQ, bPositive, qBelowAB, bBelowS, srBelowOne⟩ := rationalLess.exists_reciprocal_interval with630      qPositive, aPositive, rPositive, qrBelowA631    have bRational : Rational(b) by exact bInQ632    have sRational : Rational(s) by exact sInQ633    rw rationalMulValue.notation at srBelowOne634    have bInInverse := positiveRealInvCut.of_witness with635      bRational, sRational, rRational, bBelowS, rOutside, rPositive, srBelowOne636    apply noProduct637    refine ⟨a, aInQ, aInA, b, bInQ, bInInverse,638      aPositive, bPositive, qBelowAB⟩639640theorem positiveRealInvCut.product_eq_one (A : Real)641  requires positive : 0 < A642  shows realPosMulCut(A, positiveRealInvCut(A)) = realOne643proof644  apply Subset.antisymmetric645  . exact positiveRealInvCut.product_subset_one with positive646  . exact positiveRealInvCut.one_subset_product with positive647648theorem positiveRealInvCut.mul_eq_one (A : Real)649  requires positive : 0 < A650  shows realMulValue(A, positiveRealInvCut(A)) = realOne651proof652  obtain ⟨zeroReal, realA, properA⟩ := realLess.characterization.forward with positive653  have nonnegativeA := ProperSubset.subset with properA654  have inversePositive := positiveRealInvCut.positive with positive655  obtain ⟨zeroRealAgain, inverseReal, properInverse⟩ := realLess.characterization.forward with inversePositive656  have nonnegativeInverse := ProperSubset.subset with properInverse657  have computed := realMulValue.cut at A, positiveRealInvCut(A) with658    assumption, inverseReal659  unfold call2 at computed660  have reduction := realMulCut.of_nonnegative at661    A, positiveRealInvCut(A) with662      assumption, inverseReal, nonnegativeA, nonnegativeInverse663  have productOne := positiveRealInvCut.product_eq_one with positive664  unfold realMulValue665  cc666