Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Taylor polynomials match the prescribed derivatives at the centre

Statement

For 0≤r≤n0\le r\le n, (Tn,af)(r)(x)=∑j=rnf(j)(a)ι((j−r)!)(x−a)j−r.(T_{n,a}f)^{(r)}(x)=\sum_{j=r}^{n}\frac{f^{(j)}(a)}{\iota((j-r)!)}(x-a)^{j-r}. Consequently (Tn,af)(r)(a)=f(r)(a)(T_{n,a}f)^{(r)}(a)=f^{(r)}(a), and Rn,afR_{n,a}f and its derivatives through order nn vanish at aa.

Facts & Assumptions

Given: The Taylor polynomial of Taylor polynomials and their remainders.

[L1]

Natural powers differentiate as in For a natural n≥1n \ge 1 the function x↦xnx \mapsto x^{n} is differentiable everywhere with derivative ι(n) x n−1\iota(n)\,x^{\,n-1}; for n=0n = 0 it is the constant 11, with derivative 00; for a natural n≥1n \ge 1 the function x↦x−nx \mapsto x^{-n} is differentiable at every x≠0x \ne 0 with derivative −ι(n) x−n−1-\iota(n)\,x^{-n-1}; consequently every polynomial function is differentiable at every real, with the derivative computed term by term; applying the chain rule to x↦x−ax\mapsto x-a, whose derivative is 11, gives the same shifted-power formula; and finite sums differentiate termwise by The chain rule, in one line from Carathéodory: if gg is differentiable at cc and ff is differentiable at g(c)g(c), then f∘gf \circ g is differentiable at cc with (f∘g)′(c)=f′(g(c)) g′(c)(f \circ g)'(c) = f'(g(c))\,g'(c) and Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c)(f+g)'(c) = f'(c) + g'(c), (αf)′(c)=αf′(c)(\alpha f)'(c) = \alpha f'(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c)(fg)'(c) = f'(c)g(c) + f(c)g'(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2} when g(c)≠0g(c) \ne 0.

[L2]

Falling factorials cancel factorials according to The factorial n!n! and the falling factorial nk‾n^{\underline{k}}, defined by recursion in N\mathbb{N}; finite sums reindex by Laws of finite sums and finite products.

Proof

technique · induction
1.1

At r=0r=0 the formula is the definition.

basegiven
1.2

Assuming the formula at r<nr<n, differentiate termwise. The term indexed jj acquires ι(j−r)\iota(j-r), which cancels ι((j−r)!)\iota((j-r)!) to ι((j−r−1)!)\iota((j-r-1)!); the j=rj=r constant term disappears. This is the formula at r+1r+1.

ihL1L2algebra
2.1

At x=ax=a, only the j=rj=r term survives and equals f(r)(a)f^{(r)}(a). Subtraction from f(r)(a)f^{(r)}(a) gives the remainder assertion.

step 1.2L1algebra
3.1

The formula and both consequences hold through order nn.

step 1.1step 2.1discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 90 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources