TheoremStatement: 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.

de Boor evaluation equals the B-spline coefficient expansion

Statement

Let $p \in N_{0}$ , let $t_{0} \leq \dots \leq t_{n + p}$ be the zero-based reindexing of a clamped knot vector, and let $S (x) = \sum_{i = 0}^{n - 1} c_{i} B_{i, p} (x)$ be its degree- $p$ B-spline expansion, with $B_{i, p} = B_{i + 1, p, ξ}$ under B-spline spaces and knot conventions. If $k$ is a nonempty span index and $x \in [t_{k}, t_{k + 1})$ , then the exact-arithmetic mode of de Boor coefficient evaluation on a specified knot span returns $S (x)$ . For $x = b$ it returns the corresponding left limit when the last nonempty span is supplied.

Facts & Assumptions

Given: A clamped degree- $p$ knot vector, coefficients $c_{i}$ , a nonempty span $[t_{k}, t_{k + 1})$ , and a query in that half-open span, or the specified left limit at $b$ .

[F1]

de Boor coefficient evaluation on a specified knot span initializes the active list by $d_{j}^{(0)} = c_{k - p + j}$ and, in exact mode, updates $d_{j}^{(r)} = (1 - α_{j, r}) d_{j - 1}^{(r - 1)} + α_{j, r} d_{j}^{(r - 1)}$ with $α_{j, r} = (x - t_{k - p + j}) / (t_{k + 1 + j - r} - t_{k - p + j})$ .

[F2]

B-spline spaces and knot conventions defines degree-zero B-splines as half-open interval indicators and gives the Cox–de Boor recurrence; a zero-denominator term is zero.

[F3]

B-spline basis properties and polynomial reproduction states that on a nonempty span only $B_{k - p, p}, \dots, B_{k, p}$ can be active.

[A1]

The algorithm is run in exact arithmetic and the supplied span is nonempty.

Proof

1.1givenA1F1F3

By [F3], on the supplied span the spline value is the sum over its active indices only. With $d_{j}^{(0)} = c_{k - p + j}$ , this is $S (x) = \sum_{j = 0}^{p} d_{j}^{(0)} B_{k - p + j, p} (x)$ . If $p = 0$ , the sole active degree-zero indicator equals one on the half-open span, so the algorithm's copy $c_{k}$ is exactly $S (x)$ .

1.2A1F2algebra

Suppose a current degree- $q$ local expansion has active coefficients $a_{k - q}, \dots, a_{k}$ . Expand each basis function by [F2]. For every $i = k - q + 1, \dots, k$ , the coefficient of $B_{i, q - 1} (x)$ after collecting the two contributing terms is $\frac{(x - t_{i}) a_{i} + (t_{i + q} - x) a_{i - 1}}{t_{i + q} - t_{i}} = (1 - \frac{x - t_{i}}{t_{i + q} - t_{i}}) a_{i - 1} + \frac{x - t_{i}}{t_{i + q} - t_{i}} a_{i}$ . The two boundary terms are zero on $[t_{k}, t_{k + 1})$ : the left one is supported only up to $t_{k}$ , and the right one starts at $t_{k + 1}$ . A zero denominator contributes zero by [F2]. Thus this degree reduction preserves the value at $x$ .

2.1A1F1F2step 1.2induction∎

Starting at $q = p$ , repeat step 1.2. After $r - 1$ reductions the active degree is $q = p - r + 1$ , and the coefficient indexed by $i = k - p + j$ has the weight $(x - t_{k - p + j}) / (t_{k + 1 + j - r} - t_{k - p + j})$ , exactly $α_{j, r}$ in [F1]. Hence each algorithmic update is the coefficient collection in step 1.2 and preserves the spline value. After $p$ reductions the sole degree-zero indicator on the span is one, so the remaining coefficient $d_{p}^{(p)}$ equals $S (x)$ . At $b$ equality on the last open span extends to the prescribed left limit.

Depends on

Used by

Dependency tree · two levels

4 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

Carl de Boor, A Practical Guide to Splines, revised edition, Chapter X, pp. 123–126 (standard reference, not scraped)
Tom Lyche, Carla Manni, and Hendrik Speleers, B-Splines and Spline Approximation, §1.1 (standard reference, not scraped)