Pipeline-generated

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.

✓ 3 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

Spline evaluation and interpolation algorithms — Examples

1 · Prerequisites

2 · Summary

These examples work through a de Boor evaluation next to a double knot, show the natural boundary error for $x^{2}$ next to an endpoint, and verify that inserting a new knot leaves a linear B-spline curve unchanged.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

de Boor evaluation with a double knot

Example

Take degree $p = 2$ , knots $t_{0} = t_{1} = t_{2} = 0$ , $t_{3} = t_{4} = 1$ , and $t_{5} = t_{6} = t_{7} = 2$ , and coefficients $(c_{0}, c_{1}, c_{2}, c_{3}, c_{4}) = (0, 0, 4, 8, 0)$ . Evaluate at $x = 3 / 2$ on the nonempty span $[t_{4}, t_{5}) = [1, 2)$ . This span is adjacent to the double knot at $1$ .

Facts & Assumptions

Given: The degree, knot vector, coefficient list, span $[1, 2)$ , and query $x = 3 / 2$ from the Example.

[F1]

de Boor coefficient evaluation on a specified knot span initializes $d_{j}^{(0)} = c_{k - p + j}$ and uses the stated $α_{j, r}$ blend for $j = p, \dots, r$ .

[F2]

de Boor evaluation equals the B-spline coefficient expansion identifies the exact output with the B-spline coefficient expansion.

[F3]

B-spline spaces and knot conventions uses a clamped knot vector with half-open cells, right-side values at interior knots, and left limits at $b$ .

[A1]

$p = 2$ , $k = 4$ , $t_{0} = t_{1} = t_{2} = 0$ , $t_{3} = t_{4} = 1$ , $t_{5} = t_{6} = t_{7} = 2$ , and $(c_{0}, c_{1}, c_{2}, c_{3}, c_{4}) = (0, 0, 4, 8, 0)$ .

Verification

1.1givenA1F1F3

The input is admissible: [F3] allows the displayed clamped knot vector, including the double interior knot; the knots are nondecreasing and clamped for degree two; $t_{4} = 1 < t_{5} = 2$ ; and $x = 3 / 2 \in [1, 2)$ . By [F1], the initial active list is $(d_{0}^{(0)}, d_{1}^{(0)}, d_{2}^{(0)}) = (4, 8, 0)$ .

2.1A1F1step 1.1algebra

For $r = 1, j = 2$ , the indices are $L = 4, U = 6$ , so $α = (3 / 2 - t_{4}) / (t_{6} - t_{4}) = 1 / 2$ and $d_{2}^{(1)} = (8 + 0) / 2 = 4$ . For $r = 1, j = 1$ , $L = 3, U = 5$ , again $α = 1 / 2$ , so $d_{1}^{(1)} = (4 + 8) / 2 = 6$ .

3.1A1F1step 2.1algebra

For $r = 2, j = 2$ , $L = 4, U = 5$ and $α = 1 / 2$ . Therefore $d_{2}^{(2)} = (6 + 4) / 2 = 5$ , which is the algorithm's exact returned value.

4.1A1F2step 3.1algebra∎

By [F2], the B-spline curve value on the specified span is also $5$ . The example exercises a repeated knot without evaluating a basis function outside the active span.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The natural interpolant of x squared has a second-order endpoint error

Example

For $H > 0$ , interpolate $f (x) = x^{2}$ naturally at $0, H, 2 H$ . The error on the first interval is $H^{2} / 16$ at its midpoint, even though $f^{(4)} = 0$ . The clamped interpolant with exact endpoint slopes is $f$ itself. This displays why the fourth-order bound for the clamped method requires compatible boundary data.

Facts & Assumptions

Given: $H > 0$ , the data $(0, 0)$ , $(H, H^{2})$ , $(2 H, 4 H^{2})$ for $x^{2}$ , and the natural endpoint conditions.

[F1]

Natural cubic interpolation at distinct knots gives the natural second-derivative system and the cubic piece formula.

[F2]

Clamped cubic spline interpolation exists uniquely: for strictly increasing knots and prescribed endpoint slopes there is a unique clamped cubic interpolant.

[F3]

