LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Finite execution and storage counts for compatible neutral Euler

Statement

For Explicit Euler for a scalar neutral delay on a compatible grid, set $N = K m$ and $h = τ / m$ . With no budget let $M = N$ ; with a budget $B \in N_{0}$ let $M = \min {B, N}$ . Assuming each prescribed history, derivative-history and field evaluation returns, the procedure terminates after exactly $M$ calls to $f$ , returning completed exactly when $M = N$ and budget-exhausted otherwise. Every requested index and evaluation is admitted. If $M \geq 1$ , compatibility gives $V_{0} = ϕ^{'} (0)$ .

With the initialized history retained, the state and derivative arrays contain $2 m + 2 M + 1$ scalar values. In particular completion uses $N$ field calls and $O (N + m)$ retained scalar state and derivative values, with no memory bound constant uniformly in $N + m$ . Counts exclude the internal costs of evaluating $ϕ$ , $ϕ^{'}$ and $f$ .

Facts & Assumptions

Given: The admitted compatible scalar neutral problem and evaluation convention in the Statement.

[F1]

Explicit Euler for a scalar neutral delay on a compatible grid stores $Y_{j}, V_{j}$ for $- m \leq j < 0$ and $Y_{0}$ , then at each accepted index $n$ forms $D_{n} = ϕ^{'} (t_{n} - τ)$ for $n < m$ or $V_{n - m}$ otherwise, computes $V_{n} = a D_{n} + f (t_{n}, Y_{n}, Y_{n - m})$ , and appends $Y_{n + 1}$ .

[F2]

Compatibility is $ϕ^{'} (0) = a ϕ^{'} (- τ) + f (0, ϕ (0), ϕ (- τ))$ (Scalar neutral delay equations and the derivative-segment shift).

Proof

1.1givenF1F2algebra

At accepted index $n$ , induction gives states with indices $- m, \dots, n$ and derivative values $- m, \dots, n - 1$ . The state index $n - m$ is in range. For $n < m$ , $t_{n} - τ \in [- τ, 0)$ , so the history derivative is defined; for $n \geq m$ , $0 \leq n - m \leq n - 1$ , so the computed derivative is available. Since $n < N$ and $N h = K τ = T$ , $t_{n} < T$ , and the field accepts all scalar states at that time. Thus each accepted update is defined. At $n = 0$ , substituting the initialized states and $D_{0} = ϕ^{'} (- τ)$ into the recurrence gives $V_{0} = ϕ^{'} (0)$ by [F2]. This assertion requires an accepted first update.

2.1givenF1step 1.1algebra∎

There are finitely many loop indices $0, \dots, N - 1$ , each with one field call if accepted. The budget test rejects the first index $B$ when $B < N$ , while no index is rejected when there is no budget or $B \geq N$ . Thus exactly $M$ updates occur and the status is as asserted; all prescribed evaluations return, so the procedure terminates. Initialization stores $2 m + 1$ scalar values; each accepted update adds $V_{n}$ and $Y_{n + 1}$ , for a total $2 m + 2 M + 1$ . At completion this is $O (N + m)$ and grows with the retained array lengths, yielding the claimed memory conclusion.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Explicit Euler for a scalar neutral delay on a compatible grid.

Dependency tree · two levels

7 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

Guglielmi and Hairer, Solving Delay Differential Equations, Chapter 1 (underlying delay algorithms; finite counts proved here) (standard reference, not scraped)