Triangle decompositions III: Physical typed absorption and prescribed statistics

We study partitions of graph edges into triangles with prescribed combinations of vertex labels. We establish, with complete proofs verified in Lean, a sufficient criterion based on four conditions: an exact positive fractional covering, membership in the integer lattice of existing triangles, many typed common neighbours, and enough local exchanges called hinges. The construction prepares decomposable reserves before the uncovered edges are known. Every reserve, certificate and exchange lies inside the graph. The criterion is a variant of the partitioned framework announced by Delcourt and Postle, with stronger fractional and lattice hypotheses and an explicitly stated rooted hinge normalization. A strengthened theorem controls linear triangle statistics and Pasch configurations in the same decomposition, with targets determined by the original fractional covering. Applications give Latin squares whose profiles determine their intercalate targets, and statistical refinements of known decompositions of the complete five-partite graph Ks,s,s,s,s for 3 s. For linear triangle statistics alone, Section 7 gives a computable tower bound depending on the parameters of T+. The complete general proofs are in the accompanying Lean formalization, whose source snapshot passed reconstruction and the endpoint axiom audits. The paper explains the construction and proves the applications. First public preprint edition. This deposit contains the approved mathematical article and formal proof supplement in English and Spanish. The complete general proofs are in the Lean source archive and audit evidence at the linked immutable GitHub snapshot. The formal record covers 1,141 project modules and six endpoint axiom groups, using only propext, Classical.choice and Quot.sound. Reconstruction uses validated compiled objects.