-- Positive powers separate directions: odd units and square-root lifting.
-- 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.PowerDirections
import QuadraticRoots
import OddDirections

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)

lemma complexPower.directions_membership (k : Set)
  shows Nat(k) → k ≠ (0:N) → ∀ z ∈ ℂ, ∀ w ∈ ℂ, z ≠ ℂ[0] → w ≠ ℂ[0] →
    ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ k * w]) < realZero
proof
  induction k using membership
  intros current ih currentNat nonzero z zIn w wIn nonzeroZ nonzeroW
  have alternatives := parity.exhaustive with *
  cases alternatives with even | odd
  . obtain ⟨m, mIn, shape⟩ := even
    have mNat := nat.omega.backward at m with *
    have mNonzero : m ≠ (0:N)
      intro zero
      rw [zero, Grace.Core.Nat.Rec.add] at shape
      exact nonzero with shape
    have less := Less.add_positive at m, m with *
    rw ← shape at less
    have inside := membership.of_Less with mNat, currentNat, less
    obtain ⟨v, vIn, negative⟩ := ih with inside, mNat, mNonzero, z, zIn, w, wIn, nonzeroZ, nonzeroW
    obtain ⟨u, uIn, square⟩ := complex.square_root at v with *
    have power : u ^ current = v ^ m
      rw [shape, complexPower.square, square]
      rfl
    refine ⟨u, uIn, ?_⟩
    rwa power
  . obtain ⟨m, mIn, shape⟩ := odd
    have mNat := nat.omega.backward at m with *
    obtain ⟨u, uIn, negative⟩ := complexDot.odd_power_direction at z, w, m with *
    refine ⟨u, uIn, ?_⟩
    rwa shape

theorem complexDot.power_direction (z w : Set) (n : Nat)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  requires nonzeroZ : z ≠ ℂ[0]
  requires nonzeroW : w ≠ ℂ[0]
  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero
proof
  have next : Nat(succ(n)) by typecheck
  have nonzero : succ(n) ≠ (0:N)
    intro equal
    have impossible := Naturals.disjoint.zero.succ at n
    apply impossible
    symm
    exact equal
  have directions := complexPower.directions_membership with next, nonzero
  exact directions with z, first, w, second, nonzeroZ, nonzeroW

end Complexes