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

Zeros of the normalized midpoint residual are precisely midpoint collocation solutions

Statement

For any $Y \in D_{h}$ , $G_{h} (Y) = 0$ if and only if

$Y_{i + 1} - Y_{i} = h f ⁣ (t_{i} + \frac{h}{2}, \frac{Y_{i} + Y_{i + 1}}{2}) (0 \leq i < N), B (Y_{0}, Y_{N}) = 0.$

Equivalently, the piecewise-linear interpolant has on each segment a constant slope equal to the vector field at the segment midpoint state and satisfies the endpoint residual.

Facts & Assumptions

Given: The BVP data, uniform mesh, admissible node vector, and normalized residual from Normalized implicit-midpoint collocation residual for a two-point BVP.

[F1]

Normalized implicit-midpoint collocation residual for a two-point BVP: every interior block is the increment divided by $h > 0$ minus the midpoint vector field, and the last block is $B (Y_{0}, Y_{N})$ .

[F2]

Square nonlinear two-point boundary-value problems and endpoint residuals: the endpoint equation in the BVP is $B (y (a), y (b)) = 0$ .

Proof

1.1givenF1F2algebra

If $G_{h} (Y) = 0$ , each block is zero. For $i < N$ , multiply the normalized row by the positive scalar $h$ to get the stated increment equation; the last block gives $B (Y_{0}, Y_{N}) = 0$ , the BVP endpoint equation by [F2].

1.2givenF1F2algebra

Conversely, if all displayed increment equations and the endpoint equation hold, dividing each increment equation by $h > 0$ makes every interior block zero, and the endpoint equation makes the last block zero; by [F2] it is the BVP boundary condition. Thus $G_{h} (Y) = 0$ .

2.1step 1.1step 1.2algebra∎

The piecewise-linear interpolant changes by $Y_{i + 1} - Y_{i}$ over an interval of width $h$ , so its slope is the quotient on the left of each increment equation. This proves the equivalent slope wording without adding another condition.

Depends on

Used by

A midpoint BVP residual can have two simple solution branches Example

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

T. A. Driscoll and R. J. Braun, Fundamentals of Numerical Computation, Chapter 10 (standard reference, not scraped)