Triangle decompositions II: Robust absorption for typed triangles

We study triangle decompositions in which every triangle must use a prescribed multiset of part labels. The necessary divisibility conditions record both the global numbers of edge types and the degree profile at each vertex. We prove a typical-host decomposition theorem under a finite three-step condition on the links and the forbidden-partner condition (3.2), and deduce the nearly complete four-part results used in Paper I. A separate theorem handles semidense two-part graphs with mixed triangles. The proofs combine real corrections respecting local profiles, bounded integer certificates, and a fixed absorber chosen before the remainder. Vertex splitting and corrections of parity, balance, charge and torsion extend the construction beyond three-step links; a fixed cyclic catalogue handles the conserved families. Together with an exact finite classification, these constructions establish the typical-host property for all 765 admissible four-label families up to permutation. We give the construction arguments and their quantitative assembly, and separate the finite certificate data from the universal arguments that use them. 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.