A complete Lean 4 formalization of the analytic theory of the Defant–Lee troupe transform, covering the Lagrange–Bürmann coefficient formula, a sharp phase transition between interior-critical and boundary-subcritical singularity regimes, and a transport theorem for exp–log singular expansions. The formalization comprises 1,352 lines across nine files, with zero sorries and all theorems verified axiom-clean against Mathlib v4.28.0. Key results include a proof of the Lagrange–Bürmann inversion formula via strong induction with analytic factorization, a proof of the phase dichotomy via the intermediate value theorem, and a proof of the subcritical transport theorem via L'Hôpital ratio bounds and mean-value-type estimates for power-logarithmic singular terms.

The mathematical content formalizes results from the paper "Singular transport and phase transitions for the Defant–Lee troupe transform." The troupe transform $T(z) = B(z/(1-zT(z)))$ converts Boolean cumulants into free cumulants in noncommutative probability. This formalization establishes that the dominant singularity of $T$ is governed by the auxiliary map $\psi(u) = u/(1+uB(u))$, proves that the map $u \mapsto u^2 B'(u)$ is strictly monotone (yielding uniqueness of any critical point), computes the second derivative of $\psi$ at a critical point, derives the Gamma function value $\Gamma(-5/2) = -8\sqrt{\pi}/15$ via recurrence, and proves the full quantitative transport of singular expansions through the troupe transform with explicit error bounds.