The Laplace transform, its operational rules, and inversion were not formalized in Lean 4. Classical inversion relies on contour integration and residues, which are not sufficiently developed in the Lean library.

An abstract kernel is defined over a complete normed algebra using Mathlib's Bochner-integral framework, then specialized to complex-valued functions on the positive half-line. Basic rules (linearity, differentiation, transforms of standard functions) are proved via truncated transforms and dominated convergence. The Bromwich inversion is proved without contour integration by writing s=γ+ir, reducing to real parameter integrals, Fubini, and the Dirichlet integral.

The forward transform, operational rules, and a Bromwich-type inversion theorem are formalized in about 2,900 lines of Lean across four files. As an application, the harmonic oscillator's Laplace-domain solution is formalized and identified with the transform of sin(ωt).