Boundary-compatible clamped cubic interpolation is fourth order in the maximum norm gives the fourth-order bound when the endpoint slopes equal those of the target function.

[A1]

The knots are $0, H, 2 H$ and the target function is $f (x) = x^{2}$ .

Verification

1.1A1F1algebra

The interval lengths are both $H$ , and the two secant slopes are $H$ and $3 H$ . The natural endpoint second derivatives are zero. The single interior equation from [F1] is $4 H M_{1} = 6 (3 H - H) = 12 H$ , hence $M_{1} = 3$ .

2.1A1F1step 1.1algebra

Substituting $M_{0} = 0$ , $M_{1} = 3$ , $y_{0} = 0$ , and $y_{1} = H^{2}$ into the first-interval formula in [F1] gives $s (x) = x^{3} / (2 H) + H x / 2$ . Thus $s (H / 2) = 5 H^{2} / 16$ whereas $f (H / 2) = H^{2} / 4 = 4 H^{2} / 16$ , so the absolute error is $H^{2} / 16 > 0$ .

3.1A1F2F3step 2.1algebra∎

Since $f^{(4)} = 0$ , a general natural-boundary estimate of the form $C H^{4} ∥ f^{(4)} ∥_{\infty}$ would force zero error, contradicting step 2.1. The polynomial $f$ has the prescribed clamped slopes $f^{'} (0) = 0$ and $f^{'} (2 H) = 4 H$ , so [F2] makes it the unique clamped interpolant; [F3] also gives zero error.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Inserting a knot leaves a linear B-spline curve fixed

Example

The degree-one B-spline curve with knots $(0, 0, 1, 1)$ and controls $(0, 1)$ is $C (x) = x$ on $[0, 1]$ . Insert the new knot $u = 1 / 2$ . The new knots are $(0, 0, 1 / 2, 1, 1)$ and the updated controls are $(0, 1 / 2, 1)$ .

In the control diagram, arrows show the copied endpoints and the single midpoint blend. The diagram records the update formulas; the verification below establishes the represented curves agree.

Facts & Assumptions

Given: Degree $p = 1$ , knot vector $(0, 0, 1, 1)$ , controls $(0, 1)$ , and the inserted knot $u = 1 / 2$ .

[F1]

Single new-knot insertion for a B-spline curve uses $Q_{i} = α_{i} P_{i} + (1 - α_{i}) P_{i - 1}$ on the active blend range, with $α_{i} = (u - t_{i}) / (t_{i + p} - t_{i})$ .

[F2]

Single new-knot insertion preserves the B-spline curve proves that the old and refined coefficient expansions define the same function.

[F3]

B-spline spaces and knot conventions defines the degree-one basis by the Cox–de Boor recurrence and half-open knot cells.

[A1]

The original active span is $[0, 1)$ and $P_{0} = 0$ , $P_{1} = 1$ .

Verification

1.1A1F1algebra

For the insertion span $k = 1$ , the only blended index is $i = 1$ and $α_{1} = (1 / 2 - t_{1}) / (t_{2} - t_{1}) = 1 / 2$ . Therefore [F1] returns $Q_{0} = P_{0} = 0$ , $Q_{1} = (P_{0} + P_{1}) / 2 = 1 / 2$ , and $Q_{2} = P_{1} = 1$ .

1.2A1F3algebra

Before insertion, the two degree-one basis functions on $[0, 1)$ are $1 - x$ and $x$ , so the curve is $x$ .

2.1A1F2F3step 1.1step 1.2algebra∎

On $[0, 1 / 2)$ , the refined curve is $0 (1 - 2 x) + (1 / 2) (2 x) = x$ . On $[1 / 2, 1)$ , it is $(1 / 2) 2 (1 - x) + 1 (2 x - 1) = x$ . The endpoint value at $1$ is the left limit. Therefore the piecewise calculation agrees with the general preservation statement [F2].

Spline evaluation and interpolation algorithms — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

de Boor evaluation with a double knot

Example

Facts & Assumptions

Verification

The natural interpolant of x squared has a second-order endpoint error

Example

Facts & Assumptions

Verification

Inserting a knot leaves a linear B-spline curve fixed

Example

Facts & Assumptions

Verification

Sources