This submission formalizes Theorem 1.2 of Moser and Tardos, A Constructive Proof of the General Lovász Local Lemma, and Theorem 2.2 of Haeupler, Saha, and Srinivasan, New Constructive Aspects of the Lovász Local Lemma. For finitely many measurable bad events determined by mutually independent random variables, it proves the asymmetric local-lemma conclusion and the resampling algorithm's expected per-event and total resampling bounds. It also proves that any observed event is true at some stage—and hence in the output distribution—with probability at most its original probability times the inverse local-lemma product over its dependency neighborhood. The proofs use resampling tables, proper witness trees, branching-process weight estimates, and a finite-termination argument.