Correctness of Horner's evaluation scheme

Proved

MetodosNumericos.horner_eval

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

numerical-analysispolynomials

For every coefficient family $a$ , degree $n$ and point $z$ , the last Horner coefficient equals the value of the polynomial: $b_n = P(z)$ , where $b_0 = a_0$ and $b_i = a_i + z\\,b_{i-1}$ . This is the correctness of the algorithm of §4.5.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_polinomiosDefs

Formal statement

namespace MetodosNumericos

theorem horner_eval (a : ℕ → ℝ) (n : ℕ) (z : ℝ) :
    polyVal a n z = hornerSeq a z n := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 4, §4.4–4.5, pp. 77–79.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

For an arbitrary $a : \\mathbb{N} \\to \\mathbb{R}$ , an arbitrary natural number $n$ and an arbitrary real $z$ , the statement asserts the equality

\\sum_{i=0}^{n} a_i\\, z^{\\,n-i} \\;=\\; b_n,

where $b$ is the sequence with $b_0 = a_0$ and $b_{i+1} = a_{i+1} + z\\,b_i$ . There are no hypotheses at all; the case $n = 0$ asserts $a_0 = a_0$ .

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph