PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

Equispaced interpolation has linearly growing basis amplification

Statement

Let $m \in N$ with $m \geq 6$ , and take the $2 m + 1$ nodes $x_{k} = - 1 + \frac{k}{m}, 0 \leq k \leq 2 m .$ They are equally spaced in $[- 1, 1]$ . Let $ℓ_{m}$ be the cardinal function for the node $x_{m} = 0$ , and set $x_{*} = - 1 + \frac{1}{2 m} .$ Then $∣ ℓ_{m} (x_{*}) ∣ \geq \frac{9 m}{1280} .$ In these real formulas, natural numbers and binomial coefficients denote their canonical real images, as specified by The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , and Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ .

Facts & Assumptions

Given: $m \geq 6$ , the specified equispaced nodes, and the corresponding cardinal function.

[F1]

Cardinal-polynomial interpolation: $ℓ_{m} (X) = \prod_{k \neq m} (X - x_{k}) / (x_{m} - x_{k})$ , with the omitted-index product ordered as its length- $2 m$ list.

[F2]

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ : $(\binom{n}{k})$ is a natural number for $0 \leq k \leq n$ .

[F3]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ : factorials are products of positive naturals, $n^{\underline{k}}$ is the product of the top $k$ factors when $k \leq n$ , and $n!_{R} : = \prod_{j = 1}^{n} j$ is the corresponding real product.

[F4]

$(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ : for $k \leq n$ , the real binomial coefficient is $(\binom{n}{k}) = n!_{R} / (k!_{R} (n - k)!_{R})$ , and the natural identity $(\binom{n}{k}) k! = n^{\underline{k}}$ holds.

[F5]

The binomial coefficients are symmetric and increase to the middle level before decreasing: for even $r$ , the coefficient $(\binom{r}{r / 2})$ is at least every coefficient in that binomial row.

[F6]

The binomial theorem over an arbitrary commutative ring: $(u + v)^{r} = \sum_{k = 0}^{r} (\binom{r}{k}) u^{k} v^{r - k}$ in every commutative ring.

[F7]

The reals form a field and Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring: $R$ is a commutative ring with the field operations.

[F8]

The reals form a totally ordered field: real order is total and compatible with field addition and multiplication by positive numbers.

[F9]

Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ and The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: the canonical real images preserve natural addition, multiplication, and order, and carry finite natural sums and products to the corresponding real sums and products.

[F10]

Laws of finite sums and finite products: finite real sums preserve termwise inequalities, and each nonnegative term is at most the sum.

[F11]

Laws of integer exponents: real powers obey the natural exponent laws used to combine $2^{4 m}$ with $16^{m}$ .

Proof

technique · direct

1.1givenF8F9algebra

Put $M = m > 0$ . Since $x_{k + 1} - x_{k} = 1 / M > 0$ , the nodes increase from $- 1$ to $1$ , and $x_{m} = 0$ . If $x_{*} = x_{k}$ , then $1 = 2 k$ ; for $k = 0$ the right side is $0$ , while for $k \geq 1$ it is at least $2$ , by [F8, F9]. Thus $x_{*}$ is not a node.

1.2givenF1F3F4F9F11algebra

For $k \neq m$ , $∣ \frac{x_{*} - x_{k}}{x_{m} - x_{k}} ∣ = \frac{∣ \frac{1}{2} - k ∣}{∣ m - k ∣} .$ The denominator product is $(m!_{R})^{2}$ , where $m!_{R} = \prod_{j = 1}^{m} j$ . In the numerator, the $k = 0$ factor is $1 / 2$ and the remaining factors are $k - 1 / 2$ for $1 \leq k \leq 2 m$ , with $k = m$ omitted. Pairing the odd factors gives $\prod_{\begin{array}{c} 0 \leq k \leq 2 m \\ k \neq m \end{array}} ∣ \frac{1}{2} - k ∣ = \frac{(4 m)!_{R}}{(2 m - 1) 16^{m} (2 m)!_{R}} .$ Using [F3, F4] to rewrite the factorial ratios yields the exact identity $∣ ℓ_{m} (x_{*}) ∣ = \frac{(\binom{4 m}{2 m}) (\binom{2 m}{m})}{(2 m - 1) 16^{m}} .$

1.3givenF2F5F6F7F9F10F11algebra

Apply [F6] in the commutative ring $R$ [F7] with $u = v = 1$ . The sum of the $r$ th binomial row is $2^{r}$ . For $r = 4 m$ and $r = 2 m$ , [F5] says the central term is largest; each coefficient is nonnegative by [F2, F9], so [F10] bounds the row sum above by $(r + 1)$ times its central term. Consequently $(\binom{4 m}{2 m}) \geq \frac{16^{m}}{4 m + 1}, (\binom{2 m}{m}) \geq \frac{4^{m}}{2 m + 1} .$

1.4givenF2F3F4F6F7F8F9F10algebra

By [F6, F7], $4^{m} = (1 + 3)^{m} = \sum_{k = 0}^{m} (\binom{m}{k}) 3^{k} \geq 81 (\binom{m}{4}) .$ Here every summand is nonnegative by [F2, F8, F9], and the inequality retains the $k = 4$ term using [F10]. From [F3, F4], $(\binom{m}{4}) = m (m - 1) (m - 2) (m - 3) / 24$ . Since $m \geq 6$ , each of these four factors is at least $m / 2$ , so $(\binom{m}{4}) \geq m^{4} / 384$ . Therefore $4^{m} \geq 81 m^{4} / 384$ .

2.1step 1.2step 1.3F8F9algebra

Substituting step 1.3 in step 1.2 gives $∣ ℓ_{m} (x_{*}) ∣ \geq \frac{4^{m}}{(2 m - 1) (4 m + 1) (2 m + 1)} \geq \frac{4^{m}}{30 m^{3}},$ because the three denominator factors are at most $2 m$ , $5 m$ and $3 m$ , respectively.

3.1step 2.1step 1.4algebra∎

Combining step 1.4 with step 2.1 yields $∣ ℓ_{m} (x_{*}) ∣ \geq 81 m / (384 \cdot 30) = 9 m / 1280$ , as claimed.

Depends on

Used by

Unit nodal data exhibit equispaced cardinal basis growth Example

Dependency tree · two levels

78 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

Mark Embree, Lecture Notes on Numerical Analysis, uniformly spaced nodes example (standard reference, not scraped)
Jean-Paul Berrut and Lloyd N. Trefethen, Barycentric Lagrange Interpolation (standard reference, not scraped)