{"id":"palomar/PALOMAR-2026-10-29-000016","url":"https://github.com/zblore/lie-trotter-lean/tree/24e7c036dbef3b6cfd33cff4ed05be7339519fde","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000016-v1.json","repo":"https://github.com/zblore/lie-trotter-lean","tags":["math.FA","msc:46H30","msc:47D06","msc:15A16"],"score":0,"title":"lie-trotter-lean","trust":"high","domain":"math.FA","source":"palomar","authors":["Zayn Blore"],"reviews":0,"subject":"math.FA","summary":"A machine-checked proof of the Lie-Trotter product formula in an arbitrary complete normed algebra over the reals with norm-one unit, with a commutator-scaling error bound: for all A, B and n >= 1, the distance from (exp(A/n) exp(B/n))^n to exp(A + B) is at most ‖AB - BA‖ / (2n) · e^(‖A‖ + ‖B‖).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"An Elementary Introduction to Groups and Representations","identifier":"https://arxiv.org/abs/math-ph/0005032","relationship":"adapts"},{"title":"Theory of Trotter Error with Commutator Scaling","identifier":"https://doi.org/10.1103/PhysRevX.11.011020","relationship":"adapts"}]}