Fix a feasible measurement tuple. Choosing one local assignment from each fiber gives each compatible full assignment exactly once. The separation condition lets each group weight use the fixed outside representatives without changing its value. Expanding the product of the group sums by distributivity therefore gives precisely the sum of products for these full assignments. Different measurement tuples cannot share a full assignment, because its measurements are uniquely determined. Summing the tuple contributions covers all assignments once, so the algorithm returns H(t). This proves the separation step under its stated condition; it does not construct suitable measurements, recover H(0), or establish the paper's full running-time claim.