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.

Higher-order Rolle theorem

Statement

Let n∈Nn\in\mathbb N with n≥1n\ge1, let x0<⋯<xnx_0<\cdots<x_n, and let ff be continuous on [x0,xn][x_0,x_n] and nn-times differentiable on (x0,xn)(x_0,x_n). If f(xj)=0f(x_j)=0 for every j≤nj\le n, then some c∈(x0,xn)c\in(x_0,x_n) satisfies f(n)(c)=0f^{(n)}(c)=0.

Facts & Assumptions

Given: The ordered zeros and the stated regularity.

[L1]

Rolle's theorem produces a zero of h′h' between two zeros of a continuous, interior-differentiable function hh (Rolle's theorem: if a<ba < b, ff is continuous on [a,b][a,b], differentiable at every point of (a,b)(a,b), and f(a)=f(b)f(a) = f(b), then f′(c)=0f'(c) = 0 for some c∈(a,b)c \in (a,b)).

[L2]

Differentiability at a point implies continuity there (A function differentiable at cc is continuous at cc), and induction applies to natural numbers (The principle of mathematical induction).

Proof

technique · induction
1.1

For n=1n=1, Rolle's theorem on [x0,x1][x_0,x_1] gives c∈(x0,x1)c\in(x_0,x_1) with f′(c)=0f'(c)=0.

baseL1
1.2

For n≥2n\ge2, apply Rolle on each [xj−1,xj][x_{j-1},x_j] to obtain yj∈(xj−1,xj)y_j\in(x_{j-1},x_j) with f′(yj)=0f'(y_j)=0, so y1<⋯<yny_1<\cdots<y_n.

givenL1choose
2.1

The function f′f' is continuous on [y1,yn][y_1,y_n], because those points lie in (x0,xn)(x_0,x_n) and the existence of f′′f'' gives continuity there; it is (n−1)(n-1)-times differentiable on (y1,yn)(y_1,y_n). Apply the induction hypothesis of order n−1n-1 to f′f' and the nn ordered zeros y1,…,yny_1,\ldots,y_n. This gives c∈(y1,yn)⊂(x0,xn)c\in(y_1,y_n)\subset(x_0,x_n) with (f′)(n−1)(c)=f(n)(c)=0(f')^{(n-1)}(c)=f^{(n)}(c)=0.

step 1.2L2ih
3.1

The claim follows for every n≥1n\ge1.

step 1.1step 2.1L2discharge-induction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 61 results over 17 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