Grace/Cumulus/Complex/Core.g17

Open in Workbench Download source

Imports

Real.Squares

Declarations

Source

1-- Concrete complex numbers as ordered pairs of Dedekind reals.2-- 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.Complex.Core8import Real.Squares910def complexCarrier : Set := ℝ × ℝ11def complexZero : Set := (realZero, realZero)12def complexOne : Set := (realOne, realZero)13def complexAdd : Set := {p ∈ (complexCarrier × complexCarrier) × complexCarrier | ∃ a ∈ ℝ, ∃ b ∈ ℝ, ∃ c ∈ ℝ, ∃ d ∈ ℝ, p = (((a, b), (c, d)), (realAdd(a, c), realAdd(b, d)))}14def complexNeg : Set := {p ∈ complexCarrier × complexCarrier | ∃ a ∈ ℝ, ∃ b ∈ ℝ, p = ((a, b), (realNeg(a), realNeg(b)))}15def complexMul : Set := {p ∈ (complexCarrier × complexCarrier) × complexCarrier | ∃ a ∈ ℝ, ∃ b ∈ ℝ, ∃ c ∈ ℝ, ∃ d ∈ ℝ, p = (((a, b), (c, d)), (realAdd(realMul(a, c), realNeg(realMul(b, d))), realAdd(realMul(a, d), realMul(b, c))))}1617theorem complexCarrier.pair (a b : Real)18  shows (a, b) ∈ complexCarrier19proof20  unfold complexCarrier21  apply product.pair22  . typecheck23  . typecheck2425theorem complexCarrier.cases (x : Set)26  requires member : x ∈ complexCarrier27  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ x = (a, b)28proof29  rw complexCarrier at member30  obtain ⟨bounded, a, ha, b, hb, shape⟩ := product.membership.forward with member31  have aReal : Real(a) by typecheck32  have bReal : Real(b) by typecheck33  refine ⟨a, aReal, b, bReal, shape⟩3435theorem complexAdd.relates (a b c d : Real)36  shows relates(complexAdd, ((a, b), (c, d)), (a + c, b + d))37proof38  have aIn : a ∈ ℝ by typecheck39  have bIn : b ∈ ℝ by typecheck40  have cIn : c ∈ ℝ by typecheck41  have dIn : d ∈ ℝ by typecheck42  have first := complexCarrier.pair at a, b with *43  have second := complexCarrier.pair at c, d with *44  have input := product.pair with first, second45  have output : (a + c, b + d) ∈ complexCarrier by apply complexCarrier.pair at a + c, b + d46  have bounded := product.pair with input, output47  unfold relates48  exact complexAdd.membership.backward with ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, rfl⟩4950theorem complexAdd.factors (x y : Set)51  requires related : relates(complexAdd, x, y)52  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ ∃ c, Real(c) ∧ ∃ d, Real(d) ∧ x = ((a, b), (c, d)) ∧ y = (a + c, b + d)53proof54  obtain ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, shape⟩ := complexAdd.membership.forward at (x, y) with related55  have pair := orderedPair.injective with shape56  have aReal : Real(a) by typecheck57  have bReal : Real(b) by typecheck58  have cReal : Real(c) by typecheck59  have dReal : Real(d) by typecheck60  refine ⟨a, aReal, b, bReal, c, cReal, d, dReal, pair⟩6162theorem complexAdd.function63  shows complexAdd : complexCarrier × complexCarrier → complexCarrier64proof65  constructor66    intros p member67    have data := complexAdd.membership.forward with member68    exact data.left69  . constructor70      intros x y first z second71      obtain ⟨a, aReal, b, bReal, c, cReal, d, dReal, input, output⟩ := complexAdd.factors with first72      obtain ⟨e, eReal, f, fReal, g, gReal, h, hReal, input2, output2⟩ := complexAdd.factors with second73      have same : ((a, b), (c, d)) = ((e, f), (g, h)) by cc74      have outer := orderedPair.injective with same75      have left := orderedPair.injective with outer.left76      have right := orderedPair.injective with outer.right77      cc78    . intros x member79      obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with member80      obtain ⟨a, aReal, b, bReal, first⟩ := complexCarrier.cases with hu81      obtain ⟨c, cReal, d, dReal, second⟩ := complexCarrier.cases with hv82      rw [first, second] at shape83      witness (a + c, b + d)84      constructor85      . apply complexCarrier.pair at a + c, b + d86      . rw shape87        exact complexAdd.relates with *8889theorem complexAdd.pair (a b c d : Real)90  shows complexAdd((a, b), (c, d)) = (a + c, b + d)91proof92  have first := complexCarrier.pair at a, b with *93  have second := complexCarrier.pair at c, d with *94  have input := product.pair with first, second95  have related := complexAdd.relates at a, b, c, d with *96  have value := FunctionBetween.apply_value with complexAdd.function, input, related97  simp [call2]9899theorem complexNeg.relates (a b : Real)100  shows relates(complexNeg, (a, b), (-a, -b))101proof102  have aIn : a ∈ ℝ by typecheck103  have bIn : b ∈ ℝ by typecheck104  have first := complexCarrier.pair at a, b with *105  have input := first106  have output : (-a, -b) ∈ complexCarrier by apply complexCarrier.pair at -a, -b107  have bounded := product.pair with input, output108  unfold relates109  exact complexNeg.membership.backward with ⟨bounded, a, aIn, b, bIn, rfl⟩110111theorem complexNeg.factors (x y : Set)112  requires related : relates(complexNeg, x, y)113  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ x = (a, b) ∧ y = (-a, -b)114proof115  unfold relates at related116  obtain ⟨bounded, a, aIn, b, bIn, shape⟩ := complexNeg.membership.forward with related117  have pair := orderedPair.injective with shape118  have aReal : Real(a) by typecheck119  have bReal : Real(b) by typecheck120  refine ⟨a, aReal, b, bReal, pair⟩121122theorem complexNeg.function123  shows complexNeg : complexCarrier → complexCarrier124proof125  constructor126    intros p member127    have data := complexNeg.membership.forward with member128    exact data.left129  . constructor130      intros x y first z second131      obtain ⟨a, aReal, b, bReal, input, output⟩ := complexNeg.factors with first132      obtain ⟨e, eReal, f, fReal, input2, output2⟩ := complexNeg.factors with second133      have same : (a, b) = (e, f) by cc134      have coordinates := orderedPair.injective with same135      cc136    . intros x member137      obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member138      witness (-a, -b)139      constructor140      . apply complexCarrier.pair at -a, -b141      . rw shape142        exact complexNeg.relates with *143144theorem complexNeg.pair (a b : Real)145  shows complexNeg((a, b)) = (-a, -b)146proof147  have first := complexCarrier.pair at a, b with *148  have input := first149  have related := complexNeg.relates at a, b with *150  have value := FunctionBetween.apply_value with complexNeg.function, input, related151  assumption152153theorem complexMul.relates (a b c d : Real)154  shows relates(complexMul, ((a, b), (c, d)), (a * c + -(b * d), a * d + b * c))155proof156  have aIn : a ∈ ℝ by typecheck157  have bIn : b ∈ ℝ by typecheck158  have cIn : c ∈ ℝ by typecheck159  have dIn : d ∈ ℝ by typecheck160  have first := complexCarrier.pair at a, b with *161  have second := complexCarrier.pair at c, d with *162  have input := product.pair with first, second163  have output : (a * c + -(b * d), a * d + b * c) ∈ complexCarrier by apply complexCarrier.pair164  have bounded := product.pair with input, output165  unfold relates166  exact complexMul.membership.backward with ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, rfl⟩167168theorem complexMul.factors (x y : Set)169  requires related : relates(complexMul, x, y)170  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ ∃ c, Real(c) ∧ ∃ d, Real(d) ∧ x = ((a, b), (c, d)) ∧ y = (a * c + -(b * d), a * d + b * c)171proof172  unfold relates at related173  obtain ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, shape⟩ := complexMul.membership.forward with related174  have pair := orderedPair.injective with shape175  have aReal : Real(a) by typecheck176  have bReal : Real(b) by typecheck177  have cReal : Real(c) by typecheck178  have dReal : Real(d) by typecheck179  refine ⟨a, aReal, b, bReal, c, cReal, d, dReal, pair⟩180181theorem complexMul.function182  shows complexMul : complexCarrier × complexCarrier → complexCarrier183proof184  constructor185    intros p member186    have data := complexMul.membership.forward with member187    exact data.left188  . constructor189      intros x y first z second190      obtain ⟨a, aReal, b, bReal, c, cReal, d, dReal, input, output⟩ := complexMul.factors with first191      obtain ⟨e, eReal, f, fReal, g, gReal, h, hReal, input2, output2⟩ := complexMul.factors with second192      have same : ((a, b), (c, d)) = ((e, f), (g, h)) by cc193      have outer := orderedPair.injective with same194      have left := orderedPair.injective with outer.left195      have right := orderedPair.injective with outer.right196      cc197    . intros x member198      obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with member199      obtain ⟨a, aReal, b, bReal, first⟩ := complexCarrier.cases with hu200      obtain ⟨c, cReal, d, dReal, second⟩ := complexCarrier.cases with hv201      rw [first, second] at shape202      witness (a * c + -(b * d), a * d + b * c)203      constructor204      . apply complexCarrier.pair at a * c + -(b * d), a * d + b * c205      . rw shape206        exact complexMul.relates with *207208theorem complexMul.pair (a b c d : Real)209  shows complexMul((a, b), (c, d)) = (a * c + -(b * d), a * d + b * c)210proof211  have first := complexCarrier.pair at a, b with *212  have second := complexCarrier.pair at c, d with *213  have input := product.pair with first, second214  have related := complexMul.relates at a, b, c, d with *215  have value := FunctionBetween.apply_value with complexMul.function, input, related216  simp [call2]217