Grace/Cumulus/Real/Multiplication.g17

Open in Workbench Download source

Imports

Negation

Declarations

Source

1-- Multiplication of nonnegative 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.Multiplication8import Negation910-- The multiplicative unit is the rational cut at one, with its11-- overloaded numeral available as soon as the real carrier is known.12def realOne : Real := rationalCut(rationalOne)1314theorem realOne.real15  shows Real(realOne)16proof17  unfold realOne18  exact rationalCut.real with rationalOne.rational1920instance realOne.of_nat21  shows OfNat(ℝ, 1, realOne)22proof23  constructor24  . typecheck25  . exact realOne.real2627notation numeral "1" via OfNat(ℝ, 1, _) for Real2829theorem realZero.lt_one30  shows 0 < realOne31proof32  have rationalPositive := rationalLess.positive_natural_successor with Naturals.constructor.zero33  have zeroLessOne : rationalZero < rationalOne by simpa [rationalOne] using rationalPositive34  have strict := rationalCut.strict_mono with rationalZero.rational, rationalOne.rational, zeroLessOne35  apply realLess.characterization.backward36  unfold realZero37  unfold realOne38  exact strict3940theorem realZero.ne_one41  shows realZero ≠ realOne42proof43  intro equal44  have positive := realZero.lt_one45  rw equal at positive46  have impossible := realLess.irreflexive_on47  exact impossible with realOne, positive4849-- For nonnegative cuts A and B, their product contains every negative50-- rational and every rational strictly below a product of positive members.51-- The explicit rational bounds on a and b make all arithmetic notation52-- independently readable and resolvable.53def realPosMulCut (A B : Set) : Set :=54  { q ∈ ℚ |55    q < rationalZero ∨56    ∃ a ∈ ℚ, a ∈ A ∧ ∃ b ∈ ℚ, b ∈ B ∧57      rationalZero < a ∧ rationalZero < b ∧ q < a * b }5859-- Every cut omits a positive rational.  Starting from any omitted rational,60-- move above it to the next displayed natural; downward closure shows that61-- this larger rational remains outside the cut.62theorem DedekindCut.exists_positive_upper (A : Set)63  requires cut : DedekindCut(A)64  shows ∃ u ∈ ℚ, rationalZero < u ∧ ¬(u ∈ A)65proof66  have proper := DedekindCut.proper with cut67  obtain ⟨r, rInQ, rMissing⟩ := ProperSubset.missing with proper68  have rRational : Rational(r) by typecheck69  obtain ⟨n, nNatural, rBelowN⟩ := Rational.below_natural with rRational70  have oneNonzero : 1 ≠ 071    intro oneZero72    arith73  have nRational := rationalClass.rational at n, 0, 1 with oneNonzero74  have nBelowSucc := rationalLess.natural_successor with nNatural75  have uRational := rationalClass.rational at succ(n), 0, 1 with oneNonzero76  have rBelowU : r < rationalClass(succ(n), 0, 1)77    calc78      r < rationalClass(n, 0, 1) := rBelowN79      _ < rationalClass(succ(n), 0, 1) := nBelowSucc80  witness rationalClass(succ(n), 0, 1)81  constructor82    exact uRational83  constructor84  . exact rationalLess.positive_natural_successor at n with nNatural85  . intro uInA86    have rInA := DedekindCut.downward with cut, uInA, rInQ, rBelowU87    exact rMissing with rInA8889theorem realPosMulCut.subset_rationals (A B : Set)90  shows realPosMulCut(A, B) ⊆ ℚ91proof92  simp9394theorem realPosMulCut.nonempty (A B : Set)95  shows Nonempty(realPosMulCut(A, B))96proof97  obtain ⟨q, qInQ, qNegative⟩ := rationalLess.exists_below with rationalZero.rational98  witness q99  apply realPosMulCut.membership.backward100  refine ⟨qInQ, _⟩101  left102  exact qNegative103104theorem realPosMulCut.nonnegative (A B : Set)105  shows realZero ⊆ realPosMulCut(A, B)106proof107  intros q qInZero108  unfold realZero at qInZero109  obtain ⟨qInQ, qNegative⟩ := rationalCut.membership.forward with qInZero110  apply realPosMulCut.membership.backward111  refine ⟨qInQ, _⟩112  left113  exact qNegative114115theorem realPosMulCut.downward (A B p q : Set)116  requires qInProduct : q ∈ realPosMulCut(A, B)117  requires pInQ : p ∈ ℚ118  requires pLessQ : relates(rationalLess, p, q)119  shows p ∈ realPosMulCut(A, B)120proof121  obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct122  cases rest with negative | product123  . have pNegative := rationalLess.transitive at p, q, rationalZero with124      pLessQ, negative125    apply realPosMulCut.membership.backward126    refine ⟨pInQ, _⟩127    left128    exact pNegative129  . rcases product with130      ⟨a, aInQ, aInA, b, bInQ, bInB, positiveA, positiveB, qLessProduct⟩131    have pLessProduct := rationalLess.transitive with pLessQ, qLessProduct132    apply realPosMulCut.membership.backward133    refine ⟨pInQ, _⟩134    right135    refine ⟨a, aInQ, aInA, b, bInQ, bInB,136      positiveA, positiveB, pLessProduct⟩137138theorem realPosMulCut.no_greatest (A B q : Set)139  requires qInProduct : q ∈ realPosMulCut(A, B)140  shows ∃ s ∈ realPosMulCut(A, B), relates(rationalLess, q, s)141proof142  obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct143  have qRational : Rational(q) by typecheck144  cases rest with negative | product145  . obtain ⟨t, tInQ, qLessT, tNegative⟩ :=146      rationalLess.dense at q, rationalZero with147        qRational, rationalZero.rational, negative148    refine ⟨t, _, qLessT⟩149    apply realPosMulCut.membership.backward150    refine ⟨tInQ, _⟩151    left152    exact tNegative153  . rcases product with154      ⟨a, aInQ, aInA, b, bInQ, bInB, positiveA, positiveB, qLessProduct⟩155    obtain ⟨s2, s2InQ, qLessS2, s2LessProduct⟩ := rationalLess.dense with qLessProduct156    refine ⟨s2, _, qLessS2⟩157    apply realPosMulCut.membership.backward158    refine ⟨s2InQ, _⟩159    right160    refine ⟨a, aInQ, aInA, b, bInQ, bInB,161      positiveA, positiveB, s2LessProduct⟩162163theorem realPosMulCut.proper (A B : Real)164  shows realPosMulCut(A, B) ≠ ℚ165proof166  have cutA := Real.characterization.forward at A with assumption167  have cutB := Real.characterization.forward at B with assumption168  obtain ⟨u, uInQ, positiveU, uMissing⟩ := DedekindCut.exists_positive_upper with cutA169  obtain ⟨v, vInQ, positiveV, vMissing⟩ := DedekindCut.exists_positive_upper with cutB170  have uRational : Rational(u) by typecheck171  have vRational : Rational(v) by typecheck172  have uvRational := rationalMulValue.rational with uRational, vRational173  have positiveUV := rationalLess.mul_positive with positiveU, positiveV174  intro allRationals175  have uvInProduct : u * v ∈ realPosMulCut(A, B)176    rw allRationals177    exact uvRational178  obtain ⟨uvInQ, rest⟩ := realPosMulCut.membership.forward with uvInProduct179  cases rest with negative | product180  . have cycle := rationalLess.transitive at181      rationalZero, u * v, rationalZero with positiveUV, negative182    have impossible := rationalLess.irreflexive_on183    exact impossible with rationalZero, cycle184  . rcases product with185      ⟨a, aInQ, aInA, b, bInQ, bInB, positiveA, positiveB, uvLessAB⟩186    have aLessU := DedekindCut.lt_missing with cutA, aInA, uInQ, uMissing187    have bLessV := DedekindCut.lt_missing with cutB, bInB, vInQ, vMissing188    have abLessUB := rationalLess.mul_right with positiveB, aLessU189    have ubLessUV := rationalLess.mul_left with positiveU, bLessV190    have abLessUV : a * b < u * v191      calc192        a * b < u * b := abLessUB193        _ < u * v := ubLessUV194    have cycle : u * v < u * v195      calc196        u * v < a * b := uvLessAB197        _ < u * v := abLessUV198    have impossible := rationalLess.irreflexive_on199    exact impossible with u * v, uvInQ, cycle200201theorem realPosMulCut.cut (A B : Real)202  shows DedekindCut(realPosMulCut(A, B))203proof204  have subset := realPosMulCut.subset_rationals at A, B205  have inhabited := realPosMulCut.nonempty at A, B206  have proper := realPosMulCut.proper at A, B with *207  unfold DedekindCut208  refine ⟨subset, inhabited, proper, _, _⟩209  . intros q qInProduct p pInQ pLessQ210    exact realPosMulCut.downward with qInProduct, pInQ, pLessQ211  . intros q qInProduct212    exact realPosMulCut.no_greatest with qInProduct213214theorem realPosMulCut.real (A B : Real)215  shows Real(realPosMulCut(A, B))216proof217  apply Real.characterization.backward218  exact realPosMulCut.cut with *219220theorem realPosMulCut.commutative (A B : Real)221  shows realPosMulCut(A, B) = realPosMulCut(B, A)222proof223  ext q224  constructor225  . intro qInProduct226    obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct227    cases rest with negative | product228    . apply realPosMulCut.membership.backward at B, A, q229      refine ⟨qInQ, _⟩230      left231      exact negative232    . rcases product with233        ⟨a, aInQ, aInA, b, bInQ, bInB, positiveA, positiveB, below⟩234      have aRational : Rational(a) by typecheck235      have bRational : Rational(b) by typecheck236      have commutative := rationalMulValue.commutative with aRational, bRational237      rw commutative at below238      apply realPosMulCut.membership.backward239      refine ⟨qInQ, _⟩240      right241      refine ⟨b, bInQ, bInB, a, aInQ, aInA,242        positiveB, positiveA, below⟩243  . intro qInProduct244    obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct245    cases rest with negative | product246    . apply realPosMulCut.membership.backward at A, B, q247      refine ⟨qInQ, _⟩248      left249      exact negative250    . rcases product with251        ⟨b2, b2InQ, b2InB, a2, a2InQ, a2InA, positiveB2, positiveA2, below2⟩252      have a2Rational : Rational(a2) by typecheck253      have b2Rational : Rational(b2) by typecheck254      have commutative2 := rationalMulValue.commutative with b2Rational, a2Rational255      rw commutative2 at below2256      apply realPosMulCut.membership.backward257      refine ⟨qInQ, _⟩258      right259      refine ⟨a2, a2InQ, a2InA, b2, b2InQ, b2InB,260        positiveA2, positiveB2, below2⟩261262-- The one-sided associativity argument records the only approximation needed263-- for open products. A boundary product b*c is moved slightly inward by a264-- positive factor t<1; rational associativity preserves the outer bound.265theorem realPosMulCut.assoc_subset (A B C : Real)266  shows realPosMulCut(realPosMulCut(A, B), C) ⊆267    realPosMulCut(A, realPosMulCut(B, C))268proof269  intros q qInLeft270  obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInLeft271  apply realPosMulCut.membership.backward272  refine ⟨qInQ, _⟩273  cases rest with qNegative | product274  . left275    exact qNegative276  . rcases product with277      ⟨x, xInQ, xInAB, c, cInQ, cInC, positiveX, positiveC, qBelowXC⟩278    have cRational : Rational(c) by typecheck279    obtain ⟨xInQAgain, innerRest⟩ := realPosMulCut.membership.forward with xInAB280    cases innerRest with xNegative | factors281    . have cycle := rationalLess.transitive at282        rationalZero, x, rationalZero with positiveX, xNegative283      have impossible := rationalLess.irreflexive_on284      exfalso285      exact impossible with rationalZero, cycle286    . rcases factors with287        ⟨a, aInQ, aInA, b, bInQ, bInB,288          positiveA, positiveB, xBelowAB⟩289      have aRational : Rational(a) by typecheck290      have bRational : Rational(b) by typecheck291      have bcRational := rationalMulValue.rational with bRational, cRational292      have abcRational := rationalMulValue.rational with aRational, bcRational293      have positiveBC := rationalLess.mul_positive with positiveB, positiveC294      have positiveABC := rationalLess.mul_positive with positiveA, positiveBC295      have scaledX := rationalLess.mul_right with positiveC, xBelowAB296      have qBelowGrouped : q < (a * b) * c297        calc298          q < x * c := qBelowXC299          _ < (a * b) * c := scaledX300      have associative := rationalMulValue.associative with aRational, bRational, cRational301      have qBelowABC : q < a * (b * c) by rwa ← associative302      obtain ⟨t, tInQ, positiveT, tBelowOne, qBelowScaled⟩ :=303        rationalLess.exists_scale_below_one at q, a * (b * c) with304          abcRational, positiveABC, qBelowABC305      have tRational : Rational(t) by typecheck306      have yRational := rationalMulValue.rational with bcRational, tRational307      have positiveY := rationalLess.mul_positive with positiveBC, positiveT308      have yBelowOneScaled := rationalLess.mul_left with positiveBC, tBelowOne309      have oneProduct := rationalMulValue.one_right with bcRational310      rw oneProduct at yBelowOneScaled311      have scaledAssociative := rationalMulValue.associative with aRational, bcRational, tRational312      rw scaledAssociative at qBelowScaled313      have yInBC : (b * c) * t ∈ realPosMulCut(B, C)314        apply realPosMulCut.membership.backward315        refine ⟨yRational, _⟩316        right317        refine ⟨b, bInQ, bInB, c, cInQ, cInC,318          positiveB, positiveC, yBelowOneScaled⟩319      right320      refine ⟨a, aInQ, aInA, (b * c) * t, yRational, yInBC,321        positiveA, positiveY, qBelowScaled⟩322323theorem realPosMulCut.associative (A B C : Real)324  shows realPosMulCut(realPosMulCut(A, B), C) =325    realPosMulCut(A, realPosMulCut(B, C))326proof327  apply Subset.antisymmetric328  . exact realPosMulCut.assoc_subset at A, B, C with329      *{3}330  . have reverse := realPosMulCut.assoc_subset at C, B, A with331      *{3}332    have cb := realPosMulCut.commutative at C, B with *333    have ba := realPosMulCut.commutative at B, A with *334    rw [cb, ba] at reverse335    have bcReal := realPosMulCut.real at B, C with *336    have abReal := realPosMulCut.real at A, B with *337    have outerLeft := realPosMulCut.commutative at338      realPosMulCut(B, C), A with bcReal, assumption339    have outerRight := realPosMulCut.commutative at340      C, realPosMulCut(A, B) with assumption, abReal341    rwa [outerLeft, outerRight] at reverse342343theorem realPosMulCut.zero_left (B : Real)344  shows realPosMulCut(realZero, B) = realZero345proof346  ext q347  constructor348  . intro qInProduct349    obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct350    cases rest with negative | product351    . unfold realZero352      apply rationalCut.membership.backward353      constructor354      . exact qInQ355      . exact negative356    . rcases product with357        ⟨a, aInQ, aInZero, b, bInQ, bInB, positiveA, positiveB, below⟩358      unfold realZero at aInZero359      obtain ⟨aAgain, negativeA⟩ := rationalCut.membership.forward with aInZero360      have cycle : rationalZero < rationalZero361        calc362          rationalZero < a := positiveA363          _ < rationalZero := negativeA364      have impossible := rationalLess.irreflexive_on365      exfalso366      exact impossible with rationalZero, cycle367  . intro qInZero368    unfold realZero at qInZero369    obtain ⟨qInQ, negative⟩ := rationalCut.membership.forward with qInZero370    apply realPosMulCut.membership.backward371    refine ⟨qInQ, _⟩372    left373    exact negative374375theorem realPosMulCut.zero_right (A : Real)376  shows realPosMulCut(A, realZero) = realZero377proof378  calc379    realPosMulCut(A, realZero) = realPosMulCut(realZero, A) :=380      realPosMulCut.commutative with realZero.real381    _ = realZero := realPosMulCut.zero_left at A with assumption382383-- The positive-cut product has the expected right unit on nonnegative cuts.384-- The reverse inclusion is the open-cut step: after moving from q to a larger385-- positive member a, rational approximation chooses 0 < b < 1 with q < a*b.386theorem realPosMulCut.one_right (A : Real)387  requires nonnegative : realZero ⊆ A388  shows realPosMulCut(A, realOne) = A389proof390  have cutA := Real.characterization.forward with assumption391  have subsetA := DedekindCut.subset_rationals with cutA392  ext q393  constructor394  . intro qInProduct395    obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct396    cases rest with negative | product397      apply nonnegative with q398      unfold realZero399      exact rationalCut.membership.backward with ⟨qInQ, negative⟩400    . rcases product with401        ⟨a, aInQ, aInA, b, bInQ, bInOne,402          positiveA, positiveB, qBelowProduct⟩403      have aRational : Rational(a) by typecheck404      unfold realOne at bInOne405      obtain ⟨bAgain, bBelowOne⟩ := rationalCut.membership.forward with bInOne406      have scaled := rationalLess.mul_left with positiveA, bBelowOne407      have oneProduct := rationalMulValue.one_right with aRational408      rw oneProduct at scaled409      have qBelowA := rationalLess.transitive with qBelowProduct, scaled410      exact DedekindCut.downward with cutA, aInA, qInQ, qBelowA411  . intro qInA412    by_contra qMissingProduct413    have qInQ := subsetA with q, qInA414    have qRational : Rational(q) by typecheck415    obtain ⟨c, cInA, qBelowC⟩ := DedekindCut.no_greatest with cutA, qInA416    have cInQ := subsetA with c, cInA417    have cRational : Rational(c) by typecheck418    have distinct : rationalZero ≠ c419      intro zeroC420      have qNegative := qBelowC421      rw ← zeroC at qNegative422      apply qMissingProduct423      apply realPosMulCut.membership.backward424      refine ⟨qInQ, _⟩425      left426      exact qNegative427    have connected := rationalLess.connected_on428    have zeroInQ := rationalZero.rational429    have comparison := connected with430      rationalZero, zeroInQ, c, cInQ, distinct431    cases comparison with positiveC | cNegative432    . obtain ⟨d, dInQ, positiveD, dBelowOne, qBelowProduct⟩ :=433        rationalLess.exists_scale_below_one at q, c with434          qRational, cRational, positiveC, qBelowC435      have dInOne : d ∈ realOne436        unfold realOne437        exact rationalCut.membership.backward with ⟨dInQ, dBelowOne⟩438      apply qMissingProduct439      apply realPosMulCut.membership.backward440      refine ⟨qInQ, _⟩441      right442      refine ⟨c, cInQ, cInA, d, dInQ, dInOne,443        positiveC, positiveD, qBelowProduct⟩444    . have qNegative := rationalLess.transitive at445        q, c, rationalZero with qBelowC, cNegative446      apply qMissingProduct447      apply realPosMulCut.membership.backward448      refine ⟨qInQ, _⟩449      left450      exact qNegative451452theorem realPosMulCut.one_left (A : Real)453  requires nonnegative : realZero ⊆ A454  shows realPosMulCut(realOne, A) = A455proof456  calc457    realPosMulCut(realOne, A) = realPosMulCut(A, realOne) :=458      realPosMulCut.commutative with realOne.real459    _ = A := realPosMulCut.one_right at A with nonnegative460461-- The positive and negative parts are joins with zero.  This definition is462-- canonical for lower cuts and avoids making multiplication depend on an463-- arbitrary sign-case presentation.464def realPositivePart (A : Set) : Set := A ∪ realZero465466theorem realPositivePart.real (A : Real)467  shows Real(realPositivePart(A))468proof469  have cutA := Real.characterization.forward with assumption470  have cutZero := Real.characterization.forward with realZero.real471  have comparable := DedekindCut.comparable with cutA, cutZero472  cases comparable with subsetAZero | subsetZeroA473  . have unionSubset := union2.subset at A, realZero, realZero with474      subsetAZero, Subset.reflexive at realZero475    have zeroSubset := union2.subset_right at A, realZero476    have equal := Subset.antisymmetric with unionSubset, zeroSubset477    unfold realPositivePart478    rw equal479    exact realZero.real480  . have unionSubset := union2.subset at A, realZero, A with481      Subset.reflexive at A, subsetZeroA482    have aSubset := union2.subset_left at A, realZero483    have equal := Subset.antisymmetric with unionSubset, aSubset484    unfold realPositivePart485    rwa equal486487theorem realPositivePart.zero488  shows realPositivePart(realZero) = realZero489proof490  unfold realPositivePart491  exact union2.idempotent492493theorem realPositivePart.eq_of_nonnegative (A : Real)494  requires nonnegative : realZero ⊆ A495  shows realPositivePart(A) = A496proof497  unfold realPositivePart498  have unionSubset := union2.subset at A, realZero, A with499    Subset.reflexive at A, nonnegative500  have leftSubset := union2.subset_left at A, realZero501  exact Subset.antisymmetric with unionSubset, leftSubset502503theorem realPositivePart.nonnegative (A : Set)504  shows realZero ⊆ realPositivePart(A)505proof506  unfold realPositivePart507  exact union2.subset_right508509theorem realPositivePart.eq_zero_of_nonpositive (A : Real)510  requires nonpositive : A ⊆ realZero511  shows realPositivePart(A) = realZero512proof513  unfold realPositivePart514  have unionSubset := union2.subset at A, realZero, realZero with515    nonpositive, Subset.reflexive at realZero516  have zeroSubset := union2.subset_right at A, realZero517  exact Subset.antisymmetric with unionSubset, zeroSubset518519def realNegativePart (A : Set) : Set := realPositivePart(realNegCut(A))520521theorem realNegativePart.real (A : Real)522  shows Real(realNegativePart(A))523proof524  unfold realNegativePart525  have negative := realNegCut.real at A526  exact realPositivePart.real with negative527528theorem realNegativePart.zero529  shows realNegativePart(realZero) = realZero530proof531  unfold realNegativePart532  rw realNegCut.zero533  exact realPositivePart.zero534535theorem realNegativePart.eq_zero_of_nonnegative (A : Real)536  requires nonnegative : realZero ⊆ A537  shows realNegativePart(A) = realZero538proof539  have reversed := realNegCut.subset_reverse with realZero.real, nonnegative540  rw realNegCut.zero at reversed541  unfold realNegativePart542  unfold realPositivePart543  have unionSubset := union2.subset at realNegCut(A), realZero, realZero with544    reversed, Subset.reflexive at realZero545  have zeroSubset := union2.subset_right at realNegCut(A), realZero546  exact Subset.antisymmetric with unionSubset, zeroSubset547548theorem realNegativePart.nonnegative (A : Set)549  shows realZero ⊆ realNegativePart(A)550proof551  unfold realNegativePart552  exact realPositivePart.nonnegative553554theorem realNegativePart.eq_neg_of_nonpositive (A : Real)555  requires nonpositive : A ⊆ realZero556  shows realNegativePart(A) = realNegCut(A)557proof558  have reversed := realNegCut.subset_reverse at A, realZero with559    assumption, realZero.real, nonpositive560  rw realNegCut.zero at reversed561  unfold realNegativePart562  exact realPositivePart.eq_of_nonnegative with reversed563564-- Every real is its positive part minus its negative part.  Comparable cuts565-- make this the two-case sign argument, but the resulting identity566-- is canonical and can be used without further case splits.567theorem realParts.decomposition (A : Real)568  shows realAddCut(realPositivePart(A), realNegCut(realNegativePart(A))) = A569proof570  have cutA := Real.characterization.forward with assumption571  have cutZero := Real.characterization.forward with realZero.real572  have comparable := DedekindCut.comparable with cutA, cutZero573  cases comparable with nonpositive | nonnegative574  . have positive := realPositivePart.eq_zero_of_nonpositive with nonpositive575    have negative := realNegativePart.eq_neg_of_nonpositive with nonpositive576    simp [positive, negative, realNegCut.involutive,577      realAddCut.zero_left]578  . have positive := realPositivePart.eq_of_nonnegative with nonnegative579    have negative := realNegativePart.eq_zero_of_nonnegative with nonnegative580    simp [positive, negative, realNegCut.zero, realAddCut.zero_right]581582-- Canonical signed product: A⁺B⁺ + A⁻B⁻ - A⁺B⁻ - A⁻B⁺.  It is expressed583-- entirely through already checked cut constructors, so totality is immediate584-- and later ring laws can reason algebraically instead of splitting on signs.585def realMulCut (A B : Set) : Set :=586  realAddCut(587    realAddCut(588      realPosMulCut(realPositivePart(A), realPositivePart(B)),589      realPosMulCut(realNegativePart(A), realNegativePart(B))),590    realNegCut(591      realAddCut(592        realPosMulCut(realPositivePart(A), realNegativePart(B)),593        realPosMulCut(realNegativePart(A), realPositivePart(B)))))594595theorem realMulCut.real (A B : Real)596  shows Real(realMulCut(A, B))597proof598  have positiveA := realPositivePart.real at A599  have positiveB := realPositivePart.real at B600  have negativeA := realNegativePart.real at A601  have negativeB := realNegativePart.real at B602  have pp := realPosMulCut.real with positiveA, positiveB603  have nn := realPosMulCut.real with negativeA, negativeB604  have pn := realPosMulCut.real with positiveA, negativeB605  have np := realPosMulCut.real with negativeA, positiveB606  have positiveSum := realAddCut.real with pp, nn607  have negativeSum := realAddCut.real with pn, np608  have negatedNegativeSum := realNegCut.real at609    realAddCut(610      realPosMulCut(realPositivePart(A), realNegativePart(B)),611      realPosMulCut(realNegativePart(A), realPositivePart(B))) with negativeSum612  unfold realMulCut613  exact realAddCut.real at614    realAddCut(615      realPosMulCut(realPositivePart(A), realPositivePart(B)),616      realPosMulCut(realNegativePart(A), realNegativePart(B))),617    realNegCut(618      realAddCut(619        realPosMulCut(realPositivePart(A), realNegativePart(B)),620        realPosMulCut(realNegativePart(A), realPositivePart(B)))) with621    positiveSum, negatedNegativeSum622623theorem realMulCut.of_nonnegative (A B : Real)624  requires nonnegativeA : realZero ⊆ A625  requires nonnegativeB : realZero ⊆ B626  shows realMulCut(A, B) = realPosMulCut(A, B)627proof628  have positiveA := realPositivePart.eq_of_nonnegative with nonnegativeA629  have positiveB := realPositivePart.eq_of_nonnegative with nonnegativeB630  have negativeA := realNegativePart.eq_zero_of_nonnegative with nonnegativeA631  have negativeB := realNegativePart.eq_zero_of_nonnegative with nonnegativeB632  simp [realMulCut, positiveA, positiveB, negativeA, negativeB,633    realPosMulCut.zero_left, realPosMulCut.zero_right,634    realAddCut.zero_left, realAddCut.zero_right, realNegCut.zero]635636theorem realMulCut.zero_left (B : Real)637  shows realMulCut(realZero, B) = realZero638proof639  simp [realMulCut, realPositivePart.zero, realNegativePart.zero,640    realPosMulCut.zero_left, realPosMulCut.zero_right,641    realAddCut.zero_left, realAddCut.zero_right, realNegCut.zero]642643theorem realMulCut.commutative (A B : Real)644  shows realMulCut(A, B) = realMulCut(B, A)645proof646  have positiveA := realPositivePart.real at A647  have positiveB := realPositivePart.real at B648  have negativeA := realNegativePart.real at A649  have negativeB := realNegativePart.real at B650  have pp := realPosMulCut.commutative with positiveA, positiveB651  have nn := realPosMulCut.commutative with negativeA, negativeB652  have pn := realPosMulCut.commutative with positiveA, negativeB653  have np := realPosMulCut.commutative with negativeA, positiveB654  have crossLeft := realPosMulCut.real with negativeB, positiveA655  have crossRight := realPosMulCut.real with positiveB, negativeA656  have cross := realAddCut.commutative with crossLeft, crossRight657  simp [realMulCut, pp, nn, pn, np, cross]658659theorem realMulCut.zero_right (A : Real)660  shows realMulCut(A, realZero) = realZero661proof662  calc663    realMulCut(A, realZero) = realMulCut(realZero, A) :=664      realMulCut.commutative with realZero.real665    _ = realZero := realMulCut.zero_left at A with assumption666667theorem realMulCut.one_right (A : Real)668  shows realMulCut(A, realOne) = A669proof670  have positiveA := realPositivePart.real at A671  have negativeA := realNegativePart.real at A672  obtain ⟨zeroReal, oneReal, properOne⟩ := realLess.characterization.forward with realZero.lt_one673  have nonnegativeOne := ProperSubset.subset with properOne674  have positiveOne := realPositivePart.eq_of_nonnegative with nonnegativeOne675  have negativeOne := realNegativePart.eq_zero_of_nonnegative with nonnegativeOne676  have positiveProduct := realPosMulCut.one_right with positiveA, realPositivePart.nonnegative at A677  have negativeProduct := realPosMulCut.one_right with negativeA, realNegativePart.nonnegative at A678  simp [realMulCut, positiveOne, negativeOne, positiveProduct, negativeProduct,679    realPosMulCut.zero_left, realPosMulCut.zero_right,680    realAddCut.zero_left, realAddCut.zero_right, realParts.decomposition]681682theorem realMulCut.one_left (A : Real)683  shows realMulCut(realOne, A) = A684proof685  calc686    realMulCut(realOne, A) = realMulCut(A, realOne) :=687      realMulCut.commutative with realOne.real688    _ = A := realMulCut.one_right at A with assumption689690theorem realMulCut.associative_of_nonnegative (A B C : Real)691  requires nonnegativeA : realZero ⊆ A692  requires nonnegativeB : realZero ⊆ B693  requires nonnegativeC : realZero ⊆ C694  shows realMulCut(realMulCut(A, B), C) =695    realMulCut(A, realMulCut(B, C))696proof697  have abReduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeB698  have bcReduction := realMulCut.of_nonnegative with nonnegativeB, nonnegativeC699  have nonnegativeAB := realPosMulCut.nonnegative at A, B700  have nonnegativeBC := realPosMulCut.nonnegative at B, C701  have leftReduction := realMulCut.of_nonnegative with nonnegativeAB, nonnegativeC702  have rightReduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeBC703  have reverseRight : realPosMulCut(A, realPosMulCut(B, C)) =704      realMulCut(A, realPosMulCut(B, C))705    rw rightReduction706    rfl707  calc708    realMulCut(realMulCut(A, B), C) =709        realMulCut(realPosMulCut(A, B), C) := by simp [abReduction]710    _ = realPosMulCut(realPosMulCut(A, B), C) := leftReduction711    _ = realPosMulCut(A, realPosMulCut(B, C)) :=712      realPosMulCut.associative at A, B, C with713        *{3}714    _ = realMulCut(A, realPosMulCut(B, C)) := reverseRight715    _ = realMulCut(A, realMulCut(B, C)) := by simp [bcReduction]716717-- Total real multiplication as a set-valued function graph.718def realMul : Set :=719  { p ∈ ((ℝ × ℝ) × ℝ) |720    ∃ A ∈ ℝ, ∃ B ∈ ℝ,721      p = ((A, B) ↦ realMulCut(A, B)) }722723def realMulValue (A B : Real) : Real := realMul((A, B))724725theorem realMul.relates (A B : Real)726  shows relates(realMul, (A, B), realMulCut(A, B))727proof728  have realA : A ∈ ℝ by simp [Real]729  have realB : B ∈ ℝ by simp [Real]730  unfold relates731  apply realMul.membership.backward732  constructor733  . apply product.pair at (A, B), realMulCut(A, B), ℝ × ℝ, ℝ734    . exact product.pair with realA, realB735    . exact realMulCut.real at A, B with *{2}736  . refine ⟨A, realA, B, realB, rfl⟩737738theorem realMul.factors (input output : Set)739  requires mapped : relates(realMul, input, output)740  shows ∃ A ∈ ℝ, ∃ B ∈ ℝ,741    input = (A, B) ∧ output = realMulCut(A, B)742proof743  unfold relates at mapped744  simp [realMul.membership] at mapped745  rcases mapped with ⟨bounded, A, realA, B, realB, shape⟩746  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape747  refine ⟨A, realA, B, realB, inputShape, outputShape⟩748749theorem realMul.total750  shows TotalBetween(realMul, ℝ × ℝ, ℝ)751proof752  intros input inputInProduct753  obtain ⟨bounded, A, realA, B, realB, inputShape⟩ := product.membership.forward with inputInProduct754  have typedA : Real(A) by exact realA755  have typedB : Real(B) by exact realB756  witness realMulCut(A, B)757  constructor758  . exact realMulCut.real with typedA, typedB759  . rw inputShape760    exact realMul.relates with typedA, typedB761762theorem realMul.functional763  shows Functional(realMul)764proof765  intros input y inputY z inputZ766  obtain ⟨A, realA, B, realB, inputFirst, outputFirst⟩ := realMul.factors with inputY767  obtain ⟨C, realC, D, realD, inputSecond, outputSecond⟩ := realMul.factors with inputZ768  rw inputFirst at inputSecond769  obtain ⟨sameLeft, sameRight⟩ := orderedPair.injective with inputSecond770  rw [outputFirst, outputSecond, sameLeft, sameRight]771  rfl772773theorem realMul.function774  shows realMul : ℝ × ℝ → ℝ775proof776  constructor777    intros p hp778    simp [realMul.membership] at hp779    rcases hp with ⟨bounded, witnesses⟩780    exact bounded781  . refine ⟨realMul.functional, _⟩782    exact realMul.total783784instance realMul.operation785  shows MulOperation(ℝ, realMul)786proof787  exact realMul.function788789notation infixl 70 "*" => call2 via MulOperation(ℝ, _) for Real790791theorem realMulValue.real (A B : Real)792  shows Real(A * B)793proof794  have realA : A ∈ ℝ by simp [Real]795  have realB : B ∈ ℝ by simp [Real]796  have input := product.pair with realA, realB797  obtain ⟨C, realC, mapped⟩ := FunctionBetween.exists_value with realMul.function, input798  have applied := FunctionBetween.apply_value with realMul.function, input, mapped799  unfold call2800  rw applied801  exact realC802803theorem realMulValue.cut (A B : Real)804  shows A * B = realMulCut(A, B)805proof806  have realA : A ∈ ℝ by simp [Real]807  have realB : B ∈ ℝ by simp [Real]808  have input := product.pair with realA, realB809  have mapped := realMul.relates at A, B with *810  unfold call2811  exact FunctionBetween.apply_value with realMul.function, input, mapped812813theorem realMulValue.commutative (A B : Real)814  shows A * B = B * A815proof816  rw [realMulValue.cut, realMulValue.cut]817  exact realMulCut.commutative with *818819theorem realMulValue.zero_left (A : Real)820  shows 0 * A = 0821proof822  calc823    realZero * A = realMulCut(realZero, A) :=824      realMulValue.cut with realZero.real825    _ = realZero := realMulCut.zero_left at A with assumption826827theorem realMulValue.zero_right (A : Real)828  shows A * 0 = 0829proof830  calc831    A * realZero = realZero * A :=832      realMulValue.commutative with realZero.real833    _ = realZero := realMulValue.zero_left at A with assumption834835theorem realMulValue.one_right_of_nonnegative (A : Real)836  requires nonnegative : realZero ⊆ A837  shows A * 1 = A838proof839  obtain ⟨zeroReal, oneReal, properOne⟩ := realLess.characterization.forward with realZero.lt_one840  have nonnegativeOne := ProperSubset.subset with properOne841  calc842    A * realOne = realMulCut(A, realOne) :=843      realMulValue.cut with realOne.real844    _ = realPosMulCut(A, realOne) :=845      realMulCut.of_nonnegative at A, realOne with846        assumption, realOne.real, nonnegative, nonnegativeOne847    _ = A := realPosMulCut.one_right at A with nonnegative848849theorem realMulValue.one_left_of_nonnegative (A : Real)850  requires nonnegative : realZero ⊆ A851  shows 1 * A = A852proof853  calc854    realOne * A = A * realOne :=855      realMulValue.commutative with realOne.real856    _ = A := realMulValue.one_right_of_nonnegative at A with857      assumption, nonnegative858859theorem realMulValue.one_right (A : Real)860  shows A * 1 = A861proof862  calc863    A * realOne = realMulCut(A, realOne) :=864      realMulValue.cut with realOne.real865    _ = A := realMulCut.one_right at A with assumption866867theorem realMulValue.one_left (A : Real)868  shows 1 * A = A869proof870  calc871    realOne * A = A * realOne :=872      realMulValue.commutative with realOne.real873    _ = A := realMulValue.one_right at A with assumption874875theorem realMulValue.associative_of_nonnegative (A B C : Real)876  requires nonnegativeA : realZero ⊆ A877  requires nonnegativeB : realZero ⊆ B878  requires nonnegativeC : realZero ⊆ C879  shows (A * B) * C = A * (B * C)880proof881  have abReal := realMulValue.real at A, B with *882  have bcReal := realMulValue.real at B, C with *883  have abCut := realMulValue.cut at A, B with *884  have bcCut := realMulValue.cut at B, C with *885  have leftCut := realMulValue.cut at A * B, C with abReal, assumption886  have rightCut := realMulValue.cut at A, B * C with assumption, bcReal887  have leftInner : realMulCut(A * B, C) =888      realMulCut(realMulCut(A, B), C)889    rw abCut890    rfl891  have rightInner : realMulCut(A, realMulCut(B, C)) =892      realMulCut(A, B * C)893    rw bcCut894    rfl895  have reverseRight : realMulCut(A, B * C) = A * (B * C)896    rw rightCut897    rfl898  calc899    (A * B) * C = realMulCut(A * B, C) := leftCut900    _ = realMulCut(realMulCut(A, B), C) := leftInner901    _ = realMulCut(A, realMulCut(B, C)) :=902      realMulCut.associative_of_nonnegative at A, B, C with903        nonnegativeA, nonnegativeB, nonnegativeC904    _ = realMulCut(A, B * C) := rightInner905    _ = A * (B * C) := reverseRight906907instance realMul.identity908  shows Identity(ℝ, realMul, realOne)909proof910  constructor911  . exact realOne.real912  . intros A realA913    have typedA : Real(A) by exact realA914    constructor915    . exact realMulValue.one_left with typedA916    . exact realMulValue.one_right with typedA917918-- A real strictly above zero contains a strictly positive rational.  This is919-- the witness form of positivity used by multiplication: proper inclusion920-- supplies a new member, roundedness moves above it, and connectedness rules921-- out the larger member being nonpositive.922theorem RealLess.exists_positive_member (A : Real)923  requires positive : 0 < A924  shows ∃ a ∈ A, rationalZero < a925proof926  obtain ⟨zeroReal, realA, proper⟩ := realLess.characterization.forward with positive927  obtain ⟨q, qInA, qMissingZero⟩ := ProperSubset.missing with proper928  have cutA := Real.characterization.forward at A with assumption929  obtain ⟨a, aInA, qLessA⟩ := DedekindCut.no_greatest with cutA, qInA930  have subsetA := DedekindCut.subset_rationals with cutA931  have qInQ := subsetA with q, qInA932  have aInQ := subsetA with a, aInA933  have zeroInQ := rationalZero.rational934  have distinct : rationalZero ≠ a935    intro equal936    have qNegative : q < rationalZero by rwa equal937    apply qMissingZero938    unfold realZero939    apply rationalCut.membership.backward940    constructor941    . exact qInQ942    . exact qNegative943  have connected := rationalLess.connected_on944  have comparison := connected with945    rationalZero, zeroInQ, a, aInQ, distinct946  cases comparison with positiveA | aNegative947  . refine ⟨a, aInA, positiveA⟩948  . have qNegative := rationalLess.transitive at q, a, rationalZero with949      qLessA, aNegative950    exfalso951    apply qMissingZero952    unfold realZero953    apply rationalCut.membership.backward954    constructor955    . exact qInQ956    . exact qNegative957958-- The positive-cut product of two positive reals is positive.  The proof959-- exposes the familiar mathematical witnesses a > 0 and b > 0, then uses960-- rational density to put a member of the product above zero.961theorem realPosMulCut.positive (A B : Real)962  requires positiveA : 0 < A963  requires positiveB : 0 < B964  shows realZero < realPosMulCut(A, B)965proof966  have productReal := realPosMulCut.real at A, B with *967  have zeroSubset : realZero ⊆ realPosMulCut(A, B)968    intros q qInZero969    unfold realZero at qInZero970    obtain ⟨qInQ, qNegative⟩ := rationalCut.membership.forward with qInZero971    apply realPosMulCut.membership.backward972    refine ⟨qInQ, _⟩973    left974    exact qNegative975  obtain ⟨a, aInA, positiveRationalA⟩ := RealLess.exists_positive_member with positiveA976  obtain ⟨b, bInB, positiveRationalB⟩ := RealLess.exists_positive_member with positiveB977  have cutA := Real.characterization.forward at A with assumption978  have cutB := Real.characterization.forward at B with assumption979  have subsetA := DedekindCut.subset_rationals with cutA980  have subsetB := DedekindCut.subset_rationals with cutB981  have aInQ := subsetA with a, aInA982  have bInQ := subsetB with b, bInB983  have aRational : Rational(a) by typecheck984  have bRational : Rational(b) by typecheck985  have productPositive := rationalLess.mul_positive with positiveRationalA, positiveRationalB986  have productRational := rationalMulValue.rational with aRational, bRational987  obtain ⟨s, sInQ, sPositive, sBelowProduct⟩ := rationalLess.dense with988    rationalZero.rational, productRational, productPositive989  have sInProduct : s ∈ realPosMulCut(A, B)990    apply realPosMulCut.membership.backward991    refine ⟨sInQ, _⟩992    right993    refine ⟨a, aInQ, aInA, b, bInQ, bInB,994      positiveRationalA, positiveRationalB, sBelowProduct⟩995  have sMissingZero : ¬(s ∈ realZero)996    intro sInZero997    unfold realZero at sInZero998    obtain ⟨sAgain, sNegative⟩ := rationalCut.membership.forward with sInZero999    have cycle := rationalLess.transitive with sPositive, sNegative1000    have impossible := rationalLess.irreflexive_on1001    exact impossible with rationalZero, cycle1002  have unequal : realZero ≠ realPosMulCut(A, B)1003    intro equal1004    apply sMissingZero1005    rwa equal1006  have proper : realZero ⊂ realPosMulCut(A, B)1007    constructor1008    . exact zeroSubset1009    . exact unequal1010  apply realLess.characterization.backward1011  unfold RealLess1012  refine ⟨realZero.real, productReal, proper⟩10131014-- Positivity for the public, signed multiplication operation.  Strict1015-- positivity supplies the two nonnegative inclusions, so the canonical sign1016-- decomposition reduces definitionally to the positive-cut product.1017theorem realMulValue.positive (A B : Real)1018  requires positiveA : 0 < A1019  requires positiveB : 0 < B1020  shows 0 < A * B1021proof1022  have orderA := realLess.characterization.forward with positiveA1023  have orderB := realLess.characterization.forward with positiveB1024  rcases orderA with ⟨zeroRealA, realA, properA⟩1025  rcases orderB with ⟨zeroRealB, realB, properB⟩1026  have nonnegativeA := ProperSubset.subset with properA1027  have nonnegativeB := ProperSubset.subset with properB1028  have cutPositive := realPosMulCut.positive with positiveA, positiveB1029  have valueCut := realMulValue.cut at A, B with *1030  have reduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeB1031  rwa [valueCut, reduction]10321033instance realMul.positive1034  shows MulPositive(ℝ, realMul, realZero, realLess)1035proof1036  intros A realA B realB positiveA positiveB1037  exact realMulValue.positive with positiveA, positiveB10381039instance realMul.magma1040  shows IsMagma(ℝ, realMul)1041proof1042  exact realMul.function10431044instance realMul.commutative1045  shows Commutative(ℝ, realMul)1046proof1047  intros A realA B realB1048  have typedA : Real(A) by typecheck1049  have typedB : Real(B) by typecheck1050  exact realMulValue.commutative with typedA, typedB10511052theorem reals.nontrivial1053  shows Nontrivial(ℝ, realZero, realOne)1054proof1055  constructor1056  . exact realZero.real1057  constructor1058  . exact realOne.real1059  . exact realZero.ne_one10601061theorem realMulValue.type (A B : Real)1062  shows Real(realMulValue(A, B))1063proof1064  have closed := realMulValue.real at A, B with *1065  unfold realMulValue1066  unfold call2 at closed1067  exact closed1068