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.

Clamped cubic spline interpolation exists uniquely

Statement

Let $a = x_{0} < x_{1} < \dots < x_{m} = b$ , $m \geq 1$ , let $y_{0}, \dots, y_{m} \in R$ , and let $σ_{a}, σ_{b} \in R$ . Put $h_{i} = x_{i + 1} - x_{i} > 0$ and $d_{i} = (y_{i + 1} - y_{i}) / h_{i}$ . There is exactly one clamped cubic spline interpolant in the sense of Clamped cubic spline interpolant. Its nodal second derivatives $M_{i} = s^{''} (x_{i})$ are the unique solution of $\begin{aligned} 2 h_{0} M_{0} + h_{0} M_{1} & = 6 (d_{0} - σ_{a}), \\ h_{i - 1} M_{i - 1} + 2 (h_{i - 1} + h_{i}) M_{i} + h_{i} M_{i + 1} & = 6 (d_{i} - d_{i - 1}), 1 \leq i < m, \\ h_{m - 1} M_{m - 1} + 2 h_{m - 1} M_{m} & = 6 (σ_{b} - d_{m - 1}) . \end{aligned}$ On $[x_{i}, x_{i + 1}]$ the interpolant is $s_{i} (x) = \frac{M_{i} (x_{i + 1} - x)^{3} + M_{i + 1} (x - x_{i})^{3}}{6 h_{i}} + (y_{i} - \frac{M_{i} h_{i}^{2}}{6}) \frac{x_{i + 1} - x}{h_{i}} + (y_{i + 1} - \frac{M_{i + 1} h_{i}^{2}}{6}) \frac{x - x_{i}}{h_{i}} .$

Facts & Assumptions

Given: The partition, arbitrary nodal values, and prescribed endpoint slopes in the Statement.

[F1]

Clamped cubic spline interpolant requires a $C^{2}$ function, cubic pieces, interpolation at every node, and the two prescribed endpoint slopes.

[A1]

$m \geq 1$ , $x_{0} < \dots < x_{m}$ , $y_{i} \in R$ , and $σ_{a}, σ_{b} \in R$ .

Proof

1.1A1algebrachoose

Let $A$ be the $(m + 1) \times (m + 1)$ matrix of the displayed system. Its first row has diagonal $2 h_{0}$ and off-diagonal sum $h_{0}$ ; an interior row $i$ has diagonal $2 (h_{i - 1} + h_{i})$ and off-diagonal sum $h_{i - 1} + h_{i}$ ; the last row has diagonal $2 h_{m - 1}$ and off-diagonal sum $h_{m - 1}$ . Every diagonal entry therefore strictly exceeds the sum of the other absolute entries in its row. If $A v = 0$ for a nonzero $v$ , choose $i$ with $∣ v_{i} ∣ = \max_{j} ∣ v_{j} ∣ > 0$ . The $i$ th row gives $∣ A_{i i} ∣ ∣ v_{i} ∣ \leq \sum_{j \neq i} ∣ A_{i j} ∣ ∣ v_{j} ∣ \leq (\sum_{j \neq i} ∣ A_{i j} ∣) ∣ v_{i} ∣$ , contradicting strict row diagonal dominance. Thus $A$ has zero kernel and, being square, is invertible.

2.1A1F1step 1.1constructalgebra

Let $M_{0}, \dots, M_{m}$ be the unique solution. Define $s_{i}$ by the displayed piece formula. Substitution at $x_{i}$ and $x_{i + 1}$ gives the values $y_{i}, y_{i + 1}$ , and differentiating twice gives endpoint second derivatives $M_{i}, M_{i + 1}$ . Differentiating once gives $s_{i}^{'} (x_{i}) = d_{i} - h_{i} (2 M_{i} + M_{i + 1}) / 6$ and $s_{i}^{'} (x_{i + 1}) = d_{i} + h_{i} (M_{i} + 2 M_{i + 1}) / 6$ . The interior system rows make the adjacent endpoint slopes agree. Since the adjacent second derivatives both equal the shared $M_{i}$ , the pieces join with continuous first and second derivatives. The first and last rows give $s_{0}^{'} (a) = σ_{a}$ and $s_{m - 1}^{'} (b) = σ_{b}$ . Hence the constructed function satisfies [F1].

3.1A1F1step 1.1step 2.1algebra∎

For any clamped interpolant, its nodal second derivatives must satisfy the displayed system by the same endpoint-slope formulas, so invertibility from step 1.1 forces them to equal the constructed $M_{i}$ . On each interval, the difference from $s_{i}$ is a cubic with zero endpoint values and zero endpoint second derivatives. Its second derivative is affine and vanishes at both endpoints, hence is identically zero; the difference is then affine and vanishes at both endpoint values, hence is zero. Every piece is therefore unique, proving uniqueness of the interpolant.

Depends on

Clamped cubic spline interpolant

Used by

Dependency tree · two levels

2 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 IV, pp. 42–45 (standard reference, not scraped)
Brian LeMesurier, Introduction to Numerical Methods and Analysis with Python, §3.4.2 (standard reference, not scraped)