Exact 3D lower-hull insertion covers the hull and terminates

There are finitely many insertion prefixes, finitely many four-site subsets at each prefix, and finitely many sites to test against each subset. Projected base ranks are decided by [F5]; each weighted determinant coefficient is a finite dyadic sum of products and its sign is computed exactly by [F6]. Hence every enumeration terminates.

If a previously supporting tetrahedron remains supporting after insertion, its old four vertices still define the same plane and all old sites remain above it; it is retained exactly when the new site is also above it. Any newly supporting four-site subset not present in the preceding prefix contains the inserted site. Thus the set difference described in [F2] is precisely the new finite lower-facet list, and there is no unprocessed repair loop.

At the final prefix, every retained tetrahedron has an affinely independent projected base and satisfies all formal supporting inequalities by the exhaustive test [F2]. Conversely, every full-dimensional lower simplex in [F7] is one of the enumerated four-site subsets and passes every test, so it is retained. The two lists are therefore identical; [F7] gives coverage, common-face intersections, and weak empty-power-sphere correctness. In zero-weight mode the power distance is ordinary squared distance, so these are Delaunay tetrahedra.

A site that is a vertex of a lower face lies on the lower boundary over its projected point. By [F7], that point lies in a full lower tetrahedron; if the site were not one of its four vertices, its lift would lie on the tetrahedron's support plane, giving a zero formal determinant on an independent projected base, contrary to [F4]. Hence every lower-hull vertex appears in a retained tetrahedron. Conversely every retained tetrahedron is a lower face by step 3.1, so each of its four sites is a lower-hull vertex. Thus absence from all retained tetrahedra is equivalent to being formal-hidden by [F1]. Every degenerate projected four-tuple is separately recorded by [F2], while affine dimension below three takes the explicit status branch in [F1].

The finite enumerations and finite prefix list in step 1.1 terminate in every case and use no arbitrary choice; ties use the fixed formal order [F4]. This proves the theorem.