Triangle decompositions I: Formalizing the Nash–Williams theorem in Lean

Delcourt and Postle gave a proof that every sufficiently large triangle-divisible graph of minimum degree at least three quarters of its order has a triangle decomposition; their decomposition step invokes the manuscript listed as reference 17 in their paper. We give a Lean formalization that follows their extremal and non-extremal case division, together with the fractional threshold and stability results used in the proof. The decomposition inputs are supplied by typed absorption results developed in Paper II and by a protected covering construction presented here. This replaces the applications of their Theorem 13.16 without using it as an assumption. The protected construction combines simultaneous local packing, a sparse reserve, and matchings that control the resources needed by later rounds. We give its proof, including the bounded signed certificates used at the terminal step. We also state the typed inputs and check their application to the extremal residual graphs. The theorem, its attribution and its degree threshold are unchanged; the contribution is the formal proof and the explicit replacement constructions and interfaces. Preprint 1.0. This deposit contains four individual PDFs: the mathematical article and its separate formalization companion, each in English and Spanish. The selected Lean source archive, licences, scripts and audit evidence are available in the linked immutable GitHub snapshot. The companion identifies the frozen build evidence; a separate Palomar module-system port is not the evidence for this release.