The Erdős–Sauer Clique Decomposition Problem for 3-Graphs: Verification through Nine Vertices and Local Packing Reductions

We study the r=3 case of the Erdős–Sauer clique decomposition problem and prove that its conjectured bound holds for every 3-graph on at most nine vertices. If G is a 3-graph, m=|E(G)|, and ν(G) is the maximum number of pairwise edge-disjoint tetrahedra K_4^3 in G, then the minimum number of pieces in a decomposition into single triples and tetrahedra is m-3ν(G). Hence the problem is equivalent to m-3ν(G) ≤ ex_3(n,K_4^3). The finite result through n=9 is the first main contribution of the paper. The cases through n=7 follow from the near-Turán reduction together with the exact small Turán numbers, while n=8 and n=9 are proved analytically. The n=8 argument uses an S(3,4,8), and the n=9 argument uses an S(3,4,10) together with a collision estimate for missing triples under random relabelling. A recent working report independently records the packing identity and verifies the range through n=7; accordingly, the new finite advance claimed here is the analytic extension from seven to nine vertices. The second contribution is a deterministic local theory around a maximum tetrahedron packing. We prove a leaf-rigidity lemma, a pair-dominant assignment criterion, and a good-orientation criterion on an actual-bridge graph, whose edges represent tetrahedra actually witnessed in G rather than mere support overlaps. We also prove an internal four-pack cover of cost at most 11, improved to 10 under a mild intersection condition, and formulate a boundary-credit criterion that converts this internal saving into a genuine 3-peeling step when the residual boundary has small cover number. These structural results identify concrete sufficient conditions for the conjectured inequality, but they do not yet force such a condition in every maximum packing. No proof of the general r=3 conjecture is claimed.