Grace/Cumulus/Geometry/Absorption/Roots.g17

Open in Workbench Download source

Imports

Complex.Field · Complex.PowerArithmetic · Algebra.Polynomial.HornerRoots

Declarations

Source

1-- Roots in ℂ: for n ≥ 1 and c ∈ ℂ the solutions of zⁿ = c are the roots2-- of the polynomial zⁿ − c in Horner form, so finitely many3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Absorption.Roots9import Complex.Field10import Complex.PowerArithmetic11import Algebra.Polynomial.HornerRoots1213-- A run of k zero coefficients, and the roots of zᵏ⁺¹ − c as the root14-- set of the Horner form with the lower coefficients −c, 0, …, 0.15def complexZeros (k : Nat) → Set16  | zero => []17  | succ(j) => complexZero :: complexZeros(j)1819def complexPowerRoots (c : Set, k : Nat) : Set :=20  hornerRoots{complexCarrier}(complexAdd, complexZero, complexMul, complexOne,21    complexNeg(c) :: complexZeros(k))2223def complexUnityRoots (k : Nat) : Set := complexPowerRoots(complexOne, k)2425theorem complexZeros.zero26  shows complexZeros(0) = []27proof28  simp [complexZeros]2930theorem complexZeros.succ (j : Nat)31  shows complexZeros(succ(j)) = complexZero :: complexZeros(j)32proof33  simp [complexZeros]3435theorem complexZeros.list (k : Nat)36  shows List(complexCarrier, complexZeros(k))37proof38  induction k39  | zero =>40    rw complexZeros.zero41    typecheck42  | succ(j) using ih =>43    have zeroIn := complexZero.member44    rw complexZeros.succ45    typecheck4647section Complexes48notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)4950-- The Horner value of a run of zero coefficients under the leading51-- coefficient 1 is the power zᵏ.52theorem hornerAt.zeros (z : Set) (k : Nat)53  requires member : z ∈ complexCarrier54  shows hornerAt{complexCarrier}(complexAdd, complexMul, complexOne, z,55      complexZeros(k)) =56    monoidPow(complexMul, complexOne, z, k)57proof58  induction k59  | zero =>60    rw [complexZeros.zero, hornerAt.nil, monoidPow.zero]61    rfl62  | succ(j) using ih =>63    have ring := complexes.comm_ring64    have ordinary := IsCommRing.ring with ring65    have monoid := IsRing.multiplicative with ordinary66    have zeroIn := complexZero.member67    have tail := complexZeros.list at j68    have power := monoidPow.closed at complexCarrier, complexMul, complexOne, z, j69      with monoid, member70    have product := IsRing.mul_closed with ordinary, member, power71    rw [complexZeros.succ, hornerAt.cons, ih, monoidPow.succ]72    ring7374theorem complexPowerRoots.graph (c : Set, k : Nat)75  shows complexPowerRoots(c, k) =76    hornerRoots{complexCarrier}(complexAdd, complexZero, complexMul, complexOne,77      complexNeg(c) :: complexZeros(k))78proof79  simp [complexPowerRoots]8081theorem complexUnityRoots.graph (k : Nat)82  shows complexUnityRoots(k) = complexPowerRoots(complexOne, k)83proof84  simp [complexUnityRoots]8586theorem complexPowerRoots.contains (z c : Set) (k : Nat)87  requires member : z ∈ complexCarrier88  requires target : c ∈ complexCarrier89  requires power : monoidPow(complexMul, complexOne, z, succ(k)) = c90  shows z ∈ complexPowerRoots(c, k)91proof92  have ring := complexes.comm_ring93  have ordinary := IsCommRing.ring with ring94  have oneIn := complexOne.member95  have negIn := IsRing.neg_closed with ordinary, target96  have zeroIn := complexZero.member97  have tail := complexZeros.list at k98  have value := hornerAt.zeros with member99  rw monoidPow.succ at power100  have vanishes : hornerAt{complexCarrier}(complexAdd, complexMul, complexOne, z,101      complexNeg(c) :: complexZeros(k)) = complexZero102    rw [hornerAt.cons, value, power]103    ring104  rw complexPowerRoots.graph105  exact hornerRoots.membership.backward with ⟨member, vanishes⟩106107theorem complexPowerRoots.finite (c : Set, k : Nat)108  requires target : c ∈ complexCarrier109  shows Finite(complexPowerRoots(c, k))110proof111  have field := complexes.is_field112  have ring := complexes.comm_ring113  have ordinary := IsCommRing.ring with ring114  have oneIn := complexOne.member115  have negIn := IsRing.neg_closed with ordinary, target116  have zeroIn := complexZero.member117  have tail := complexZeros.list at k118  have distinct := Nontrivial.distinct with complexes.nontrivial119  have nonzero : complexOne ≠ complexZero120    intro same121    symm at same122    exact distinct with same123  rw complexPowerRoots.graph124  exact hornerRoots.finite with field, oneIn, nonzero125126theorem complexUnityRoots.contains (z : Set) (k : Nat)127  requires member : z ∈ complexCarrier128  requires power : monoidPow(complexMul, complexOne, z, succ(k)) = complexOne129  shows z ∈ complexUnityRoots(k)130proof131  have oneIn := complexOne.member132  rw complexUnityRoots.graph133  exact complexPowerRoots.contains with member, oneIn, power134135theorem complexUnityRoots.finite (k : Nat)136  shows Finite(complexUnityRoots(k))137proof138  have oneIn := complexOne.member139  rw complexUnityRoots.graph140  exact complexPowerRoots.finite with oneIn141142end Complexes143