Grace/Cumulus/Real/Negation.g17

Open in Workbench Download source

Imports

Addition · Archimedean · Algebra.OrderedField.Defs

Declarations

Source

1-- Negation 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.Negation8import Addition9import Archimedean10import Algebra.OrderedField.Defs1112-- The open reflected complement of a lower cut.  The strict inequality is13-- essential: it makes the result rounded without choosing endpoints.14def realNegCut (A : Set) : Set :=15  { q ∈ ℚ | ∃ r ∈ ℚ, ¬(r ∈ A) ∧ q < -r }1617theorem realNegCut.subset_rationals (A : Set)18  shows realNegCut(A) ⊆ ℚ19proof20  simp2122theorem realNegCut.nonempty (A : Real)23  shows Nonempty(realNegCut(A))24proof25  have cutA := Real.characterization.forward with assumption26  have properA := DedekindCut.proper with cutA27  obtain ⟨u, uInQ, uMissing⟩ := ProperSubset.missing with properA28  have uRational : Rational(u) by exact uInQ29  have negURational := rationalNegValue.rational with uRational30  obtain ⟨q, qInQ, qLessNegU⟩ := rationalLess.exists_below with negURational31  witness q32  exact realNegCut.membership.backward with ⟨qInQ, u, uInQ, uMissing, qLessNegU⟩3334theorem realNegCut.proper (A : Real)35  shows realNegCut(A) ≠ ℚ36proof37  have cutA := Real.characterization.forward with assumption38  obtain ⟨a, aInA⟩ := DedekindCut.nonempty with cutA39  have subsetA := DedekindCut.subset_rationals with cutA40  have aInQ := subsetA with a, aInA41  have aRational : Rational(a) by exact aInQ42  have negARational := rationalNegValue.rational with aRational43  intro allRationals44  have negAInCut : -a ∈ realNegCut(A)45    rw allRationals46    exact negARational47  obtain ⟨negAInQ, r, rInQ, rMissing, negALessNegR⟩ := realNegCut.membership.forward with negAInCut48  have rRational : Rational(r) by exact rInQ49  have negated := rationalLess.neg_reverse at -a, -r with50    negARational, rationalNegValue.rational at r with rRational,51    negALessNegR52  have involutiveA := rationalNegValue.involutive with aRational53  have involutiveR := rationalNegValue.involutive with rRational54  rw [involutiveA, involutiveR] at negated55  have rInA := DedekindCut.downward with cutA, aInA, rInQ, negated56  exact rMissing with rInA5758theorem realNegCut.downward (A p q : Set)59  requires qInNeg : q ∈ realNegCut(A)60  requires pInQ : p ∈ ℚ61  requires pLessQ : relates(rationalLess, p, q)62  shows p ∈ realNegCut(A)63proof64  obtain ⟨qInQ, r, rInQ, rMissing, qLessNegR⟩ := realNegCut.membership.forward with qInNeg65  have pRational : Rational(p) by exact pInQ66  have qRational : Rational(q) by exact qInQ67  have rRational : Rational(r) by exact rInQ68  have pLessNegR := rationalLess.transitive at p, q, -r with69    pRational, qRational, rationalNegValue.rational at r with rRational,70    pLessQ, qLessNegR71  exact realNegCut.membership.backward with ⟨pInQ, r, rInQ, rMissing, pLessNegR⟩7273theorem realNegCut.no_greatest (A q : Set)74  requires qInNeg : q ∈ realNegCut(A)75  shows ∃ s ∈ realNegCut(A), relates(rationalLess, q, s)76proof77  obtain ⟨qInQ, r, rInQ, rMissing, qLessNegR⟩ := realNegCut.membership.forward with qInNeg78  obtain ⟨s, sInQ, qLessS, sLessNegR⟩ := rationalLess.dense with qLessNegR79  witness s80  constructor81  . apply realNegCut.membership.backward at A, s82    refine ⟨sInQ, r, rInQ, rMissing, sLessNegR⟩83  . exact qLessS8485theorem realNegCut.cut (A : Real)86  shows DedekindCut(realNegCut(A))87proof88  unfold DedekindCut89  refine ⟨realNegCut.subset_rationals at A,90    realNegCut.nonempty at A with assumption,91    realNegCut.proper at A with assumption, _, _⟩92  . intros q qInNeg p pInQ pLessQ93    exact realNegCut.downward with qInNeg, pInQ, pLessQ94  . intros q qInNeg95    exact realNegCut.no_greatest with qInNeg9697theorem realNegCut.real (A : Real)98  shows Real(realNegCut(A))99proof100  apply Real.characterization.backward101  exact realNegCut.cut with assumption102103theorem realNegCut.subset_reverse (A B : Real)104  requires subset : A ⊆ B105  shows realNegCut(B) ⊆ realNegCut(A)106proof107  intros q qInNegB108  obtain ⟨qInQ, r, rInQ, rMissingB, qLessNegR⟩ := realNegCut.membership.forward with qInNegB109  have rMissingA : ¬(r ∈ A)110    intro rInA111    specialize subset with r, rInA112    exact rMissingB with subset113  exact realNegCut.membership.backward with ⟨qInQ, r, rInQ, rMissingA, qLessNegR⟩114115-- Negation as a total set-valued function graph on the real carrier.116def realNeg : Set :=117  { p ∈ (ℝ × ℝ) | ∃ A ∈ ℝ, p = (A ↦ realNegCut(A)) }118119def realNegValue (A : Real) : Real := realNeg(A)120121theorem realNeg.relates (A : Real)122  shows relates(realNeg, A, realNegCut(A))123proof124  have realA : A ∈ ℝ by simp [Real]125  unfold relates126  apply realNeg.membership.backward127  constructor128  . apply product.pair at A, realNegCut(A), ℝ, ℝ129    . exact realA130    . exact realNegCut.real at A131  . refine ⟨A, realA, rfl⟩132133theorem realNeg.factors (input output : Set)134  requires mapped : relates(realNeg, input, output)135  shows ∃ A ∈ ℝ, input = A ∧ output = realNegCut(A)136proof137  unfold relates at mapped138  simp [realNeg.membership] at mapped139  rcases mapped with ⟨bounded, A, realA, shape⟩140  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape141  refine ⟨A, realA, inputShape, outputShape⟩142143theorem realNeg.total144  shows TotalBetween(realNeg, ℝ, ℝ)145proof146  intros A realA147  have typedA : Real(A) by exact realA148  refine ⟨realNegCut(A), realNegCut.real at A with typedA, realNeg.relates at A with typedA⟩149150theorem realNeg.functional151  shows Functional(realNeg)152proof153  intros input y inputY z inputZ154  obtain ⟨A, realA, inputFirst, outputFirst⟩ := realNeg.factors with inputY155  obtain ⟨B, realB, inputSecond, outputSecond⟩ := realNeg.factors with inputZ156  rw inputFirst at inputSecond157  rw [outputFirst, outputSecond, inputSecond]158  rfl159160theorem realNeg.function161  shows realNeg : ℝ → ℝ162proof163  constructor164    intros p member165    simp [realNeg.membership] at member166    rcases member with ⟨bounded, witnesses⟩167    exact bounded168  . constructor169    . exact realNeg.functional170    . exact realNeg.total171172instance realNeg.operation173  shows NegOperation(ℝ, realNeg)174proof175  exact realNeg.function176177notation prefix 75 "-" => apply via NegOperation(ℝ, _) for Real178179theorem realNegValue.real (A : Real)180  shows Real(-A)181proof182  have realA : A ∈ ℝ by simp [Real]183  obtain ⟨B, realB, mapped⟩ := FunctionBetween.exists_value with realNeg.function, realA184  have applied := FunctionBetween.apply_value with realNeg.function, mapped185  rw applied186  exact realB187188theorem realNegValue.cut (A : Real)189  shows -A = realNegCut(A)190proof191  have mapped := realNeg.relates at A192  exact FunctionBetween.apply_value with realNeg.function, mapped193194theorem realNegCut.involutive (A : Real)195  shows realNegCut(realNegCut(A)) = A196proof197  ext q198  constructor199  . intro qInDoubleNeg200    obtain ⟨qInQ, r, rInQ, rMissingNegA, qLessNegR⟩ := realNegCut.membership.forward with qInDoubleNeg201    by_contra qMissingA202    have qRational : Rational(q) by exact qInQ203    have rRational : Rational(r) by exact rInQ204    have rLessNegQ := rationalLess.neg_reverse at q, -r with205      qRational, rationalNegValue.rational at r with rRational,206      qLessNegR207    have involutiveR := rationalNegValue.involutive with rRational208    rw involutiveR at rLessNegQ209    have rInNegA : r ∈ realNegCut(A) := realNegCut.membership.backward with ⟨rInQ, q, qInQ, qMissingA, rLessNegQ⟩210    exact rMissingNegA with rInNegA211  . intro qInA212    have cutA := Real.characterization.forward with assumption213    have subsetA := DedekindCut.subset_rationals with cutA214    have qInQ := subsetA with q, qInA215    obtain ⟨s, sInA, qLessS⟩ := DedekindCut.no_greatest with cutA, qInA216    have sInQ := subsetA with s, sInA217    have sRational : Rational(s) by typecheck218    have negSRational := rationalNegValue.rational with sRational219    have negSMissing : ¬(-s ∈ realNegCut(A))220      intro negSInNegA221      obtain ⟨negSInQ, u, uInQ, uMissingA, negSLessNegU⟩ := realNegCut.membership.forward with negSInNegA222      have uRational : Rational(u) by exact uInQ223      have uLessS := rationalLess.neg_reverse at -s, -u with224        negSRational, rationalNegValue.rational at u with uRational,225        negSLessNegU226      have involutiveS := rationalNegValue.involutive with sRational227      have involutiveU := rationalNegValue.involutive with uRational228      rw [involutiveS, involutiveU] at uLessS229      have uInA := DedekindCut.downward with cutA, sInA, uInQ, uLessS230      exact uMissingA with uInA231    apply realNegCut.membership.backward232    have involutiveS := rationalNegValue.involutive with sRational233    rw ← involutiveS at qLessS234    refine ⟨qInQ, -s, negSRational, negSMissing, qLessS⟩235236theorem realNegValue.involutive (A : Real)237  shows -(-A) = A238proof239  have negReal := realNegValue.real at A240  calc241    -(-A) = realNegCut(-A) := realNegValue.cut at -A with negReal242    _ = realNegCut(realNegCut(A)) := by simp [realNegValue.cut]243    _ = A := realNegCut.involutive at A with assumption244245-- A cut and its reflected complement add to the zero cut.  The reverse246-- inclusion is the one genuinely Archimedean step: choose an interior247-- rational s between q and zero, then cross the boundary of A within -s.248theorem realAddCut.neg_right (A : Real)249  shows realAddCut(A, realNegCut(A)) = realZero250proof251  have cutA := Real.characterization.forward with assumption252  have subsetA := DedekindCut.subset_rationals with cutA253  ext q254  constructor255  . intro qInSum256    obtain ⟨qInQ, a, aInA, b, bInNegA, qLessSum⟩ := realAddCut.membership_value.forward with qInSum257    obtain ⟨bInQ, r, rInQ, rMissingA, bLessNegR⟩ := realNegCut.membership.forward with bInNegA258    have aRational : Rational(a)259      unfold Rational260      exact subsetA with a, aInA261    have bRational : Rational(b) by exact bInQ262    have rRational : Rational(r) by exact rInQ263    have aLessR := DedekindCut.lt_missing with cutA, aInA, rInQ, rMissingA264    have sumBelowDifference := rationalLess.add_left at265      b, -r, a with bRational,266      rationalNegValue.rational at r with rRational,267      aRational, bLessNegR268    have differenceNegative := rationalLess.sub_self_negative with aLessR269    unfold rationalSubValue at differenceNegative270    rw ← rationalAddValue.notation at qLessSum271    have qRational : Rational(q) by exact qInQ272    have qBelowDifference := rationalLess.transitive with qLessSum, sumBelowDifference273    have qBelowZero := rationalLess.transitive with qBelowDifference, differenceNegative274    unfold realZero275    simp [rationalCut.membership]276  . intro qInZero277    unfold realZero at qInZero278    simp [rationalCut.membership] at qInZero279    rcases qInZero with ⟨qInQ, qLessZero⟩280    have qRational : Rational(q) by exact qInQ281    obtain ⟨s, sInQ, qLessS, sLessZero⟩ := rationalLess.dense with qRational, rationalZero.rational, qLessZero282    have sRational : Rational(s) by exact sInQ283    have negSRational := rationalNegValue.rational with sRational284    have epsilonPositive : rationalZero < -s285      have shifted := rationalLess.add_right with sRational, rationalZero.rational, negSRational, sLessZero286      have inverse := rationalAddValue.neg_right with sRational287      have identity := rationalAddValue.zero_left with negSRational288      rwa [inverse, identity] at shifted289    obtain ⟨p, pRational, pInA, boundaryMissing⟩ := DedekindCut.exists_boundary_within with290      cutA, epsilonPositive291    have rRational := rationalAddValue.rational_raw with pRational, negSRational292    have pMinusR := rationalSubValue.sub_sum_left with pRational, negSRational293    have involutiveS := rationalNegValue.involutive with sRational294    rw involutiveS at pMinusR295    rw ← pMinusR at qLessS296    unfold rationalSubValue at qLessS297    have rNotationRational := rationalAddValue.rational with pRational, negSRational298    have negRNotationRational := rationalNegValue.rational with rNotationRational299    have qMinusPLessNegR := rationalLess.sub_left with qRational, pRational, negRNotationRational, qLessS300    have qMinusPRational := rationalSubValue.rational with qRational, pRational301    obtain ⟨t, tInQ, qMinusPLessT, tLessNegR⟩ := rationalLess.dense with302      qMinusPRational, negRNotationRational, qMinusPLessNegR303    rw rationalAddValue.notation at tLessNegR304    have tInNegA : t ∈ realNegCut(A)305      apply realNegCut.membership.backward306      refine ⟨tInQ, rationalAddValue(p, -s), rRational,307        boundaryMissing, tLessNegR⟩308    have qLessSum := rationalLess.add_left_of_sub_left with qRational, pRational, qMinusPLessT309    apply realAddCut.membership_value.backward310    rw rationalAddValue.notation at qLessSum311    refine ⟨qInQ, p, pInA, t, tInNegA, qLessSum⟩312313theorem realAddValue.neg_right (A : Real)314  shows A + (-A) = 0315proof316  calc317    A + (-A) = realAddCut(A, realNegCut(A)) := by simp [realAddValue.cut, realNegValue.cut]318    _ = realZero := realAddCut.neg_right at A with assumption319320theorem realAddValue.neg_left (A : Real)321  shows (-A) + A = 0322proof323  have negReal := realNegValue.real at A324  calc325    (-A) + A = A + (-A) :=326      realAddValue.commutative with negReal, assumption327    _ = realZero := realAddValue.neg_right at A with assumption328329instance realAdd.abelian_group330  shows IsAbelianGroup(ℝ, realAdd, realZero, realNeg)331proof332  constructor333    constructor334    . have additive := realAdd.comm_monoid335      simp [IsCommMonoid]336      constructor337      . exact realNeg.function338      . intros A realA339        have typedA : Real(A) by exact realA340        constructor341        . exact realAddValue.neg_left with typedA342        . exact realAddValue.neg_right with typedA343  . have additive := realAdd.comm_monoid344    simp [IsCommMonoid]345346theorem realNegCut.strict_antitone (A B : Real)347  requires proper : A ⊂ B348  shows realNegCut(B) ⊂ realNegCut(A)349proof350  constructor351    intros q qInNegB352    obtain ⟨qInQ, r, rInQ, rMissingB, qLessNegR⟩ := realNegCut.membership.forward with qInNegB353    have subsetAB := ProperSubset.subset with proper354    have rMissingA : ¬(r ∈ A)355      intro rInA356      have rInB := subsetAB with r, rInA357      exact rMissingB with rInB358    exact realNegCut.membership.backward with ⟨qInQ, r, rInQ, rMissingA, qLessNegR⟩359  . intro equalNeg360    have involutiveA := realNegCut.involutive at A361    have involutiveB := realNegCut.involutive at B362    rw [equalNeg, involutiveA] at involutiveB363    have unequal := ProperSubset.ne with proper364    exact unequal with involutiveB365366theorem RealLess.neg_reverse (A B : Real)367  requires less : RealLess(A, B)368  shows RealLess(-B, -A)369proof370  rcases less with ⟨realA, realB, proper⟩371  have negAReal := realNegValue.real with realA372  have negBReal := realNegValue.real with realB373  unfold RealLess374  refine ⟨negBReal, negAReal, _⟩375  have antitone := realNegCut.strict_antitone with realA, realB, proper376  have cutA := realNegValue.cut with realA377  have cutB := realNegValue.cut with realB378  rwa [cutA, cutB]379380-- Translation preserves the strict order on the Dedekind reals.  The subset381-- direction is immediate from witnesses for cut addition; strictness follows382-- by cancelling the common summand in the additive group.383theorem realAddCut.subset_left (A B C : Real)384  requires subset : A ⊆ B385  shows realAddCut(A, C) ⊆ realAddCut(B, C)386proof387  intros q qInAC388  obtain ⟨qInQ, a, aInA, c, cInC, qLessSum⟩ := realAddCut.membership_value.forward with qInAC389  have aInB : a ∈ B by exact subset with a, aInA390  exact realAddCut.membership_value.backward with ⟨qInQ, a, aInB, c, cInC, qLessSum⟩391392theorem realLess.add_right (A B C : Real)393  requires less : A < B394  shows A + C < B + C395proof396  obtain ⟨realA, realB, proper⟩ := realLess.characterization.forward with less397  have properSubset := ProperSubset.subset with proper398  have sumACReal := realAddValue.real at A, C with *399  have sumBCReal := realAddValue.real at B, C with *400  apply realLess.characterization.backward401  unfold RealLess402  refine ⟨sumACReal, sumBCReal, _⟩403  constructor404  . have cutSubset := realAddCut.subset_left at A, B, C with405      *{3}, properSubset406    have cutAC := realAddValue.cut at A, C with *407    have cutBC := realAddValue.cut at B, C with *408    rwa [← cutAC, ← cutBC] at cutSubset409  . intro equalSums410    have negCReal := realNegValue.real at C411    have equalCancelled : (A + C) + (-C) = (B + C) + (-C)412      rw equalSums413      rfl414    have leftCancel : (A + C) + (-C) = A415      calc416        (A + C) + (-C) = A + (C + (-C)) :=417          realAddValue.associative at A, C, -C with418            *{2}, negCReal419        _ = A + 0 := by simp [realAddValue.neg_right]420        _ = A := realAddValue.zero_right at A with assumption421    have rightCancel : (B + C) + (-C) = B422      calc423        (B + C) + (-C) = B + (C + (-C)) :=424          realAddValue.associative at B, C, -C with425            *{2}, negCReal426        _ = B + 0 := by simp [realAddValue.neg_right]427        _ = B := realAddValue.zero_right at B with assumption428    rw [leftCancel, rightCancel] at equalCancelled429    have unequal := ProperSubset.ne with proper430    exact unequal with equalCancelled431432theorem realLess.add_left (A B C : Real)433  requires less : A < B434  shows C + A < C + B435proof436  have translated := realLess.add_right at A, B, C with437    *{3}, less438  have leftCommutative := realAddValue.commutative at A, C with439    *{2}440  have rightCommutative := realAddValue.commutative at B, C with441    *{2}442  rwa [leftCommutative, rightCommutative] at translated443444theorem realLess.add (A B C D : Real)445  requires ab : A < B446  requires cd : C < D447  shows A + C < B + D448proof449  have first := realLess.add_right at A, B, C with450    *{3}, ab451  have second := realLess.add_left at C, D, B with452    *{3}, cd453  exact realLess.transitive with first, second454455theorem realLess.add_right_iff (A B C : Real)456  shows A + C < B + C ↔ A < B457proof458  constructor459  . intro translated460    have sumACReal := realAddValue.real at A, C with *461    have sumBCReal := realAddValue.real at B, C with *462    have negCReal := realNegValue.real at C463    have cancelled := realLess.add_right with sumACReal, sumBCReal, negCReal, translated464    have leftCancel : (A + C) + (-C) = A465      calc466        (A + C) + (-C) = A + (C + (-C)) :=467          realAddValue.associative at A, C, -C with468            *{2}, negCReal469        _ = A + 0 := by simp [realAddValue.neg_right]470        _ = A := realAddValue.zero_right at A with assumption471    have rightCancel : (B + C) + (-C) = B472      calc473        (B + C) + (-C) = B + (C + (-C)) :=474          realAddValue.associative at B, C, -C with475            *{2}, negCReal476        _ = B + 0 := by simp [realAddValue.neg_right]477        _ = B := realAddValue.zero_right at B with assumption478    rwa [leftCancel, rightCancel] at cancelled479  . intro less480    exact realLess.add_right with less481482-- Subtraction is addition of the additive inverse, exposed at the same typed483-- mathematical boundary as rational subtraction.484def realSubValue (A B : Real) : Real := A + (-B)485notation infixl 60 "-" => realSubValue for Real486487theorem realSubValue.real (A B : Real)488  shows Real(A - B)489proof490  unfold realSubValue491  exact realAddValue.real at A, -B with492    assumption, realNegValue.real at B with assumption493494theorem realNegValue.zero495  shows -realZero = realZero496proof497  have inverse := realAddValue.neg_right with realZero.real498  have negZeroReal := realNegValue.real with realZero.real499  have identity := realAddValue.zero_left with negZeroReal500  rwa identity at inverse501502theorem realNegCut.zero503  shows realNegCut(realZero) = realZero504proof505  have cut := realNegValue.cut with realZero.real506  rw ← cut507  exact realNegValue.zero508509theorem realSubValue.self (A : Real)510  shows A - A = 0511proof512  unfold realSubValue513  exact realAddValue.neg_right with assumption514515theorem realSubValue.zero_right (A : Real)516  shows A - 0 = A517proof518  unfold realSubValue519  rw realNegValue.zero520  exact realAddValue.zero_right with assumption521522theorem realSubValue.zero_left (A : Real)523  shows 0 - A = -A524proof525  unfold realSubValue526  exact realAddValue.zero_left at -A with527    realNegValue.real at A with assumption528529theorem realSubValue.add_cancel_right (A B : Real)530  shows (A + B) - B = A531proof532  unfold realSubValue533  have negBReal := realNegValue.real at B534  calc535    (A + B) + (-B) = A + (B + (-B)) :=536      realAddValue.associative at A, B, -B with537        *{2}, negBReal538    _ = A + 0 := by simp [realAddValue.neg_right]539    _ = A := realAddValue.zero_right at A with assumption540541theorem realSubValue.add_cancel_left (A B : Real)542  shows (A + B) - A = B543proof544  have commutes := realAddValue.commutative at A, B with545    *{2}546  calc547    (A + B) - A = (B + A) - A := by simp [commutes]548    _ = B := realSubValue.add_cancel_right at B, A with549      *{2}550551theorem realLess.iff_pos_sub (A B : Real)552  shows A < B ↔ 0 < B - A553proof554  constructor555  . intro less556    have negAReal := realNegValue.real at A557    have shifted := realLess.add_left at A, B, -A with558      *{2}, negAReal, less559    have leftInverse := realAddValue.neg_left at A560    rw leftInverse at shifted561    have differenceCommutative := realAddValue.commutative at -A, B with562      negAReal, assumption563    rw differenceCommutative at shifted564    unfold realSubValue565    exact shifted566  . intro positive567    have differenceReal := realSubValue.real at B, A with568      *{2}569    have shifted := realLess.add_right at realZero, B - A, A with570      realZero.real, differenceReal, assumption, positive571    have leftIdentity := realAddValue.zero_left at A572    have rightCancel : (B - A) + A = B573      unfold realSubValue574      have negAReal := realNegValue.real at A575      calc576        (B + (-A)) + A = B + ((-A) + A) :=577          realAddValue.associative at B, -A, A with578            assumption, negAReal, assumption579        _ = B + 0 := by simp [realAddValue.neg_left]580        _ = B := realAddValue.zero_right at B with assumption581    rwa [leftIdentity, rightCancel] at shifted582583instance realAdd.strict_mono584  shows AddStrictMono(ℝ, realAdd, realLess)585proof586  intros A realA B realB C realC less587  exact realLess.add_right with less588589theorem realNegValue.type (A : Real)590  shows Real(realNegValue(A))591proof592  have closed := realNegValue.real with *593  unfold realNegValue594  exact closed595