-- Four explicit square directions separate nonzero complex vectors.
-- 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.Complex.SquareDirections
import PolynomialStationarity

theorem realLe.zero_of_opposite_bounds (a : Real)
  requires positive : realZero ≤ a
  requires negative : realZero ≤ -a
  shows a = realZero
proof
  have shifted := realLe.add_right at realZero, -a, a with *
  rw realAddValue.zero_left at shifted
  have cancel : -a + a = realZero by ring
  rw cancel at shifted
  have lower := realLe.characterization.forward with positive
  have upper := realLe.characterization.forward with shifted
  exact RealLe.antisymmetric with upper, lower

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)
notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)

theorem complexDot.square_pair (a b c d x y : Real)
  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)]
proof
  simp [complexMul.pair, Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]
  ring

theorem complexDot.square_bounds (a b c d : Real)
  requires bounds : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot((a, b), ℂ[(u * u) * (c, d)])
  shows R[a * c + b * d] = realZero ∧ R[2 * (b * c - a * d)] = realZero
proof
  have p1 := complexCarrier.pair at realOne, realZero with *
  have pi := complexCarrier.pair at realZero, realOne with *
  have pp := complexCarrier.pair at realOne, realOne with *
  have pm := complexCarrier.pair at realOne, R[-1] with *
  have b1 := bounds with (realOne, realZero), p1
  have bi := bounds with (realZero, realOne), pi
  have bp := bounds with (realOne, realOne), pp
  have bm := bounds with (realOne, R[-1]), pm
  rw complexDot.square_pair at b1
  rw complexDot.square_pair at bi
  rw complexDot.square_pair at bp
  rw complexDot.square_pair at bm
  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 ring
  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 ring
  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)]
    ring
  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))]
    ring
  rw e1 at b1
  rw ei at bi
  rw ep at bp
  rw em at bm
  have first := realLe.zero_of_opposite_bounds at R[a * c + b * d] with *
  have second := realLe.zero_of_opposite_bounds at R[2 * (b * c - a * d)] with *
  refine ⟨first, second⟩

theorem complexDot.square_direction (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  requires nonzeroZ : z ≠ ℂ[0]
  requires nonzeroW : w ≠ ℂ[0]
  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[(u * u) * w]) < realZero
proof
  by_contra noDirection
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  have pointZ := complex.point at z with *
  have all : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot(z, ℂ[(u * u) * w])
    intros u uIn
    have square := IsRing.mul_closed with ordinary, uIn, uIn
    have product := IsRing.mul_closed with ordinary, square, second
    have point := complex.point with product
    by_contra notNonnegative
    have negative := realLess.of_not_le with *
    apply noDirection
    refine ⟨u, uIn, negative⟩
  have positiveZ := complexNormSquared.positive at z with *
  have positiveW := complexNormSquared.positive at w with *
  have productPositive := realMulValue.positive at complexNormSquared(z), complexNormSquared(w) with *
  have twoPositive : (0:R) < 2 by linarith
  have fourPositive := realMulValue.positive at R[2], R[2] with *
  have positive := realMulValue.positive at R[2 * 2], R[complexNormSquared(z) * complexNormSquared(w)] with *
  obtain ⟨a, aReal, b, bReal, zShape⟩ := complexCarrier.cases at z with *
  obtain ⟨c, cReal, d, dReal, wShape⟩ := complexCarrier.cases at w with *
  have coordinateBounds : ∀ u ∈ ℂ, realZero ≤ Euclidean.dot((a, b), ℂ[(u * u) * (c, d)])
    intros u uIn
    have bound := all with u, uIn
    rwa [zShape, wShape] at bound
  obtain ⟨vanishes, imaginaryVanishes⟩ := complexDot.square_bounds at a, b, c, d with *
  rw [zShape, wShape, complexNormSquared.pair, complexNormSquared.pair] at positive
  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))]
    ring
  rw [identity, vanishes, imaginaryVanishes] at positive
  have zero : R[(2 * 0) * (2 * 0) + 0 * 0] = realZero by ring
  rw zero at positive
  have irrefl := realLess.irreflexive_on
  exact irrefl with realZero, positive

theorem complexDot.small_power_direction (z w : Set) (n : Nat)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  requires nonzeroZ : z ≠ ℂ[0]
  requires nonzeroW : w ≠ ℂ[0]
  requires small : n ≤ (1:N)
  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero
proof
  obtain ⟨u, uIn, negative⟩ := complexDot.square_direction at z, w with *
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  have square := IsRing.mul_closed with ordinary, uIn, uIn
  have shape := natural.zero_or_successor with *
  cases shape with zero | successor
  . have power : ℂ[(u * u) ^ succ(n)] = ℂ[u * u]
      rw [zero, monoidPow.succ, monoidPow.zero]
      ring
    refine ⟨ℂ[u * u], square, ?_⟩
    rwa power
  . obtain ⟨k, kNat, nShape⟩ := successor
    rw nShape at small
    have upper : k ≤ (0:N) by arith
    have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at k with *
    have kZero := LessEqual.antisymmetric at k, (0:N) with *
    have nOne : n = (1:N)
      rw [nShape, kZero]
      rfl
    have power : ℂ[u ^ succ(n)] = ℂ[u * u]
      rw [nOne, monoidPow.succ, monoidPow.succ, monoidPow.zero]
      ring
    refine ⟨u, uIn, ?_⟩
    rwa power

end Complexes