# Global smoothness for relativistic Vlasov–Maxwell

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system](../../preprints/Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026/paper.pdf)

## Scope

The formalized result gives global existence and uniqueness for the three-dimensional one-species relativistic Vlasov–Maxwell system. The initial particle density is nonnegative, smooth, and compactly supported; the initial fields have bounded derivatives of all orders, finite energy, and satisfy both Gauss constraints. The solution is smooth on every finite time interval, has compact particle phase support there, and is unique among classical solutions. No smallness, symmetry, or neutrality assumption is imposed.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Global classical Vlasov–Maxwell solutions | [VlasovMaxwell.lean](../ComparatorChallenges/VlasovMaxwell.lean) |