No post-Lie algebra structures on pairs of perfect and nilpotent Lie algebras

Let $\mathfrak{g}$ and $\mathfrak{n}$ be finite-dimensional Lie algebras on the same vector space over a field of characteristic zero, with $\mathfrak{n}$ nilpotent. We prove that if the pair $(\mathfrak{g},\mathfrak{n})$ carries a post-Lie algebra structure all of whose right multiplications have trace zero, then $\mathfrak{g}$ is solvable. Hence no nonzero perfect Lie algebra $\mathfrak{g}$ admits a post-Lie algebra structure on $(\mathfrak{g},\mathfrak{n})$ with $\mathfrak{n}$ nilpotent. This answers a question of Burde and Dekimpe in the negative and proves the nilpotent case of a conjecture of Burde, Dekimpe and Monadjem. Nonexistence was known for abelian $\mathfrak{n}$, by a theorem of Helmstetter on left-symmetric algebras; for two-step nilpotent $\mathfrak{n}$, by Burde and Dekimpe; and for the complex perfect non-semisimple $\mathfrak{g}$ of dimensions five and six, by Burde and Dekimpe and by Burde, Dekimpe and Monadjem. The proof extends Helmstetter's argument. A post-Lie algebra structure embeds $\mathfrak{g}$ into the holomorph of $\mathfrak{n}$. Conjugations chosen by Whitehead's first lemma along the lower central series of $\mathfrak{n}$ make the translation part of this embedding vanish on a Levi factor of $\mathfrak{g}$, while its determinant stays equal to one, as in Kriebel's treatment of semisimple $\mathfrak{n}$. The proof is formalized in Lean with Mathlib, assuming Levi's theorem and Whitehead's first lemma as stated in Weibel's textbook. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Written proof, with Lean and computer checks; not yet reviewed by experts. Produced by AI models under the author's direction.