OAI/NumberTheory/DukePrimeDegree/Geometry/LeafBoxSeparation.lean

Pointwise separation of root fibers on a conull set

Coordinate disintegration gives one ambient null set outside which the intrinsic leaf agrees with the chart leaf at every remaining point. Within a fixed root box, equal leaves at points in one fiber then force equal points in the noninvariant ergodic case. This strengthens the conditional-almost-everywhere form needed in EKL (2006), Lemma 4.4(2).