TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

PCHIP is C1, monotone on each data segment, and has no interval overshoot

Statement

For every input to PCHIP slope selection, the resulting interpolant is $C^{1}$ and interpolates all input values. On each cell with nonzero secant $d_{i}$ , the interpolant is monotone from $y_{i}$ to $y_{i + 1}$ and stays between those endpoint values; on a cell with $d_{i} = 0$ it is constant. In particular, if the input values are nondecreasing (respectively nonincreasing), the complete interpolant is nondecreasing (respectively nonincreasing). No $C^{2}$ matching is asserted.

Facts & Assumptions

Given: Strictly increasing real nodes with arbitrary real data and the PCHIP slopes and pieces selected by PCHIP slope selection.

[F1]

PCHIP slope selection: the procedure returns the Hermite pieces determined by its input values and selected slopes.

[F2]

PCHIP slope selection has no zero denominator: all selected slopes are finite and the procedure's divisions are defined.

[F3]

Interpolation, C1 matching, and cubic reproduction for Hermite pieces: shared nodal values and slopes give interpolation and $C^{1}$ matching.

[F4]

A sufficient monotonicity square for cubic Hermite interpolation: normalized endpoint slopes in $[0, 3]^{2}$ make a nonflat Hermite segment monotone between its endpoint values; zero secant and zero endpoint slopes make it constant.

[F5]

PCHIP endpoint slopes lie in the Hermite monotonicity square: PCHIP has precisely those normalized-slope bounds on every cell, including the flat-cell case.

Proof

1.1F1F2F3given

By [F2], the algorithm defines one finite slope at each input node. Its output consists of Hermite pieces sharing the same value and selected slope at each common node, so [F3] gives interpolation and $C^{1}$ matching.

1.2F4F5given

Fix a cell with $d_{i} \neq 0$ . By [F5], both slopes normalized by $d_{i}$ lie in $[0, 3]$ ; [F4] therefore makes this piece monotone from $y_{i}$ to $y_{i + 1}$ and keeps it between those values.

2.1F4F5step 1.1step 1.2given∎

If $d_{i} = 0$ , [F5] gives zero slopes at both endpoints, and [F4] makes that Hermite piece constant at its common endpoint value. For nondecreasing input, every $d_{i} \geq 0$ , so each nonflat cell is nondecreasing by step 1.2, the flat cells are constant by the calculation above, and the pieces agree at nodes by step 1.1; concatenating the cells gives a nondecreasing function. The nonincreasing case is identical with all inequalities reversed.

Depends on

Used by

Dependency tree · two levels

8 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

F. N. Fritsch and J. Butland, A Method for Constructing Local Monotone Piecewise Cubic Interpolants, SIAM Journal on Scientific and Statistical Computing 5 (1984), pp. 300–304 (standard reference, not scraped)
SciPy v1.18.0, PchipInterpolator documentation, Notes (standard reference, not scraped)