Step 2 of marked order reduction: separating the cosupport from the nonmonomial part #

Step 2 of the proof of [Kol07, Theorem 107] ([Kol07, 111, Step 2]) makes the cosupports of (I, m) and of N(I) disjoint. With s the maximal order of N(I) along cosupp(I, m), the order is reduced step by step until s = 0, which is the disjointness. Kollár's device is the observation that ord_Z J₁ ≥ s and ord_Z J₂ ≥ m together are equivalent to ord_Z (J₁^m + J₂^s) ≥ ms: order reduction is applied to the single ideal N(I)^m + I^s, of order ≥ ms, and every smooth blow-up sequence of order ms for it is at once one of order s for N(I) and one of order m for I; after r = r(m, s) blow-ups cosupp(I_r, m) ∩ cosupp(N(I_r), s) = ∅, and the process continues with s − 1. At the end the two cosupports are disjoint; since every further centre lies in cosupp(I, m), X may be replaced by X ∖ cosupp N(I), where I = M(I).

The construction follows the pattern of Step 1 (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step1NonmonomialPart.lean), with the input bo : ∀ d, BOData n d, order reduction for ideals in dimension n at every mark.

sepOrder T: Kollár's s, the maximal order of N(I) along cosupp(I, m) = {x | m ≤ ord_x I} (maxOrdAlong), as a natural number (coe_sepOrder); sepOrder_eq_zero_iff: s = 0 iff the two cosupports are disjoint, the exit of the loop.
sepIdeal T = N(I)^m + I^s and sepTriple T = (X, N(I)^m + I^s, E), with max-ord ≤ ms (maxOrd_sepIdeal_le) and the admission boClass_sepTriple to BOClass n (m·s) for s ≥ 1.
step2Round bo T hT hs: one round, BO_{n,ms}(X, N(I)^m + I^s, E); weakTransformSeq_step2Round (the induced birational transform of N(I)^m + I^s is Π^{-1}_*(N(I), s)^m + Π^{-1}_*(I, m)^s at every stage), step2Round_isOrderGeSeq (of order ≥ m for (I, m)) and step2Round_isOrderGeSeq_nonmonomial (of order ≥ s for (N(I), s)).
step2Triple bo T hT hs: the marked triple (X_r, Π^{-1}_*(I, m), m, Π^{-1}_{tot} E) induced at the end of the round, again of BMOClass n m (bmoClass_step2Triple); sepOrder_step2Triple_lt: its s is smaller, since clause (1) of [Kol07, Theorem 103] for the round and Kollár's observation leave no point with ord N_r ≥ s and ord I_r ≥ m, while N(I_r) = N(N_r) (nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq) with N_r ⊆ N(N_r) gives ord N(I_r) ≤ ord N_r < s on cosupp(I_r, m).
step2 bo T hT: Step 2, by well-founded recursion on sepOrder T: the empty sequence once s = 0, otherwise the round followed by Step 2 of the induced marked triple (concat), carried with the proofs that it is a smooth blow-up sequence of order ≥ m for (X, I, m, E) without empty blow-ups; the unfolding equations step2_of_eq_zero, step2_of_pos and the result sepOrder_induced_step2_eq_zero, disjoint_cosupp_induced_step2: at the end, cosupp(I_r, m) ∩ cosupp N(I_r) = ∅.
The reduction to the monomial part, in the form the assembly uses: at the exit, cosupp(I, m) lies in the open U = X ∖ cosupp N(I) (setOf_le_ord_subset_compl_support_of_sepOrder_eq_zero), I = M(I) on U (stalkIdeal_eq_monomialPart_of_notMem_support, comap_ι_eq_monomialPart for an open inside U); with the remarks cosupp(M(I), m) ⊆ cosupp(I, m) and ord_x I = ord_x M(I) off cosupp N(I).

The result of Step 1, max-ord N(I) < m, is not a hypothesis here: the construction, its admission and its termination do not use it (the bound max-ord (N(I)^m + I^s) ≤ ms holds for every marked triple of the class); the assembly (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Assembly.lean) applies Step 2 after Step 1.