One disjoining step kills the top multiplicity

After the blow-up π_0 : X_1 → X_0 of Z_0 with exceptional divisor F^1, the birational transforms (π_0)^{-1}_* E_1, …, (π_0)^{-1}_* E_k "do not have any k-fold intersections" [Kol07, 72]. At multiplicity m + 1: if m + 1 strict transforms met at a point x' of B_Z X, their originals would meet at x = π(x'), so x ∈ Z and x' lies on the exceptional divisor F = π^{-1}(Z), whose stalk at x' is generated by a nonzerodivisor e (the exceptional ideal is invertible). Kollár's coordinates z at x for the snc family make the members through x the hyperplanes z_{c(i)} = 0 and the center (z_{c(i)} : i through x); the chart computation of the blow-up writes π^* z_{c(i)} = u_i e with the strict transform of the member i having stalk (u_i) at x' (compare [Hau14, Proposition 5.4 (7)]). All m + 1 members through x have their transforms through x' (there are exactly m + 1 of them, since there are no (m+2)-fold intersections), so every u_i lies in 𝔪_{x'}; but F_{x'} = π^* Z_x = (u_i e : i) ⊆ 𝔪_{x'} · (e), and e ∈ 𝔪_{x'} (e) forces (1 − y) e = 0 with y ∈ 𝔪_{x'}, impossible for a nonzerodivisor e. Hence no (m+1)-fold intersection survives.

theorem Hironaka.Sequence.meetLocus_strictTransform_disjoinCenter {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} (hF : F.IsSnc) {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (hG : ∀ (i : ι), G i ∈ Set.range F.component) (m : ℕ) (hm : meetLocus G (m + 2) = ⊥) : meetLocus (fun (i : ι) => (G i).strictTransform (disjoinCenter G (m + 1))) (m + 1) = ⊥

"The (π_0)^{-1}_* E_i do not have any k-fold intersections" [Kol07, 72]: after blowing up the (m+1)-fold meet locus, the strict transforms of the members have no (m+1)-fold intersections.