Clause (1) of marked order reduction: the final maximal order is below the mark

Clause (1) of [Kol07, Theorem 107]: at the end of BMO_{n,m}(X, I, m, E) the marked transform (I_r, m) has max-ord I_r < m. After Steps 1 and 2 the induced marked triple has max-ord N(I) < m and cosupp(I, m) ∩ cosupp N(I) = ∅; Kollár then runs Step 3 on X ∖ cosupp N(I), where I = M(I), and at its end max-ord < m ([Kol07, 111, Steps 2–3]). Here the geometric Step 3 is run on X for (M(I), m, E) (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean), and the result is read for (I, m) through two facts not in the sources as such:

• the propagation center_step3Seq_disjoint: every centre of Step 3 avoids the preimage of cosupp N(I), since the centres lie in cosupp(M_i, m) and over cosupp N(I) the order of M_i is the order of M(I), which is ≤ ord I < m there (Hironaka/Resolution/Algebraic/Kol07/IsoLocus.lean);
• the assembly maxOrd_markedTransformSeq_step3Seq_lt: at a point of the end stage over cosupp N(I) the marked transform of (I, m) is the pull-back (the blow-ups are isomorphisms there), of order ord I < m; at a point off it, I = M(I) locally at the image, so the marked transforms of (I, m) and (M(I), m) have the same stalk (stalkIdeal_markedTransformSeq_congr), and realize_maxOrd_lt bounds the latter.

maxOrd_lt is clause (1) for BMO.functor: along the concatenation Step 1 ++ Step 2 ++ Step 3 the end data are the end data of Step 3 for the marked triple induced after Step 2 (markedEnd_concat_iff), whose separation order is 0 (sepOrder_induced_step2_eq_zero).

theorem Hironaka.BMO.maxOrd_lt_of_forall_lt {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {m : ℕ} (hm : 1 ≤ m) (h : ∀ (x : ↥X), I.ord x < ↑m) : I.maxOrd < ↑m

max-ord I < m (for 1 ≤ m) once ord_x I < m at every point: the maximal order is the supremum of the orders, and ord_x I < m means ord_x I ≤ m − 1 in ℕ∞.

theorem Hironaka.BMO.step3Seq_isOrderGeSeq_monomialPart {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) : (step3Seq T hT).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (monomialPart T.I T.E) m T.E

Step 3 is a smooth blow-up sequence of order ≥ m for (X, M(I), m, E) (conditions (2′)–(4′) of [Kol07, Definition 66] for (M(I), m); realize_isOrderGeSeq through monomial_exponentAt_step3Family), the form the propagation uses.

theorem Hironaka.BMO.center_step3Seq_disjoint {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) (h0 : sepOrder T = 0) (i : Fin (step3Seq T hT).length) : Disjoint (↑((step3Seq T hT).center i).support) (⇑((step3Seq T hT).stageMap i.castSucc) ⁻¹' ↑(nonmonomialPart T.I T.E).support)

The propagation: after Step 2 (sepOrder T = 0) every centre of Step 3 avoids the preimage of supp N(I). By induction along the run, the centres lie in cosupp(M_i, m), and over the locus where the blow-ups are isomorphisms ord M_i = ord M(I) ≤ ord I < m at points of supp N(I) (setOf_le_ord_subset_compl_support_of_sepOrder_eq_zero). Not in the sources as such.

theorem Hironaka.BMO.maxOrd_markedTransformSeq_step3Seq_lt {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) (h0 : sepOrder T = 0) : ((step3Seq T hT).markedTransformSeq T.I T.m (Fin.last (step3Seq T hT).length)).maxOrd < ↑m

For a marked triple with cosupp(I, m) ∩ supp N(I) = ∅, the marked transform of (I, m) at the end of Step 3 has max-ord < m (clause (1) of [Kol07, Theorem 107] for the Step 3 part): over supp N(I) the order is the order at the image (ord_markedTransformSeq_eq_of_disjoint with center_step3Seq_disjoint), < m there; off it I = M(I) locally and step3Seq_maxOrd_lt bounds the order.

theorem Hironaka.BMO.maxOrd_lt {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) : (((functor bo m).seq T hT).markedTransformSeq T.I T.m (Fin.last ((functor bo m).seq T hT).length)).maxOrd < ↑m

At the end of BMO_{n,m}(X, I, m, E) the marked transform of (I, m) has max-ord < m (clause (1) of [Kol07, Theorem 107]; the field BMOData.maxOrd_lt for BMO.functor): the end data of Step 1 ++ Step 2 ++ Step 3 are the end data of Step 3 for the marked triple induced after Step 2 (markedEnd_concat_iff, twice), whose separation order is 0 (sepOrder_afterStep2_eq_zero), where maxOrd_markedTransformSeq_step3Seq_lt applies.