-- Addition of Dedekind real numbers -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.Real.Addition import Embedding -- The lower cut generated by all rational sums a+b with a ∈ A and b ∈ B. -- Writing the strict lower closure into the definition makes downward closure -- and roundedness consequences of the rational order itself. def realAddCut (A B : Set) : Set := { q ∈ ℚ | ∃ a ∈ A, ∃ b ∈ B, relates(rationalLess, q, rationalAdd((a, b))) } -- The real zero is the lower rational cut at zero. Its soft result type lets -- overloaded real notation recognize it, while realZero.real below supplies -- the kernel-checked mathematical certificate. def realZero : Real := rationalCut(rationalZero) theorem realZero.real shows Real(realZero) proof unfold realZero exact rationalCut.real with rationalZero.rational instance realZero.of_nat shows OfNat(ℝ, 0, realZero) proof constructor . typecheck . exact realZero.real -- Public-facing membership avoids exposing the underlying function-graph -- application. The witnesses are still checked against the same definition. theorem realAddCut.membership_value (A B q : Set) shows q ∈ realAddCut(A, B) ↔ (q ∈ ℚ ∧ ∃ a ∈ A, ∃ b ∈ B, q < rationalAddValue(a, b)) proof constructor . intro member obtain ⟨qInQ, a, aInA, b, bInB, less⟩ := realAddCut.membership.forward with member refine ⟨qInQ, a, aInA, b, bInB, _⟩ unfold rationalAddValue exact less . intro data rcases data with ⟨qInQ2, c, cInA, d, dInB, less2⟩ unfold rationalAddValue at less2 exact realAddCut.membership.backward with ⟨qInQ2, c, cInA, d, dInB, less2⟩ theorem realAddCut.subset_rationals (A B : Set) shows (realAddCut(A, B) ⊆ ℚ) proof simp theorem realAddCut.nonempty (A B : Real) shows Nonempty(realAddCut(A, B)) proof have cutA := Real.characterization.forward at A with assumption have cutB := Real.characterization.forward at B with assumption obtain ⟨a, aInA⟩ := DedekindCut.nonempty with cutA obtain ⟨b, bInB⟩ := DedekindCut.nonempty with cutB have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have aInQ := subsetA with a, aInA have bInQ := subsetB with b, bInB have aRational : Rational(a) by exact aInQ have bRational : Rational(b) by exact bInQ have sumRational := rationalAddValue.rational_raw with aRational, bRational obtain ⟨q, qInQ, qLessSum⟩ := rationalLess.exists_below with sumRational witness q apply realAddCut.membership.backward constructor . exact qInQ . witness a constructor . exact aInA . witness b constructor . exact bInB . unfold rationalAddValue at qLessSum exact qLessSum theorem realAddCut.downward (A B p q : Set) requires realA : Real(A) requires realB : Real(B) requires qInSum : q ∈ realAddCut(A, B) requires pInQ : p ∈ ℚ requires pLessQ : relates(rationalLess, p, q) shows p ∈ realAddCut(A, B) proof obtain ⟨qInQ, a, aInA, b, bInB, qLessSum⟩ := realAddCut.membership.forward with qInSum have cutA := Real.characterization.forward with realA have cutB := Real.characterization.forward with realB have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have aRational : Rational(a) unfold Rational exact subsetA with a, aInA have bRational : Rational(b) unfold Rational exact subsetB with b, bInB have transitive := rationalLess.transitive_on have sumInQ := rationalAddValue.rational_raw with aRational, bRational unfold rationalAddValue at sumInQ have pLessSum := transitive with p, pInQ, q, qInQ, rationalAdd((a, b)), sumInQ, pLessQ, qLessSum exact realAddCut.membership.backward with ⟨pInQ, a, aInA, b, bInB, pLessSum⟩ theorem realAddCut.no_greatest (A B q : Set) requires realA : Real(A) requires realB : Real(B) requires qInSum : q ∈ realAddCut(A, B) shows ∃ r ∈ realAddCut(A, B), relates(rationalLess, q, r) proof obtain ⟨qInQ, a, aInA, b, bInB, qLessSum⟩ := realAddCut.membership.forward with qInSum have cutA := Real.characterization.forward with realA have cutB := Real.characterization.forward with realB have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have aRational : Rational(a) unfold Rational exact subsetA with a, aInA have bRational : Rational(b) unfold Rational exact subsetB with b, bInB have sumRational := rationalAddValue.rational_raw with aRational, bRational have qRational : Rational(q) by exact qInQ unfold rationalAddValue at sumRational obtain ⟨r, rInQ, qLessR, rLessSum⟩ := rationalLess.dense with qRational, sumRational, qLessSum witness r constructor . apply realAddCut.membership.backward at A, B, r refine ⟨rInQ, a, aInA, b, bInB, rLessSum⟩ . exact qLessR theorem realAddCut.proper (A B : Real) shows realAddCut(A, B) ≠ ℚ proof have cutA := Real.characterization.forward at A with assumption have cutB := Real.characterization.forward at B with assumption have properA := DedekindCut.proper with cutA have properB := DedekindCut.proper with cutB obtain ⟨u, uInQ, uMissing⟩ := ProperSubset.missing with properA obtain ⟨v, vInQ, vMissing⟩ := ProperSubset.missing with properB have uRational : Rational(u) by exact uInQ have vRational : Rational(v) by exact vInQ have upperRational := rationalAddValue.rational_raw with uRational, vRational intro allRationals have upperInSum : rationalAddValue(u, v) ∈ realAddCut(A, B) rw allRationals exact upperRational obtain ⟨upperInQ, a, aInA, b, bInB, upperLessSum⟩ := realAddCut.membership.forward with upperInSum have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have aRational : Rational(a) unfold Rational exact subsetA with a, aInA have bRational : Rational(b) unfold Rational exact subsetB with b, bInB have aLessU := DedekindCut.lt_missing with cutA, aInA, uInQ, uMissing have bLessV := DedekindCut.lt_missing with cutB, bInB, vInQ, vMissing have first := rationalLess.add_right with aRational, uRational, bRational, aLessU have second := rationalLess.add_left with bRational, vRational, uRational, bLessV rw [rationalAddValue.notation, rationalAddValue.notation] at first rw [rationalAddValue.notation, rationalAddValue.notation] at second have sumRational := rationalAddValue.rational_raw with aRational, bRational have middleRational := rationalAddValue.rational_raw with uRational, bRational have sumInQ := sumRational have middleInQ := middleRational have transitive := rationalLess.transitive_on have sumLessUpper := transitive with rationalAddValue(a, b), sumInQ, rationalAddValue(u, b), middleInQ, rationalAddValue(u, v), upperInQ, first, second unfold rationalAddValue at upperLessSum unfold rationalAddValue at sumLessUpper unfold rationalAddValue at upperInQ unfold rationalAddValue at sumInQ have cycle := transitive with rationalAdd((u, v)), upperInQ, rationalAdd((a, b)), sumInQ, rationalAdd((u, v)), upperInQ, upperLessSum, sumLessUpper have irreflexive := rationalLess.irreflexive_on exact irreflexive with rationalAdd((u, v)), upperInQ, cycle theorem realAddCut.cut (A B : Real) shows DedekindCut(realAddCut(A, B)) proof have subset := realAddCut.subset_rationals at A, B have inhabited := realAddCut.nonempty at A, B with * have proper := realAddCut.proper at A, B with * unfold DedekindCut refine ⟨subset, inhabited, proper, _, _⟩ . intros q qInSum p pInQ pLessQ exact realAddCut.downward with qInSum, pInQ, pLessQ . intros q qInSum exact realAddCut.no_greatest with qInSum theorem realAddCut.real (A B : Real) shows Real(realAddCut(A, B)) proof apply Real.characterization.backward exact realAddCut.cut with * -- Real addition as a set-valued function graph on pairs of cuts. def realAdd : Set := { p ∈ ((ℝ × ℝ) × ℝ) | ∃ A ∈ ℝ, ∃ B ∈ ℝ, p = ((A, B) ↦ realAddCut(A, B)) } def realAddValue (A B : Real) : Real := realAdd((A, B)) theorem realAdd.relates (A B : Real) shows relates(realAdd, (A, B), realAddCut(A, B)) proof have realA : A ∈ ℝ by simp [Real] have realB : B ∈ ℝ by simp [Real] unfold relates apply realAdd.membership.backward constructor . apply product.pair at (A, B), realAddCut(A, B), ℝ × ℝ, ℝ . apply product.pair at A, B, ℝ, ℝ . exact realA . exact realB . exact realAddCut.real at A, B with *{2} . refine ⟨A, realA, B, realB, rfl⟩ theorem realAdd.factors (input output : Set) requires mapped : relates(realAdd, input, output) shows ∃ A ∈ ℝ, ∃ B ∈ ℝ, input = (A, B) ∧ output = realAddCut(A, B) proof unfold relates at mapped simp [realAdd.membership] at mapped rcases mapped with ⟨bounded, A, realA, B, realB, shape⟩ obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape refine ⟨A, realA, B, realB, inputShape, outputShape⟩ theorem realAdd.total shows TotalBetween(realAdd, ℝ × ℝ, ℝ) proof intros input inputInProduct obtain ⟨bounded, A, realA, B, realB, inputShape⟩ := product.membership.forward with inputInProduct have typedA : Real(A) by exact realA have typedB : Real(B) by exact realB witness realAddCut(A, B) constructor . exact realAddCut.real with typedA, typedB . rw inputShape exact realAdd.relates with typedA, typedB theorem realAdd.functional shows Functional(realAdd) proof intros input y inputY z inputZ obtain ⟨A, realA, B, realB, inputFirst, outputFirst⟩ := realAdd.factors with inputY obtain ⟨C, realC, D, realD, inputSecond, outputSecond⟩ := realAdd.factors with inputZ rw inputFirst at inputSecond obtain ⟨sameLeft, sameRight⟩ := orderedPair.injective with inputSecond rw [outputFirst, outputSecond, sameLeft, sameRight] rfl theorem realAdd.function shows realAdd : ℝ × ℝ → ℝ proof constructor intros p hp simp [realAdd.membership] at hp rcases hp with ⟨bounded, witnesses⟩ exact bounded . constructor . exact realAdd.functional . exact realAdd.total instance realAdd.operation shows AddOperation(ℝ, realAdd) proof exact realAdd.function notation infixl 60 "+" => call2 via AddOperation(ℝ, _) for Real notation numeral "0" via OfNat(ℝ, 0, _) for Real theorem realAddValue.real (A B : Real) shows Real(A + B) proof have realA : A ∈ ℝ by simp [Real] have realB : B ∈ ℝ by simp [Real] have input := product.pair with realA, realB obtain ⟨C, realC, mapped⟩ := FunctionBetween.exists_value with realAdd.function, input have applied := FunctionBetween.apply_value with realAdd.function, input, mapped unfold call2 rw applied exact realC theorem realAddValue.cut (A B : Real) shows A + B = realAddCut(A, B) proof have realA : A ∈ ℝ by simp [Real] have realB : B ∈ ℝ by simp [Real] have input := product.pair with realA, realB have mapped := realAdd.relates at A, B with * unfold call2 exact FunctionBetween.apply_value with realAdd.function, input, mapped theorem realAddCut.commutative (A B : Real) shows realAddCut(A, B) = realAddCut(B, A) proof ext q constructor . intro qInSum obtain ⟨qInQ, a, aInA, b, bInB, qLessSum⟩ := realAddCut.membership.forward with qInSum have cutA := Real.characterization.forward at A with assumption have cutB := Real.characterization.forward at B with assumption have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have aRational : Rational(a) unfold Rational exact subsetA with a, aInA have bRational : Rational(b) unfold Rational exact subsetB with b, bInB have sumComm := rationalAddValue.commutative with aRational, bRational unfold call2 at sumComm rw sumComm at qLessSum exact realAddCut.membership.backward with ⟨qInQ, b, bInB, a, aInA, qLessSum⟩ . intro qInSum obtain ⟨qInQ2, b2, b2InB, a2, a2InA, qLessSum2⟩ := realAddCut.membership.forward with qInSum have cutA := Real.characterization.forward at A with assumption have cutB := Real.characterization.forward at B with assumption have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have a2Rational : Rational(a2) unfold Rational exact subsetA with a2, a2InA have b2Rational : Rational(b2) unfold Rational exact subsetB with b2, b2InB have sumComm2 := rationalAddValue.commutative with b2Rational, a2Rational unfold call2 at sumComm2 rw sumComm2 at qLessSum2 exact realAddCut.membership.backward with ⟨qInQ2, a2, a2InA, b2, b2InB, qLessSum2⟩ theorem realAddCut.zero_right (A : Real) shows realAddCut(A, realZero) = A proof ext q constructor . intro qInSum obtain ⟨qInQ, a, aInA, b, bInZero, qLessSum⟩ := realAddCut.membership.forward with qInSum unfold realZero at bInZero simp [rationalCut.membership] at bInZero rcases bInZero with ⟨bInQ, bLessZero⟩ have cutA := Real.characterization.forward with assumption have subsetA := DedekindCut.subset_rationals with cutA have aInQ := subsetA with a, aInA have aRational : Rational(a) by exact aInQ have bRational : Rational(b) by exact bInQ have shifted := rationalLess.add_left with bRational, rationalZero.rational, aRational, bLessZero have identity := rationalAddValue.zero_right with aRational rw identity at shifted have sumRational := rationalAddValue.rational_raw with aRational, bRational have sumInQ := sumRational unfold rationalAddValue at sumInQ unfold call2 at shifted have transitive := rationalLess.transitive_on have qLessA := transitive with q, qInQ, rationalAdd((a, b)), sumInQ, a, aInQ, qLessSum, shifted exact DedekindCut.downward with cutA, aInA, qInQ, qLessA . intro qInA have cutA := Real.characterization.forward with assumption have subsetA := DedekindCut.subset_rationals with cutA have qInQ := subsetA with q, qInA obtain ⟨r, rInA, qLessR⟩ := DedekindCut.no_greatest with cutA, qInA have rInQ := subsetA with r, rInA have rRational : Rational(r) by exact rInQ obtain ⟨s, sInQ, qLessS, sLessR⟩ := rationalLess.dense with qLessR have sRational : Rational(s) by typecheck have differenceRational := rationalSubValue.rational with sRational, rRational have differenceNegative := rationalLess.sub_self_negative with sLessR have differenceInZero : s - r ∈ realZero unfold realZero simp [rationalCut.membership] constructor exact differenceRational . exact differenceNegative have sumShape := rationalAddValue.add_sub_cancel_left with rRational, sRational rw ← sumShape at qLessS unfold call2 at qLessS exact realAddCut.membership.backward with ⟨qInQ, r, rInA, s - r, differenceInZero, qLessS⟩ theorem realAddCut.zero_left (A : Real) shows realAddCut(realZero, A) = A proof calc realAddCut(realZero, A) = realAddCut(A, realZero) := realAddCut.commutative with realZero.real _ = A := realAddCut.zero_right at A with assumption -- Associativity is proved at the level of cuts. Density supplies an inner -- witness close enough to the desired rational sum; no representative of a -- real number or algebraic axiom is hidden in the argument. theorem realAddCut.associative (A B C : Real) shows realAddCut(realAddCut(A, B), C) = realAddCut(A, realAddCut(B, C)) proof ext q constructor . intro qInLeft obtain ⟨qInQ, x, xInAB, c, cInC, qLessXC⟩ := realAddCut.membership_value.forward with qInLeft obtain ⟨xInQ, a, aInA, b, bInB, xLessAB⟩ := realAddCut.membership_value.forward with xInAB rw ← rationalAddValue.notation at qLessXC rw ← rationalAddValue.notation at xLessAB have cutA := Real.characterization.forward at A with assumption have cutB := Real.characterization.forward at B with assumption have cutC := Real.characterization.forward at C with assumption have subsetA := DedekindCut.subset_rationals with cutA have subsetB := DedekindCut.subset_rationals with cutB have subsetC := DedekindCut.subset_rationals with cutC have qRational : Rational(q) by exact qInQ have xRational : Rational(x) by exact xInQ have aRational : Rational(a) unfold Rational exact subsetA with a, aInA have bRational : Rational(b) unfold Rational exact subsetB with b, bInB have cRational : Rational(c) unfold Rational exact subsetC with c, cInC have abRational := rationalAddValue.rational with aRational, bRational have bcRational := rationalAddValue.rational with bRational, cRational have scaled := rationalLess.add_right with xRational, abRational, cRational, xLessAB have qLessABC := rationalLess.transitive with qLessXC, scaled rw rationalAddValue.associative at qLessABC have differenceLess := rationalLess.sub_left with qLessABC have differenceRational := rationalSubValue.rational with qRational, aRational obtain ⟨y, yInQ, differenceLessY, yLessBC⟩ := rationalLess.dense with differenceRational, bcRational, differenceLess have yInBC : y ∈ realAddCut(B, C) apply realAddCut.membership_value.backward rw rationalAddValue.notation at yLessBC refine ⟨yInQ, b, bInB, c, cInC, yLessBC⟩ have qLessAY := rationalLess.add_left_of_sub_left with differenceLessY apply realAddCut.membership_value.backward rw rationalAddValue.notation at qLessAY refine ⟨qInQ, a, aInA, y, yInBC, qLessAY⟩ . intro qInRight obtain ⟨qInQ2, a2, a2InA, y2, y2InBC, qLessAY2⟩ := realAddCut.membership_value.forward with qInRight obtain ⟨y2InQ, b2, b2InB, c2, c2InC, y2LessBC⟩ := realAddCut.membership_value.forward with y2InBC rw ← rationalAddValue.notation at qLessAY2 rw ← rationalAddValue.notation at y2LessBC have cutA2 := Real.characterization.forward at A with assumption have cutB2 := Real.characterization.forward at B with assumption have cutC2 := Real.characterization.forward at C with assumption have subsetA2 := DedekindCut.subset_rationals with cutA2 have subsetB2 := DedekindCut.subset_rationals with cutB2 have subsetC2 := DedekindCut.subset_rationals with cutC2 have qRational2 : Rational(q) by exact qInQ2 have a2Rational : Rational(a2) unfold Rational exact subsetA2 with a2, a2InA have y2Rational : Rational(y2) by exact y2InQ have b2Rational : Rational(b2) unfold Rational exact subsetB2 with b2, b2InB have c2Rational : Rational(c2) unfold Rational exact subsetC2 with c2, c2InC have a2b2Rational := rationalAddValue.rational with a2Rational, b2Rational have b2c2Rational := rationalAddValue.rational with b2Rational, c2Rational have scaled2 := rationalLess.add_left with y2Rational, b2c2Rational, a2Rational, y2LessBC have qLessABC2 := rationalLess.transitive with qLessAY2, scaled2 rw ← rationalAddValue.associative at qLessABC2 have outerCommutative2 := rationalAddValue.commutative with a2b2Rational, c2Rational rw outerCommutative2 at qLessABC2 have differenceLess2 := rationalLess.sub_left with qLessABC2 have differenceRational2 := rationalSubValue.rational with qRational2, c2Rational obtain ⟨x2, x2InQ, differenceLessX2, x2LessAB⟩ := rationalLess.dense with differenceRational2, a2b2Rational, differenceLess2 have x2Rational : Rational(x2) by typecheck have x2InAB : x2 ∈ realAddCut(A, B) apply realAddCut.membership_value.backward rw rationalAddValue.notation at x2LessAB refine ⟨x2InQ, a2, a2InA, b2, b2InB, x2LessAB⟩ have qLessCX2 := rationalLess.add_left_of_sub_left with qRational2, c2Rational, x2Rational, differenceLessX2 have innerCommutative2 := rationalAddValue.commutative with c2Rational, x2Rational rw innerCommutative2 at qLessCX2 apply realAddCut.membership_value.backward rw rationalAddValue.notation at qLessCX2 refine ⟨qInQ2, x2, x2InAB, c2, c2InC, qLessCX2⟩ theorem realAddValue.commutative (A B : Real) shows A + B = B + A proof calc A + B = realAddCut(A, B) := realAddValue.cut with *{2} _ = realAddCut(B, A) := realAddCut.commutative with *{2} _ = B + A := by simp [realAddValue.cut] theorem realAddValue.zero_right (A : Real) shows A + 0 = A proof calc A + realZero = realAddCut(A, realZero) := realAddValue.cut with realZero.real _ = A := realAddCut.zero_right at A with assumption theorem realAddValue.zero_left (A : Real) shows 0 + A = A proof calc realZero + A = A + realZero := realAddValue.commutative with realZero.real _ = A := realAddValue.zero_right at A with assumption theorem realAddValue.associative (A B C : Real) shows (A + B) + C = A + (B + C) proof calc (A + B) + C = realAddCut(realAddCut(A, B), C) := by simp [realAddValue.cut] _ = realAddCut(A, realAddCut(B, C)) := realAddCut.associative with *{3} _ = A + (B + C) := by simp [realAddValue.cut] -- The first bundled algebraic structure on the Dedekind reals. It is a -- checked theorem that elaboration registers as an instance. instance realAdd.comm_monoid shows IsCommMonoid(ℝ, realAdd, realZero) proof constructor constructor constructor exact realAdd.function intros A realA B realB C realC have typedA : Real(A) by exact realA have typedB : Real(B) by exact realB have typedC : Real(C) by exact realC exact realAddValue.associative with typedA, typedB, typedC constructor . exact realZero.real . intros A realA have typedA : Real(A) by exact realA constructor . exact realAddValue.zero_left with typedA . exact realAddValue.zero_right with typedA intros A realA B realB have typedA : Real(A) by exact realA have typedB : Real(B) by exact realB exact realAddValue.commutative with typedA, typedB theorem realAddValue.type (A B : Real) shows Real(realAddValue(A, B)) proof have closed := realAddValue.real at A, B with * unfold realAddValue unfold call2 at closed exact closed