Gallai's Path Decomposition Conjecture for Graphs with Small Bowtie Boundaries

Let F be the subgraph induced by the even-degree vertices of a connected simple graph G. Suppose F has a component consisting of two triangles sharing exactly one vertex (a whole bowtie), and let y be an even vertex outside that component. We prove that if the bowtie has at most four external neighbours, and every other even vertex except possibly y has degree at most three in F, then G admits an edge partition into at most ceil(|V(G)|/2) simple paths, with at least two paths ending at y. Edges among external neighbours are unrestricted, and deleting the bowtie need not leave a connected graph. The computer-assisted proof combines published endpoint-decomposition theorems, componentwise path budgets, and complete finite local reconstruction certificates, with symbolic substitution into arbitrary ambient graphs. We also establish a sharp two-path star expansion, a supported composition theorem, elementary reductions for further boundary types, and an odd-order two-exception result. The unrestricted even-order two-nonadjacent-exception problem remains open. This is manuscript draft v0.8; it has not been peer reviewed. The associated Lean formalization is a separate work in progress and is not claimed as Palomar-verified.