Grace/Cumulus/Algebra/Polynomial/HornerVanishing.g17

Open in Workbench Download source

Imports

HornerTranslation · Group.Power

Declarations

• hornerAt.first_nonzero theorem derivation

Source

1-- Extract the first nonzero term without choosing a coefficient or a degree.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.HornerVanishing8import HornerTranslation9import Group.Power1011section Rings12variable (A add zero neg mul one leading : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)15hypothesis initial : leading ∈ R16hypothesis nonzero : leading ≠ R[0]1718-- The remaining Horner polynomial has nonzero constant coefficient. Its19-- degree plus the extracted multiplicity is exactly the original degree.20theorem hornerAt.first_nonzero (cs : List(A))21  shows ∃ n ∈ ℕ, ∃ ds, List(A, ds) ∧ listHeadOr{A}(leading, ds) ≠ R[0] ∧22    length{A}(cs) = Grace.Core.Nat.Rec.add(n, length{A}(ds)) ∧23    (∀ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) = R[monoidPow(R, x, n) * hornerAt{A}(add, mul, leading, x, ds)])24proof25  have ordinary := IsCommRing.ring with ring26  have monoid := IsRing.multiplicative with ordinary27  induction cs28  | List.nil =>29    have zeroNat : (0:N) ∈ ℕ by typecheck30    have empty : List(A, []) by typecheck31    have head : listHeadOr{A}(leading, []) ≠ R[0] by rwa listHeadOr32    refine ⟨(0:N), zeroNat, [], empty, head, ?_⟩33    constructor34    . rw add.left_unit35      rfl36    . intros x member37      rw [monoidPow.zero, hornerAt.nil]38      ring39  | List.cons(c, tail) using ih =>40    have coefficient : c ∈ R by assumption41    have list : List(A, c :: tail) by typecheck42    have comparison : c = R[0] ∨ c ≠ R[0] by tauto43    cases comparison with vanishes | survives44    . obtain ⟨n, nIn, ds, dsList, head, degree, factor⟩ := ih45      have nNat := nat.omega.backward at n with *46      have next : succ(n) ∈ ℕ by typecheck47      refine ⟨succ(n), next, ds, dsList, head, ?_⟩48      constructor49      . rw [length.cons, degree, Grace.Core.Nat.Rec.add]50        rfl51      . intros x member52        have ordinary := IsCommRing.ring with ring53        have monoid := IsRing.multiplicative with ordinary54        have power := monoidPow.closed at A, mul, one, x, n with *55        have rest := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, ds with *56        have decomposition := factor with x, member57        rw [hornerAt.cons, vanishes, decomposition, monoidPow.succ]58        ring59    . have zeroNat : (0:N) ∈ ℕ60        typecheck61      have head : listHeadOr{A}(leading, c :: tail) ≠ R[0] by rwa listHeadOr62      refine ⟨(0:N), zeroNat, c :: tail, list, head, ?_⟩63      constructor64      . rw add.left_unit65        rfl66      . intros x member67        have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, c :: tail with *68        rw monoidPow.zero69        ring7071end Rings72