Grace/Cumulus/Complex/FundamentalTheoremGeneral.g17

Open in Workbench Download source

Imports

FundamentalTheorem · Algebra.Polynomial.HornerNormalization

Declarations

Source

1-- The fundamental theorem of algebra for every nonconstant complex polynomial.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.FundamentalTheoremGeneral8import FundamentalTheorem9import Algebra.Polynomial.HornerNormalization1011section Complexes12notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1314-- A product with a unit's partner vanishes only at zero.15theorem complex.zero_of_inverse_mul (b c v : Set)16  requires bIn : b ∈ ℂ17  requires cIn : c ∈ ℂ18  requires vIn : v ∈ ℂ19  requires cancels : ℂ[b * c] = ℂ[1]20  requires product : ℂ[b * v] = ℂ[0]21  shows v = ℂ[0]22proof23  linear_combination c * product - v * cancels2425-- Scaling the leading coefficient and every lower coefficient by b scales26-- the value of the polynomial by b.27theorem complexPolynomial.leading_scale (b c x : Set) (cs : List(ℂ))28  requires bIn : b ∈ ℂ29  requires cIn : c ∈ ℂ30  requires xIn : x ∈ ℂ31  shows hornerAt{ℂ}(complexAdd, complexMul, ℂ[b * c], x, ringScale{ℂ}(complexMul, b, cs)) =32    ℂ[b * hornerAt{ℂ}(complexAdd, complexMul, c, x, cs)]33proof34  have ring := complexes.comm_ring35  have hom := IsRingHom.identity with ring36  have scaled := hornerValue.scale at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne,37    complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne,38    identity(complexCarrier), x, b, c, cs with *39  have bValue := identity.apply with bIn40  rw bValue at scaled41  unfold hornerAt42  cc4344-- Scaling preserves nonemptiness of the coefficient list.45theorem complexPolynomial.scaled_nonempty (b : Set) (cs : List(ℂ))46  requires bIn : b ∈ ℂ47  requires nonconstant : cs ≠ []48  shows ringScale{ℂ}(complexMul, b, cs) ≠ []49proof50  have cases := List.cases with *51  cases cases with empty | cons52  . exfalso53    exact nonconstant with empty54  . obtain ⟨d, dIn, tail, tailList, shape⟩ := cons55    have productIn : ℂ[b * d] ∈ ℂ by typecheck56    have scaleClosed : ∀ u ∈ ℂ, ℂ[b * u] ∈ ℂ57      intros u uIn58      typecheck59    have scaledTail := ringScale.closed at complexCarrier, complexMul, b, tail with scaleClosed60    rw [shape, ringScale]61    intro equal62    symm at equal63    exact List.inductive.disjoint.nil.cons at ℂ[b * d],64      ringScale{ℂ}(complexMul, b, tail) with equal6566-- The fundamental theorem of algebra with an arbitrary nonzero leading67-- coefficient c: cs lists the lower coefficients in ascending order, so the68-- polynomial is c X^n + cs(n-1) X^(n-1) + ... + cs(0) with n = length(cs) ≥ 1.69theorem complexes.fundamental_theorem_of_algebra_general (c : Set) (cs : List(ℂ))70  requires leading : c ∈ ℂ71  requires nonzero : c ≠ ℂ[0]72  requires nonconstant : cs ≠ []73  shows ∃ a ∈ ℂ, hornerAt{ℂ}(complexAdd, complexMul, c, a, cs) = ℂ[0]74proof75  have field := complexes.is_field76  have ring := complexes.comm_ring77  obtain ⟨b, inverse⟩ := IsField.inverse_exists with field, leading, nonzero78  have bIn := inverse.right.left79  have cancels := inverse.right.right.left80  have scaleClosed : ∀ u ∈ ℂ, ℂ[b * u] ∈ ℂ81    intros u uIn82    typecheck83  have scaledList := ringScale.closed with *84  have scaledNonempty := complexPolynomial.scaled_nonempty with bIn, nonconstant85  obtain ⟨a, aIn, root⟩ := complexes.fundamental_theorem_of_algebra at86    ringScale{ℂ}(complexMul, b, cs) with *87  have monicRoot : hornerAt{ℂ}(complexAdd, complexMul, ℂ[1], a, ringScale{ℂ}(complexMul, b, cs)) = ℂ[0]88    unfold hornerAt89    cc90  have scaled := complexPolynomial.leading_scale at b, c, a, cs with *91  rw [cancels, monicRoot] at scaled92  have valueIn := hornerAt.closed at93    complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, c, a, cs with *94  symm at scaled95  refine ⟨a, aIn, ?_⟩96  exact complex.zero_of_inverse_mul with bIn, leading, valueIn, cancels, scaled9798end Complexes99100-- The same theorem for a single ascending coefficient list cs representing101-- cs(0) + cs(1) X + ... : a nonzero coefficient of X^(n+1) makes the102-- polynomial nonconstant, whatever zeros follow it.103theorem complexes.fundamental_theorem_of_algebra_coefficients (cs : List(complexCarrier)) (n : Nat)104  requires nonconstant : listCoefficient{complexCarrier}(complexZero, cs, n + 1) ≠ complexZero105  shows ∃ a ∈ complexCarrier,106    hornerAt{complexCarrier}(complexAdd, complexMul, complexZero, a, cs) = complexZero107proof108  have ring := complexes.comm_ring109  have successor := add.right_one at n110  rw successor at nonconstant111  have cases := List.cases with *112  cases cases with empty | cons113  . exfalso114    rw [empty, listCoefficient.nil] at nonconstant115    apply nonconstant116    rfl117  . obtain ⟨d, dIn, tail, tailList, shape⟩ := cons118    rw [shape, listCoefficient.succ] at nonconstant119    have tailNonzero : ∃ m, Nat(m) ∧ listCoefficient{complexCarrier}(complexZero, tail, m) ≠ complexZero120      refine ⟨n, assumption, nonconstant⟩121    obtain ⟨leading, leadingIn, nonzero, lower, lowerList, equal⟩ := hornerAt.normalize at122      complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, tail with *123    have consNonempty : d :: lower ≠ []124      intro same125      symm at same126      exact List.inductive.disjoint.nil.cons at d, lower with same127    obtain ⟨a, aIn, root⟩ := complexes.fundamental_theorem_of_algebra_general at128      leading, d :: lower with *129    have value := equal with a, aIn130    refine ⟨a, aIn, ?_⟩131    rw [shape, hornerAt.cons, value]132    rw hornerAt.cons at root133    exact root134