Grace/Cumulus/Complex/PowerDirections.g17

Open in Workbench Download source

Imports

QuadraticRoots · OddDirections

Declarations

• complexPower.directions_membership lemma derivation
• complexDot.power_direction theorem derivation

Source

1-- Positive powers separate directions: odd units and square-root lifting.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.PowerDirections8import QuadraticRoots9import OddDirections1011section Complexes12notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1314lemma complexPower.directions_membership (k : Set)15  shows Nat(k) → k ≠ (0:N) → ∀ z ∈ ℂ, ∀ w ∈ ℂ, z ≠ ℂ[0] → w ≠ ℂ[0] →16    ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ k * w]) < realZero17proof18  induction k using membership19  intros current ih currentNat nonzero z zIn w wIn nonzeroZ nonzeroW20  have alternatives := parity.exhaustive with *21  cases alternatives with even | odd22  . obtain ⟨m, mIn, shape⟩ := even23    have mNat := nat.omega.backward at m with *24    have mNonzero : m ≠ (0:N)25      intro zero26      rw [zero, Grace.Core.Nat.Rec.add] at shape27      exact nonzero with shape28    have less := Less.add_positive at m, m with *29    rw ← shape at less30    have inside := membership.of_Less with mNat, currentNat, less31    obtain ⟨v, vIn, negative⟩ := ih with inside, mNat, mNonzero, z, zIn, w, wIn, nonzeroZ, nonzeroW32    obtain ⟨u, uIn, square⟩ := complex.square_root at v with *33    have power : u ^ current = v ^ m34      rw [shape, complexPower.square, square]35      rfl36    refine ⟨u, uIn, ?_⟩37    rwa power38  . obtain ⟨m, mIn, shape⟩ := odd39    have mNat := nat.omega.backward at m with *40    obtain ⟨u, uIn, negative⟩ := complexDot.odd_power_direction at z, w, m with *41    refine ⟨u, uIn, ?_⟩42    rwa shape4344theorem complexDot.power_direction (z w : Set) (n : Nat)45  requires first : z ∈ ℂ46  requires second : w ∈ ℂ47  requires nonzeroZ : z ≠ ℂ[0]48  requires nonzeroW : w ≠ ℂ[0]49  shows ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero50proof51  have next : Nat(succ(n)) by typecheck52  have nonzero : succ(n) ≠ (0:N)53    intro equal54    have impossible := Naturals.disjoint.zero.succ at n55    apply impossible56    symm57    exact equal58  have directions := complexPower.directions_membership with next, nonzero59  exact directions with z, first, w, second, nonzeroZ, nonzeroW6061end Complexes62