Grace/Cumulus/Complex/SquareDirections.g17

Open in Workbench Download source

Imports

PolynomialStationarity

Declarations

Source

1-- Four explicit square directions separate nonzero complex 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.SquareDirections8import PolynomialStationarity910theorem realLe.zero_of_opposite_bounds (a : Real)11  requires positive : realZero ≤ a12  requires negative : realZero ≤ -a13  shows a = realZero14proof15  have shifted := realLe.add_right at realZero, -a, a with *16  rw realAddValue.zero_left at shifted17  have cancel : -a + a = realZero by ring18  rw cancel at shifted19  have lower := realLe.characterization.forward with positive20  have upper := realLe.characterization.forward with shifted21  exact RealLe.antisymmetric with upper, lower2223section Complexes24notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)25notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)2627theorem complexDot.square_pair (a b c d x y : Real)28  shows Euclidean.dot((a, b), ℂ[((x, y) * (x, y)) * (c, d)]) = R[(x * x - y * y) * (a * c + b * d) + (x * y + y * x) * (b * c - a * d)]29proof30  simp [complexMul.pair, Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]31  ring3233theorem complexDot.square_bounds (a b c d : Real)34  requires bounds : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot((a, b), ℂ[(u * u) * (c, d)])35  shows R[a * c + b * d] = realZero ∧ R[2 * (b * c - a * d)] = realZero36proof37  have p1 := complexCarrier.pair at realOne, realZero with *38  have pi := complexCarrier.pair at realZero, realOne with *39  have pp := complexCarrier.pair at realOne, realOne with *40  have pm := complexCarrier.pair at realOne, R[-1] with *41  have b1 := bounds with (realOne, realZero), p142  have bi := bounds with (realZero, realOne), pi43  have bp := bounds with (realOne, realOne), pp44  have bm := bounds with (realOne, R[-1]), pm45  rw complexDot.square_pair at b146  rw complexDot.square_pair at bi47  rw complexDot.square_pair at bp48  rw complexDot.square_pair at bm49  have e1 : R[(1 * 1 - 0 * 0) * (a * c + b * d) + (1 * 0 + 0 * 1) * (b * c - a * d)] = R[a * c + b * d] by ring50  have ei : R[(0 * 0 - 1 * 1) * (a * c + b * d) + (0 * 1 + 1 * 0) * (b * c - a * d)] = R[-(a * c + b * d)] by ring51  have ep : R[(1 * 1 - 1 * 1) * (a * c + b * d) + (1 * 1 + 1 * 1) * (b * c - a * d)] = R[2 * (b * c - a * d)]52    ring53  have em : R[(1 * 1 - (-1) * (-1)) * (a * c + b * d) + (1 * (-1) + (-1) * 1) * (b * c - a * d)] = R[-(2 * (b * c - a * d))]54    ring55  rw e1 at b156  rw ei at bi57  rw ep at bp58  rw em at bm59  have first := realLe.zero_of_opposite_bounds at R[a * c + b * d] with *60  have second := realLe.zero_of_opposite_bounds at R[2 * (b * c - a * d)] with *61  refine ⟨first, second⟩6263theorem complexDot.square_direction (z w : Set)64  requires first : z ∈ ℂ65  requires second : w ∈ ℂ66  requires nonzeroZ : z ≠ ℂ[0]67  requires nonzeroW : w ≠ ℂ[0]68  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[(u * u) * w]) < realZero69proof70  by_contra noDirection71  have ring := complexes.comm_ring72  have ordinary := IsCommRing.ring with ring73  have pointZ := complex.point at z with *74  have all : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot(z, ℂ[(u * u) * w])75    intros u uIn76    have square := IsRing.mul_closed with ordinary, uIn, uIn77    have product := IsRing.mul_closed with ordinary, square, second78    have point := complex.point with product79    by_contra notNonnegative80    have negative := realLess.of_not_le with *81    apply noDirection82    refine ⟨u, uIn, negative⟩83  have positiveZ := complexNormSquared.positive at z with *84  have positiveW := complexNormSquared.positive at w with *85  have productPositive := realMulValue.positive at complexNormSquared(z), complexNormSquared(w) with *86  have twoPositive : (0:R) < 2 by linarith87  have fourPositive := realMulValue.positive at R[2], R[2] with *88  have positive := realMulValue.positive at R[2 * 2], R[complexNormSquared(z) * complexNormSquared(w)] with *89  obtain ⟨a, aReal, b, bReal, zShape⟩ := complexCarrier.cases at z with *90  obtain ⟨c, cReal, d, dReal, wShape⟩ := complexCarrier.cases at w with *91  have coordinateBounds : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot((a, b), ℂ[(u * u) * (c, d)])92    intros u uIn93    have bound := all with u, uIn94    rwa [zShape, wShape] at bound95  obtain ⟨vanishes, imaginaryVanishes⟩ := complexDot.square_bounds at a, b, c, d with *96  rw [zShape, wShape, complexNormSquared.pair, complexNormSquared.pair] at positive97  have identity : R[(2 * 2) * ((a * a + b * b) * (c * c + d * d))] = R[(2 * (a * c + b * d)) * (2 * (a * c + b * d)) + (2 * (b * c - a * d)) * (2 * (b * c - a * d))]98    ring99  rw [identity, vanishes, imaginaryVanishes] at positive100  have zero : R[(2 * 0) * (2 * 0) + 0 * 0] = realZero by ring101  rw zero at positive102  have irrefl := realLess.irreflexive_on103  exact irrefl with realZero, positive104105theorem complexDot.small_power_direction (z w : Set) (n : Nat)106  requires first : z ∈ ℂ107  requires second : w ∈ ℂ108  requires nonzeroZ : z ≠ ℂ[0]109  requires nonzeroW : w ≠ ℂ[0]110  requires small : n ≤ (1:N)111  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero112proof113  obtain ⟨u, uIn, negative⟩ := complexDot.square_direction at z, w with *114  have ring := complexes.comm_ring115  have ordinary := IsCommRing.ring with ring116  have square := IsRing.mul_closed with ordinary, uIn, uIn117  have shape := natural.zero_or_successor with *118  cases shape with zero | successor119  . have power : ℂ[(u * u) ^ succ(n)] = ℂ[u * u]120      rw [zero, monoidPow.succ, monoidPow.zero]121      ring122    refine ⟨ℂ[u * u], square, ?_⟩123    rwa power124  . obtain ⟨k, kNat, nShape⟩ := successor125    rw nShape at small126    have upper : k ≤ (0:N) by arith127    have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at k with *128    have kZero := LessEqual.antisymmetric at k, (0:N) with *129    have nOne : n = (1:N)130      rw [nShape, kZero]131      rfl132    have power : ℂ[u ^ succ(n)] = ℂ[u * u]133      rw [nOne, monoidPow.succ, monoidPow.succ, monoidPow.zero]134      ring135    refine ⟨u, uIn, ?_⟩136    rwa power137138end Complexes139