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

A finite-matrix Schrödinger split preserves norm

Example

Realify $C^{2}$ as $R^{4}$ and let $H_{K} = (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array}), V = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), A = - i H_{K}, B = - i V .$ Here $H_{K}$ is a two-level kinetic matrix and $V$ is a Hermitian potential coupling. The finite-dimensional Schrödinger equation is $ψ^{'} = (A + B) ψ = - i (H_{K} + V) ψ$ . Each exact kinetic or potential subflow preserves the Euclidean norm, so every exact Lie or Strang composition does as well. The local errors are nonzero for suitable initial data because the two generators do not commute; no spatial PDE or unbounded-operator conclusion is claimed.

Facts & Assumptions

Given: The matrices $H_{K}, V, A, B$ and a differentiable solution $ψ (t) \in C^{2}$ of the total or split Schrödinger equation.

[F1]

Lie and Strang compositions of exact split flows: Lie and Strang maps are compositions of the exact flows of the two component fields, and their bracket is $[a, b] = D b a - D a b$ .

[F2]

Lie and Strang splitting errors have commutator expansions: the leading Lie defect is $\frac{1}{2} h^{2} [a, b]$ , and the Strang defect has the stated cubic double-bracket coefficient.

[F3]

The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product and 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: the standard complex Euclidean norm satisfies $∥ ψ ∥_{2}^{2} = ψ^{*} ψ$ .

[F4]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ and In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: the adjoint matrix is the conjugate transpose, and $H^{*} = H$ for a Hermitian matrix.

[F5]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix products have their standard associative coordinate meaning.

[F6]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ and The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : the product rule applies to real and imaginary coordinates, and a real differentiable scalar function with zero derivative is constant.

[F7]

The exponential series of a bounded operator: a finite matrix exponential is defined for every real time, equals $I$ at zero, and has derivative $A e^{t A}$ .

[A1]

$H_{K}^{*} = H_{K}$ and $V^{*} = V$ , as direct conjugate-transpose calculation verifies.

Proof

1.1A1F3F4F5F6F7algebra

Let $H$ be any of $H_{K}$ , $V$ , or $H_{K} + V$ . Its exact flow exists for all real time by [F7], and every solution obeys $ψ^{'} = - i H ψ$ . By [F3]–[F6], differentiating the real function $ψ^{*} ψ$ gives $\frac{d}{d t} (ψ^{*} ψ) = (ψ^{'})^{*} ψ + ψ^{*} ψ^{'} = i ψ^{*} H^{*} ψ - i ψ^{*} H ψ = 0,$ where [A1] supplies $H^{*} = H$ . Therefore [F6] makes $∥ ψ (t) ∥_{2}^{2}$ constant on every admitted interval, and each exact subflow and the total flow preserve norm.

1.2A1F1F5algebra

Direct multiplication gives $C : = B A - A B = H_{K} V - V H_{K} = (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array}) \neq 0.$ This is the linear matrix of $[a, b]$ by [F1]. Also $C A - A C = i (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), C B - B C = 2 i (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}) .$

2.1F1step 1.1

By [F1], a Lie or Strang step is a composition of exact component flows. Each factor preserves norm by step 1.1, so the composition preserves norm by repeated application of the same equality.

3.1F2step 1.2algebra∎

For $ψ = e_{1}$ , the Lie coefficient $\frac{1}{2} C ψ$ is nonzero. The Strang coefficient $- \frac{1}{24} (C A - A C) ψ - \frac{1}{12} (C B - B C) ψ$ is also nonzero, since its first coordinate is $- i / 6$ . Applying [F2] shows the exact subflows retain norm while the Lie and Strang maps have their respective nonzero local splitting defects.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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.