Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
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.

Bounded integer-grid values control excursions by the derivative

Statement

Let N≥1 be an integer and let q be a real polynomial. On [0,N], set h:=max⁡q−min⁡q,D:=max⁡∣q′∣. If 0≤q(k)≤1 for every integer k=0,…,N, then D≥max⁡{0,h−1}.

Facts & Assumptions

Given: An integer N≥1, a real polynomial q, and the grid bounds 0≤q(k)≤1 for k=0,…,N.

[F1]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials and For a natural n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(n) x−n−1; consequently every polynomial function is differentiable at every real, with the derivative computed term by term: a real polynomial is a finite coefficient list evaluated by powers, and its real function is differentiable everywhere with derivative a polynomial function.

[F2]

Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function: every polynomial function is continuous, and so is the absolute value of a continuous function.

[F3]

Extreme value theorem: a continuous real function on a nonempty compact subset of R attains a greatest and a least value: a continuous real function on the nonempty compact interval [0,N] attains its maximum and minimum.

[F4]

The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a): if a function is continuous on a closed interval and differentiable in its interior, its endpoint difference equals its derivative at an interior point times the interval length.

Proof

1.1givenF1F2F3

By [F1]–[F3], both q and ∣q′∣ are continuous on the compact interval [0,N]. Thus there exist u,v∈[0,N] with q(u)=max⁡q=:M, q(v)=min⁡q=:m, and D=max⁡∣q′∣. In particular h=M−m≥0 and D≥0.

1.2givenF4choose

For any x∈[0,N], some grid integer k∈{0,…,N} satisfies ∣x−k∣≤1/2 (choose a nearest integer, with an endpoint grid point at either boundary). Applying [F4] on the interval between x and k when they differ gives ∣q(x)−q(k)∣≤D∣x−k∣≤D/2; equality of the points gives the same inequality directly.

2.1step 1.1algebra

If h≤1, then max⁡{0,h−1}=0≤D. It remains to consider h>1.

3.1step 1.1step 1.2algebra∎

Apply step 1.2 at a maximizer u and a minimizer v. The grid bounds give M≤1+D/2 and m≥−D/2, so h=M−m≤1+D. Rearranging yields D≥h−1.

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources