Grace/Cumulus/Algebra/Polynomial/BundledRoots.g17

Open in Workbench Download source

Imports

BundledEvaluation · HornerPolynomial · FactorTheorem

Declarations

Source

1-- One-variable polynomials over a bundled ring in Horner form: the value2-- horner(R, leading, x, cs), the synthetic quotient, the remainder and3-- factor theorems, the polynomial hornerPolynomial(R, I, j, leading, cs) of4-- polynomialRing(R, I) with that value, and over a field the finiteness of5-- the root set rootSet(R, leading, cs); everything here is ZF6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Polynomial.BundledRoots12import BundledEvaluation13import HornerPolynomial14import FactorTheorem1516-- cs lists the lower coefficients and leading is the coefficient of the17-- top power, so horner(R, leading, x, c :: cs) = c + x * horner(…, cs).18def horner (R leading x cs : Set) : Set :=19  hornerAt{R.carrier}(R.add, R.mul, leading, x, cs)20def syntheticQuotient (R leading a cs : Set) : Set :=21  hornerQuotient{R.carrier}(R.add, R.mul, leading, a, cs)22def rootSet (R leading cs : Set) : Set :=23  hornerRoots{R.carrier}(R.add, R.zero, R.mul, leading, cs)24def hornerPolynomial (R I j leading cs : Set) : Set :=25  polynomialFromHorner(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j,26    leading, cs)2728theorem horner.graph (R leading x cs : Set)29  shows horner(R, leading, x, cs) =30    hornerAt{R.carrier}(R.add, R.mul, leading, x, cs)31proof32  simp [horner]3334theorem syntheticQuotient.graph (R leading a cs : Set)35  shows syntheticQuotient(R, leading, a, cs) =36    hornerQuotient{R.carrier}(R.add, R.mul, leading, a, cs)37proof38  simp [syntheticQuotient]3940theorem rootSet.graph (R leading cs : Set)41  shows rootSet(R, leading, cs) =42    hornerRoots{R.carrier}(R.add, R.zero, R.mul, leading, cs)43proof44  simp [rootSet]4546theorem hornerPolynomial.graph (R I j leading cs : Set)47  shows hornerPolynomial(R, I, j, leading, cs) =48    polynomialFromHorner(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j,49      leading, cs)50proof51  simp [hornerPolynomial]5253section Rings54variable (R leading : Set)55hypothesis comm : CommRing(R)56hypothesis initial : leading ∈ R5758theorem horner.nil (x : R)59  shows horner(R, leading, x, []) = leading60proof61  rw horner.graph62  exact hornerAt.nil6364theorem horner.cons (x c : R) (cs : List(R.carrier))65  shows horner(R, leading, x, c :: cs) = c + x * horner(R, leading, x, cs)66proof67  have cIn : c ∈ R by assumption68  rw [horner.graph, horner.graph]69  exact hornerAt.cons with cIn7071instance horner.mem (x : R) (cs : List(R.carrier))72  shows horner(R, leading, x, cs) ∈ R73proof74  have parts := CommRing.parts with comm75  have xIn : x ∈ R by assumption76  rw horner.graph77  exact hornerAt.closed with parts, initial, xIn7879theorem syntheticQuotient.list (a : R) (cs : List(R.carrier))80  shows List(R.carrier, syntheticQuotient(R, leading, a, cs))81proof82  have parts := CommRing.parts with comm83  have aIn : a ∈ R by assumption84  rw syntheticQuotient.graph85  exact hornerQuotient.closed with parts, initial, aIn8687-- The remainder theorem: dividing by X - a leaves the remainder p(a).88theorem horner.remainder (a x c : R) (cs : List(R.carrier))89  shows horner(R, leading, x, c :: cs) = horner(R, leading, a, c :: cs) +90    (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))91proof92  have parts := CommRing.parts with comm93  have aIn : a ∈ R by assumption94  have xIn : x ∈ R by assumption95  have cIn : c ∈ R by assumption96  have engine := remainder.theorem with parts, initial, aIn, xIn, cIn97  have ordinary := CommRing.to_ring with comm98  rw [Ring.sub.value, horner.graph, horner.graph, horner.graph,99    syntheticQuotient.graph]100  exact engine101102-- The factor theorem: at a root a, X - a divides p with the synthetic103-- quotient, and conversely such a factorization forces the root.104theorem horner.factor (a x c : R) (cs : List(R.carrier))105  requires root : horner(R, leading, a, c :: cs) = R[0]106  shows horner(R, leading, x, c :: cs) =107    (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))108proof109  have parts := CommRing.parts with comm110  have aIn : a ∈ R by assumption111  have xIn : x ∈ R by assumption112  have cIn : c ∈ R by assumption113  rw horner.graph at root114  have engine := factor.theorem with parts, initial, aIn, xIn, cIn, root115  have ordinary := CommRing.to_ring with comm116  rw [Ring.sub.value, horner.graph, horner.graph, syntheticQuotient.graph]117  exact engine118119theorem horner.root_of_factor (a c : R) (cs : List(R.carrier))120  requires factor : ∀ x ∈ R, horner(R, leading, x, c :: cs) =121    (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))122  shows horner(R, leading, a, c :: cs) = R[0]123proof124  have parts := CommRing.parts with comm125  have ordinary := CommRing.to_ring with comm126  have aIn : a ∈ R by assumption127  have cIn : c ∈ R by assumption128  have engineFactor : ∀ x ∈ R,129      hornerAt{R.carrier}(R.add, R.mul, leading, x, c :: cs) =130      (x + -a) * hornerAt{R.carrier}(R.add, R.mul, leading, x,131        hornerQuotient{R.carrier}(R.add, R.mul, leading, a, cs))132    intros x hx133    have value := factor with x, hx134    rw [Ring.sub.value, horner.graph] at value135    rw [horner.graph, syntheticQuotient.graph] at value136    exact value137  rw horner.graph138  exact factor.root with parts, initial, aIn, cIn, engineFactor139140-- The Horner form as an element of the polynomial ring in the variable j.141section Polynomials142variable (I j : Set)143144theorem hornerPolynomial.mem (cs : List(R.carrier))145  shows hornerPolynomial(R, I, j, leading, cs) ∈ polynomialRing(R, I)146proof147  have parts := CommRing.parts with comm148  rw [hornerPolynomial.graph, polynomialRing.carrierOf]149  exact polynomialFromHorner.member with parts, initial150151theorem hornerPolynomial.cons (c : R) (cs : List(R.carrier))152  shows hornerPolynomial(R, I, j, leading, c :: cs) =153    Ring.add(polynomialRing(R, I))(polynomialConstant(R, I)(c),154      Ring.mul(polynomialRing(R, I))(X(R, I, j),155        hornerPolynomial(R, I, j, leading, cs)))156proof157  have parts := CommRing.parts with comm158  have cIn : c ∈ R by assumption159  rw [hornerPolynomial.graph, hornerPolynomial.graph, polynomialRing.addOf,160    polynomialRing.mulOf, polynomialConstant.apply, X.value]161  exact polynomialFromHorner.cons with parts, initial, cIn162163theorem hornerPolynomial.eval (v : Set) (cs : List(R.carrier))164  requires assignment : v : I → R.carrier165  requires index : j ∈ I166  shows evaluationAt(R, I, v)(hornerPolynomial(R, I, j, leading, cs)) =167    horner(R, leading, v(j), cs)168proof169  have parts := CommRing.parts with comm170  rw [hornerPolynomial.graph, evaluationAt.graph, horner.graph]171  exact polynomialAt.from_horner with parts, initial, assignment, index172173end Polynomials174end Rings175176section Fields177variable (R leading : Set)178hypothesis field : Field(R)179hypothesis initial : leading ∈ R180hypothesis nonzero : leading ≠ R[0]181182theorem rootSet.membership (x : Set) (cs : List(R.carrier))183  shows x ∈ rootSet(R, leading, cs) ↔184    x ∈ R ∧ horner(R, leading, x, cs) = R[0]185proof186  rw [rootSet.graph, horner.graph]187  exact hornerRoots.membership188189-- A nonzero polynomial over a field has finitely many roots, so over an190-- infinite field it takes a nonzero value.191theorem rootSet.finite (cs : List(R.carrier))192  shows Finite(rootSet(R, leading, cs))193proof194  have isField := Field.parts with field195  rw rootSet.graph196  exact hornerRoots.finite with isField, initial, nonzero197198theorem horner.exists_nonzero (cs : List(R.carrier))199  requires infinite : ¬Finite(R)200  shows ∃ x ∈ R, horner(R, leading, x, cs) ≠ R[0]201proof202  have isField := Field.parts with field203  obtain ⟨x, xIn, value⟩ := hornerAt.exists_nonzero with isField, initial,204    nonzero, infinite205  refine ⟨x, xIn, ?_⟩206  rw horner.graph207  exact value208209end Fields210