Grace/Cumulus/Complex/OddDirections.g17

Open in Workbench Download source

Imports

PowerArithmetic

Declarations

Source

1-- Odd powers preserve enough unit directions to separate nonzero vectors.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.OddDirections8import PowerArithmetic910section Complexes11notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)12notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1314theorem complexDot.neg_right (z w : Set)15  requires first : z ∈ ℂ16  requires second : w ∈ ℂ17  shows Euclidean.dot(z, ℂ[-w]) = R[-Euclidean.dot(z, w)]18proof19  obtain ⟨a, aReal, b, bReal, zs⟩ := complexCarrier.cases at z with *20  obtain ⟨c, cReal, d, dReal, ws⟩ := complexCarrier.cases at w with *21  rw [zs, ws]22  simp [complexNeg.pair, Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]23  ring2425theorem complexDot.imaginary_pair (a b c d : Real)26  shows Euclidean.dot((a, b), ℂ[complexImaginaryUnit * (c, d)]) = R[b * c - a * d]27proof28  unfold complexImaginaryUnit29  simp [complexMul.pair, Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]30  ring3132theorem complexDot.square_zero (z w u : Set)33  requires first : z ∈ ℂ34  requires second : w ∈ ℂ35  requires direction : u ∈ ℂ36  requires realPart : Euclidean.dot(z, w) = realZero37  requires imaginaryPart : Euclidean.dot(z, ℂ[complexImaginaryUnit * w]) = realZero38  shows Euclidean.dot(z, ℂ[(u * u) * w]) = realZero39proof40  obtain ⟨a, aReal, b, bReal, zs⟩ := complexCarrier.cases at z with *41  obtain ⟨c, cReal, d, dReal, ws⟩ := complexCarrier.cases at w with *42  obtain ⟨x, xReal, y, yReal, us⟩ := complexCarrier.cases at u with *43  rw [zs, ws] at realPart44  simp [Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair] at realPart45  rw [zs, ws, complexDot.imaginary_pair] at imaginaryPart46  rw [zs, ws, us, complexDot.square_pair, realPart, imaginaryPart]47  ring4849theorem complexDot.odd_power_direction (z w : Set) (n : Nat)50  requires first : z ∈ ℂ51  requires second : w ∈ ℂ52  requires nonzeroZ : z ≠ ℂ[0]53  requires nonzeroW : w ≠ ℂ[0]54  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ (succ(Grace.Core.Nat.Rec.add(n, n))) * w]) < realZero55proof56  by_contra noDirection57  have ring := complexes.comm_ring58  have ordinary := IsCommRing.ring with ring59  have monoid := IsRing.multiplicative with ordinary60  have pointZ := complex.point at z with *61  have all : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot(z, ℂ[u ^ (succ(Grace.Core.Nat.Rec.add(n, n))) * w])62    intros u uIn63    have power := monoidPow.closed at ℂ, complexMul, complexOne, u, succ(Grace.Core.Nat.Rec.add(n, n)) with *64    have product := IsRing.mul_closed with ordinary, power, second65    have point := complex.point with product66    by_contra notNonnegative67    have negative := realLess.of_not_le with *68    apply noDirection69    refine ⟨u, uIn, negative⟩70  have oneIn := complexOne.member71  have negOne := IsRing.neg_closed with ordinary, oneIn72  have iIn := complexImaginaryUnit.member73  have niIn := IsRing.neg_closed with ordinary, iIn74  have iw := IsRing.mul_closed with ordinary, iIn, second75  have oneBound := all with ℂ[1], oneIn76  have negBound := all with ℂ[-1], negOne77  rw complexPower.one at oneBound78  rw complexPower.negative_one_odd at negBound79  have unit : ℂ[1 * w] = w by ring80  have negativeUnit : ℂ[(-1) * w] = ℂ[-w] by ring81  rw unit at oneBound82  rw [negativeUnit, complexDot.neg_right] at negBound83  have pointW := complex.point at w with *84  have realPart := realLe.zero_of_opposite_bounds with *85  have iBound := all with complexImaginaryUnit, iIn86  have niBound := all with ℂ[-complexImaginaryUnit], niIn87  have negativeProduct : ℂ[(-complexImaginaryUnit) * w] = ℂ[-(complexImaginaryUnit * w)] by ring88  have iwPoint := complex.point with iw89  have imaginaryPart : Euclidean.dot(z, ℂ[complexImaginaryUnit * w]) = realZero90    have alternatives := complexPower.imaginary_odd with *91    cases alternatives with direct | reversed92    . rw direct.left at iBound93      rw [direct.right, negativeProduct, complexDot.neg_right] at niBound94      exact realLe.zero_of_opposite_bounds with *95    . rw reversed.left at iBound96      rw reversed.right at niBound97      rw [negativeProduct, complexDot.neg_right] at iBound98      exact realLe.zero_of_opposite_bounds with *99  obtain ⟨u, uIn, negative⟩ := complexDot.square_direction at z, w with *100  have zero := complexDot.square_zero at z, w, u with *101  rw zero at negative102  have irrefl := realLess.irreflexive_on103  exact irrefl with realZero, negative104105end Complexes106