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.

Single new-knot insertion preserves the B-spline curve

Statement

Let $t_{0} \leq \dots \leq t_{n + p}$ be a clamped knot vector of degree $p$ as in B-spline spaces and knot conventions, with $a = t_{0}$ and $b = t_{n + p}$ , and let $ξ (v)_{j} = v_{j - 1}$ be the one-based version of any zero-based knot vector $v$ . Write $B_{i, q, v} = B_{i + 1, q, ξ (v)}$ for the basis in B-spline spaces and knot conventions. Let a B-spline curve be $C (x) = \sum_{i = 0}^{n - 1} P_{i} B_{i, p, t} (x)$ with $d \in N$ and $P_{i} \in R^{d}$ . Insert one new knot $u$ strictly inside a nonempty span by Single new-knot insertion for a B-spline curve, obtaining knots $t^{'}$ and controls $Q_{i}$ . Write $B_{i, q}^{'} = B_{i, q, t^{'}}$ . Then, for every $x \in [a, b]$ , $C (x) = \sum_{i = 0}^{n} Q_{i} B_{i, p, t^{'}} (x) .$

Facts & Assumptions

Given: A clamped degree- $p$ knot vector, controls $P_{i}$ , and a new knot $u$ strictly inside a nonempty span $[t_{k}, t_{k + 1}]$ .

[F1]

B-spline spaces and knot conventions defines degree-zero B-splines as half-open interval indicators and defines higher degrees by the Cox–de Boor recurrence with zero-denominator terms set to zero.

[F2]

Single new-knot insertion for a B-spline curve uses $Q_{i} = P_{i}$ for $i \leq k - p$ , $Q_{i} = λ_{i} P_{i} + (1 - λ_{i}) P_{i - 1}$ for $k - p + 1 \leq i \leq k$ , and $Q_{i} = P_{i - 1}$ for $i \geq k + 1$ , where $λ_{i} = (u - t_{i}) / (t_{i + p} - t_{i})$ in the middle range.

[F3]

A single new knot refines the B-spline basis gives $B_{i, p, t} = λ_{i}^{(p)} B_{i, p, t^{'}} + (1 - λ_{i + 1}^{(p)}) B_{i + 1, p, t^{'}}$ for every old degree- $p$ basis index.

[A1]

$u$ is strictly inside the nonempty span, so it is not already a knot and every denominator in the middle blend range is strictly positive.

Proof

1.1A1F1F2F3algebraconstruct

Since the knot vector is clamped and the insertion span is nonempty, $p \leq k \leq n - 1$ . For bookkeeping only, set $P_{- 1} = P_{n} = 0$ and write $λ_{j} = λ_{j}^{(p)}$ . The copy, blend, and shift ranges in [F2] give $Q_{j} = λ_{j} P_{j} + (1 - λ_{j}) P_{j - 1}$ for every $0 \leq j \leq n$ : in the copy range $λ_{j} = 1$ , in the blend range the algorithm's $α_{j}$ is $λ_{j}$ , and in the shift range $λ_{j} = 0$ . This also covers $p = 0$ , when the blend range is empty. Therefore the finite refined sum is $\sum_{j = 0}^{n} Q_{j} B_{j, p}^{'} = \sum_{i = 0}^{n - 1} P_{i} [λ_{i} B_{i, p}^{'} + (1 - λ_{i + 1}) B_{i + 1, p}^{'}]$ : the first control sum uses $P_{n} = 0$ , and in the second the change of index $i = j - 1$ drops the $P_{- 1} = 0$ term.

2.1A1F1F3step 1.1algebra∎

By [F3], each bracketed basis combination in step 1.1 equals $B_{i, p, t}$ . Substitution in that finite sum gives $\sum_{j = 0}^{n} Q_{j} B_{j, p, t^{'}} = \sum_{i = 0}^{n - 1} P_{i} B_{i, p, t} = C (x)$ . The recurrence and control algebra hold at interior knots under the right-cell convention, and at $b$ they hold by the prescribed left limits. Hence the refined expansion equals the original curve for every $x \in [a, b]$ .

Depends on

Used by

Dependency tree · one level

3 results within one dependency step 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 XI, pp. 135–138 (standard reference, not scraped)
Gershon Elber, Computer Aided Geometric Design, Chapter 7, Boehm's knot insertion (standard reference, not scraped)