Grace/Cumulus/Algebra/Polynomial/HornerRoots.g17

Imports

Declarations

hornerRoots def
hornerRoots.nil theorem derivation
hornerRoots.divide theorem derivation
hornerRoots.finite_of_length theorem derivation
hornerRoots.finite theorem derivation
hornerAt.exists_nonzero theorem derivation
hornerAt.exists_nonzero_avoiding theorem derivation
Source

1-- Finite roots and nonvanishing of nonzero-leading Horner polynomials.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.Algebra.Polynomial.HornerRoots8import Horner910def hornerRoots {A : Set} (add z mul leading : Set) (cs : List(A)) : Set :=11  {x ∈ A | hornerAt{A}(add, mul, leading, x, cs) = z}1213theorem hornerRoots.nil (A add z mul leading : Set)14  requires nonzero : leading ≠ z15  shows hornerRoots{A}(add, z, mul, leading, []) = ∅16proof17  ext x18  have value := hornerAt.nil at A, add, mul, leading, x19  constructor20  . intro member21    have data := hornerRoots.membership.forward with member22    have equal := data.right23    rw value at equal24    exfalso25    exact nonzero with equal26  . intro impossible27    exfalso28    simp2930section Fields31variable (A add z neg mul one leading : Set)32notation ring R := (A, add, z, neg, mul, one)33hypothesis field : IsField(R)34hypothesis initial : leading ∈ R3536theorem hornerRoots.divide (a c : Set) (cs : List(A))37  requires center : a ∈ R38  requires coefficient : c ∈ R39  requires root : hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]40  shows hornerRoots{A}(add, z, mul, leading, c :: cs) ⊆ insert(a, hornerRoots{A}(add, z, mul, leading, hornerQuotient{A}(add, mul, leading, a, cs)))41proof42  have ring := IsField.comm_ring with field43  have ordinary := IsCommRing.ring with ring44  have quotient := hornerQuotient.closed at A, add, z, neg, mul, one, leading, a, cs with *45  have noZero := IsField.no_zero_divisors with field46  intros x hx47  obtain ⟨element, vanishes⟩ := hornerRoots.membership.forward at48    A, add, z, mul, leading, c :: cs, x with *49  have division := hornerAt.synthetic_division at A, add, z, neg, mul, one, leading, a, x, c, cs with *50  have value := hornerAt.closed at A, add, z, neg, mul, one, leading, x, hornerQuotient{A}(add, mul, leading, a, cs) with *51  have negative := IsRing.neg_closed with ordinary, center52  have difference := IsRing.add_closed with ordinary, element, negative53  rw [root, vanishes] at division54  have productZero : R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))] = R[0]55    linear_combination -division56  have alternatives := noZero with R[x - a], difference, hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs)), productZero57  cases alternatives with same | remaining58  . have equal : x = a59      linear_combination same60    rw equal61    exact insert.self62  . have member : x ∈ hornerRoots{A}(add, z, mul, leading, hornerQuotient{A}(add, mul, leading, a, cs))63      apply hornerRoots.membership.backward64      refine ⟨element, remaining⟩65    exact insert.contains with member6667hypothesis nonzero : leading ≠ R[0]6869theorem hornerRoots.finite_of_length (n : Nat) (cs : List(A))70  requires size : length{A}(cs) = n71  shows Finite(hornerRoots{A}(add, z, mul, leading, cs))72proof73  induction n generalizing cs74  | zero =>75    intros cs list size76    have cases := List.cases with list77    cases cases with empty | cons78    . rw [empty, hornerRoots.nil]79      exact Finite.empty80    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons81      rw [shape, length.cons] at size82      have impossible := Naturals.disjoint.zero.succ at length{A}(tail)83      exfalso84      apply impossible85      symm86      exact size87  | succ(k) using ih =>88    intros cs list size89    have cases := List.cases with list90    cases cases with empty | cons91    . rw [empty, hornerRoots.nil]92      exact Finite.empty93    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons94      have tailSize : length{A}(tail) = k95        rw [shape, length.cons] at size96        exact Naturals.injective.succ with size97      have alternatives : (∃ a, a ∈ hornerRoots{A}(add, z, mul, leading, cs)) ∨ ¬(∃ a, a ∈ hornerRoots{A}(add, z, mul, leading, cs))98        tauto99      cases alternatives with inhabited | emptyRoots100      . obtain ⟨a, ha⟩ := inhabited101        rw shape at ha102        obtain ⟨center, root⟩ := hornerRoots.membership.forward at103          A, add, z, mul, leading, c :: tail, a with *104        have ring := IsField.comm_ring with field105        have quotient := hornerQuotient.closed at A, add, z, neg, mul, one, leading, a, tail with *106        have quotientLength := hornerQuotient.length at A, add, z, neg, mul, one, leading, a, tail with *107        have quotientSize : length{A}(hornerQuotient{A}(add, mul, leading, a, tail)) = k by cc108        have finite := ih with hornerQuotient{A}(add, mul, leading, a, tail), quotientSize109        have inserted := Finite.insert at hornerRoots{A}(add, z, mul, leading, hornerQuotient{A}(add, mul, leading, a, tail)), a with finite110        have subset := hornerRoots.divide at A, add, z, neg, mul, one, leading, a, c, tail with *111        rw shape112        exact Finite.subset with inserted, subset113      . have empty : hornerRoots{A}(add, z, mul, leading, cs) = ∅114          ext x115          constructor116          . intro member117            exfalso118            apply emptyRoots119            refine ⟨x, member⟩120          . intro impossible121            exfalso122            exact set.empty with impossible123        rw empty124        exact Finite.empty125126theorem hornerRoots.finite (cs : List(A))127  shows Finite(hornerRoots{A}(add, z, mul, leading, cs))128proof129  have size : length{A}(cs) = length{A}(cs) by rfl130  exact hornerRoots.finite_of_length with *131132theorem hornerAt.exists_nonzero (cs : List(A))133  requires infinite : ¬Finite(R)134  shows ∃ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]135proof136  have finite := hornerRoots.finite with *137  by_contra absent138  have equal : hornerRoots{A}(add, z, mul, leading, cs) = R139    ext x140    constructor141    . intro member142      have data := hornerRoots.membership.forward with member143      exact data.left144    . intro member145      apply hornerRoots.membership.backward146      refine ⟨member, ?_⟩147      by_contra value148      apply absent149      refine ⟨x, member, value⟩150  rw equal at finite151  exact infinite with finite152153theorem hornerAt.exists_nonzero_avoiding (F : Set) (cs : List(A))154  requires infinite : ¬Finite(R)155  requires excluded : Finite(F)156  shows ∃ x ∈ R, ¬(x ∈ F) ∧ hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]157proof158  have roots := hornerRoots.finite with *159  have finite := Finite.union with excluded, roots160  by_contra absent161  have included : R ⊆ F ∪ hornerRoots{A}(add, z, mul, leading, cs)162    intros x hx163    have alternatives : x ∈ F ∨ ¬(x ∈ F) by tauto164    cases alternatives with forbidden | fresh165    . settle with union2.membership166    . have vanishes : hornerAt{A}(add, mul, leading, x, cs) = R[0]167        by_contra value168        apply absent169        refine ⟨x, hx, fresh, value⟩170      have root : x ∈ hornerRoots{A}(add, z, mul, leading, cs)171        apply hornerRoots.membership.backward172        refine ⟨hx, vanishes⟩173      simp174  have impossible := Finite.subset with finite, included175  exact infinite with impossible176177end Fields178