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.

Real-time unitary and imaginary-time finite-matrix propagation

Statement

Let $H = diag (1, 2)$ and $y_{0} = (1, 1)^{T}$ . For imaginary time $τ \geq 0$ , solve $u^{'} = - H u$ , $u (0) = y_{0}$ , and compute its norm to exhibit the nonunitary decay. For real time $t \in R$ , set $A = - i H$ and solve $y^{'} = A y$ , $y (0) = y_{0}$ ; show that exact-action exponential Euler and ETD2 preserve the norm at grid points. For a certified implementation of the real-time methods with per-step action bounds $δ_{j}$ , give the global error bound.

Facts & Assumptions

Given: The finite matrix, initial vector, zero nonlinear term, and methods of Exponential Euler and the two-stage ETD2 step maps.

[F1]

A skew-Hermitian matrix exponential is unitary: if $A^{*} = - A$ , then $(e^{t A})^{*} e^{t A} = I$ for every real $t$ .

[F2]

Exponential Euler and the two-stage ETD2 step maps: with $g = 0$ , both exact step maps are $y \mapsto e^{h A} y$ .

[F3]

Fixed-matrix global orders and certified-action error propagation: under its tube and regularity hypotheses, certified step action errors contribute at most $K_{+} K_{-} e^{L_{p} T} \sum_{j} δ_{j}$ in addition to its local-defect term.

[F4]

The complex exponential by its power series: the scalar complex exponential is defined by its convergent power series.

[F5]

The exponential series of a bounded operator: the matrix exponential is defined by the same series, and its semigroup property holds.

[F6]

Variation of constants for a finite-matrix semilinear system: when $g = 0$ , a solution satisfies $y (t) = e^{t A} y (0)$ .

[F7]

The real exponential function and the number $e$ by a power series, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , and The exponential function is strictly increasing: $e^{0} = 1$ , $e^{x} > 0$ for real $x$ , and $x < y$ implies $e^{x} < e^{y}$ .

[F8]

$C$ is the real coordinate plane, with coordinate arithmetic, The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products, and The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product: the componentwise coordinate map identifies $C^{2}$ real-linearly with $R^{4}$ and preserves its Euclidean norm.

[F9]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: a closed bounded box in the finite-dimensional realification of $R \times C^{2}$ is compact.

[A1]

Here $A_{i m} = - H$ and $A_{r t} = - i H$ , $g = 0$ , and the exact initial state is used. The real-time uniform grid has $T > 0$ , $N \geq 1$ , and $h = T / N$ .

Verification

1.1A1F5F6F7algebra

The matrix series [F5] for $A_{i m} = - H$ is diagonal term by term and its diagonal series are the real exponential series from [F7], so $e^{τ A_{i m}} = diag (e^{- τ}, e^{- 2 τ})$ . By [F6], $u (τ) = (e^{- τ}, e^{- 2 τ})^{T}$ . For $τ > 0$ , [F7] gives $0 < e^{- τ} < 1$ and $0 < e^{- 2 τ} < 1$ , hence $∥ u (τ) ∥_{2}^{2} = (e^{- τ})^{2} + (e^{- 2 τ})^{2} < 2 = ∥ u (0) ∥_{2}^{2}$ ; this imaginary-time propagator is not unitary.

1.2A1F1F4F5F6algebra

The matrix series [F5] for $A_{r t} = - i H$ is diagonal term by term and agrees with [F4], so $e^{t A_{r t}} = diag (e^{- i t}, e^{- 2 i t})$ . Since $A_{r t}^{*} = - A_{r t}$ , [F1] gives a unitary propagator; [F6] yields $y (t) = (e^{- i t}, e^{- 2 i t})^{T}$ and $∥ y (t) ∥_{2} = \sqrt{2}$ .

2.1F2F5step 1.2algebrainduction

By [F2], both exact-action methods reduce to multiplication by $e^{h A_{r t}}$ . The semigroup identity [F5] gives $(e^{h A_{r t}})^{n} = e^{n h A_{r t}}$ , so every grid value is the exact $y (t_{n})$ from step 1.2 and has norm $\sqrt{2}$ .

3.1A1F1F3F8F9step 1.2algebra∎

By [F8], $R \times C^{2}$ is identified with $R^{5}$ using the realification and product Euclidean norm. For a finite certified real-time run, take $D = R \times C^{2}$ and $g = 0$ . Choose $R > \sqrt{2}$ larger than the absolute values of every real and imaginary coordinate of its finitely many numerical states and ETD2 predictor stages. The box $T = [0, T] \times [- R, R]^{4}$ contains those states and stages, and the exact path from step 1.2 lies in it because its norm is $\sqrt{2}$ . By [F9], $T$ is compact; since $D$ is the whole time-state space, it has positive margin. Here $M = 1$ , $ω = 0$ , $K_{+} = K_{-} = 1$ , $L_{g} = Q_{1} = Q_{2} = 0$ , and therefore $C_{p} = L_{p} = 0$ in [F3]. With exact starting data, [F3] gives $\max_{n} ∥ {\tilde{y}}_{n} - y (t_{n}) ∥_{2} \leq \sum_{j = 0}^{N - 1} δ_{j}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

103 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

Marlis Hochbruck and Alexander Ostermann, Exponential Integrators, Acta Numerica 19 (2010) (standard reference, not scraped)
ISEM Team 2011/12, Operator Semigroups for Numerical Analysis, 15th Internet Seminar on Evolution Equations (standard reference, not scraped)