Alphabeta Math
ExampleConstruction: AI-generatedVerification: 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.

A diagonal stiff diffusion step with linear reaction

Statement

Take A=diag⁡(−1,−1000), g(y)=1−y, y(0)=0, and h=10−3. Compute the exact first-step state and the exponential-Euler and ETD2 first-step states, showing how the diagonal linear diffusion is exponentiated while the reaction is approximated.

Facts & Assumptions

Given: The finite-dimensional ODE, initial state, step size, and exact step maps from Exponential Euler and the two-stage ETD2 step maps.

[F1]

Exponential Euler and the two-stage ETD2 step maps: exponential Euler is ehAy+hφ1(hA)g(y), while ETD2 uses the predictor ah and the φ1−φ2,φ2 correction.

[F2]

The phi-function family by everywhere-convergent series: φk(X)=∑j≥0Xj/(j+k)!, so the matrix functions used at finite arguments are defined by convergent series.

[F3]

The exponential function is smooth and (exp⁡)′=exp⁡: the real exponential is differentiable with (et)′=et.

[F5]
[F8]

Rectangular matrix multiplication and the identity matrix In, including zero-sized shapes: powers of a diagonal matrix are diagonal with the corresponding scalar powers on the diagonal.

[A1]

The displayed g is componentwise, gi(y)=1−yi.

Verification

1.1givenA1F3F4F5F6F7algebra

For coordinate i with λi∈{1,1000}, put a=λi+1>0. The exact equation is yi′=−ayi+1, yi(0)=0. The product rule [F6] and chain rule [F7] show (eatyi(t))′=eat. Integrating by [F4] gives eahyi(h)=∫0heas ds=(eah−1)/a, since [F3], [F7] give antiderivative eas/a. Dividing by the positive exponential using [F5] yields yi(h)=(1−e−ah)/a.

2.1F1F2F8step 1.1algebra

By [F8], powers of A=diag⁡(−λi) are diagonal with entries (−λi)j, so the series [F2] evaluates the matrix phi functions coordinatewise. The exact exponential-Euler map has e−λihyi(0)=0 and reaction value gi(0)=1, so its coordinate is hφ1(−λih). The ETD2 predictor has that same coordinate; hence gi(a)=1−hφ1(−λih) and the ETD2 coordinate is h[(φ1(−λih)−φ2(−λih))+φ2(−λih)(1−hφ1(−λih))]=h(φ1(−λih)−hφ1(−λih)φ2(−λih)).

3.1F1F2F8step 1.1step 2.1algebra∎

In particular the stiff coordinate uses λ2h=1: its exact, exponential-Euler, and ETD2 values are respectively (1−e−1.001)/1001, 10−3φ1(−1), and 10−3(φ1(−1)−10−3φ1(−1)φ2(−1)). All exponential and phi actions are at explicit matrix/scalar arguments; any numerical implementation must return the certificates specified by Certified-action implementation of exponential Euler and ETD2.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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