Route B: vector-fiber elimination of the barycentric witness

The scalar-fiber argument of Step 4 is insufficient after existentially quantifying over barycentric witnesses. The correct fiber is the complete p-vector attached to one retained movable vertex.

Fix all other vertex values. If the selected vertex has positive barycentric weight and the affine face value lies on the diagonal line, then its vector is contained in the affine set generated by

• the remaining p - 2 retained face vertices, and
• the diagonal direction 1.

This affine set has dimension at most (p - 2) + 1 = p - 1 in Real^p, and therefore has zero p-dimensional Lebesgue measure. Fubini then gives nullity of the complete bad parameter set.

The Fubini lemma below supplies the measure-theoretic step. The concrete vector-block geometry and coordinate transport are provided by the downstream construction.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.volume_prod_eq_zero_of_fiberwise_eq_zero {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] (s : Set (X × Y)) (hs : MeasurableSet s) (hfiber : ∀ (x : X), ν {y : Y | (x, y) ∈ s} = 0) : (μ.prod ν) s = 0

A product set whose every vector fiber is null is null. This is the exact Fubini step needed by the vector-block argument.