Lie-Trotter product formula

In plain terms

Here is the problem. The exponential of a sum is not the product of the exponentials when the pieces do not commute -- and in quantum mechanics the interesting pieces never commute. The Lie-Trotter formula is the repair: alternate many tiny steps of each piece, and in the limit you recover the exponential of the sum exactly.

Physicists use this daily; it is the licence behind every quantum simulation. The corpus needed it in a form its libraries did not have: for operators on matrix space, with a quantitative error, and without special structural assumptions on the pieces.

So it was proved from scratch, at textbook generality: any complete normed algebra, explicit convergence rate, one step's defect controlled by a series-tail estimate and telescoped without growth.

In CSD

The formula is the assembly step in the complete-positivity proof of the Lindblad flow: the drift and jump parts of the generator are separately positive flows, and Trotter is what lets their alternation converge to the full flow so positivity passes to the limit.

It is staged as a Mathlib-upstream candidate -- CSD-free by construction, the kind of infrastructure the formalisation deliberately leaves better than it found.

Mathematically

NormedSpace.trotter_product: in a complete normed real algebra with unit norm one, the n-fold alternating product of exp(A/n) and exp(B/n) converges to exp(A+B), with a one-step defect of order one over n squared, telescoped to an overall rate with the explicit constant s^2 (3 + s) e^(2s) over n for s the sum of the norms. The earlier staged version required skew-adjointness; the de-skewed form replaces the two places skewness entered by norm bounds the final constant absorbs.

The name

Hale Trotter (1931-2022) was a Canadian-American mathematician at Princeton; the 1959 product formula came out of his thesis work on semigroups of operators. The finite-dimensional antecedent is Sophus Lie's, from the nineteenth-century theory of continuous groups, which is why the formula carries both names -- and Masuo Suzuki's later higher-order refinements are why simulation people say Trotter-Suzuki.