OAI/NumberTheory/DukePrimeDegree/Geometry/LeafNullClosure.lean

Enlarging a null set to avoid it along every conditional root leaf

Iterating the ambient-to-leaf null-set implication gives one measurable null set whose complement is leafwise conull at every remaining point. This lets the commutator construction choose all of its vertices outside the same exceptional set.