The empty run of Step 3: below the mark, Step 3 does nothing

The last paragraph of [Kol07, 111] proves clause (3) of Theorem 107: when E = ∅ and m = max-ord I, after Step 1 the cosupport of the marked transform is empty and its monomial part is 𝒪_{X¹}, "Steps 2 and 3 do nothing". On the combinatorial side Step 3 is the sequence of phases 1, …, n, each blowing up Kollár's choice of faces while (∗_r) fails (Hironaka/Resolution/Algebraic/Monomial/Step3Phases.lean); on a state that already satisfies (∗_s) for every s, every face having sum < m, every choice is empty and the run is [] (step3_eq_of_star). Geometrically the realised sequence of the empty run is the empty blow-up sequence (realize_eq_nil), and the state of a piece family whose marked monomial ideal has max-ord < m satisfies every (∗_s): each face of the nerve lies in the face of some point, whose sum is the order of the monomial ideal there (ord_monomial_eq_total of Hironaka/Resolution/Algebraic/Monomial/Geometric/Exponent.lean), hence < m (star_toState_of_maxOrd_lt). These three lemmas are what Hironaka/Resolution/Algebraic/MarkedOrderReduction/Clause3.lean uses for the Step 3 half of clause (3). Not in the sources as statements.

theorem Hironaka.Monomial.MonomialState.phases_eq_of_star (k r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) : (∀ (s : ℕ), st.Star s) → phases k r st hs = (st, [])

The phases r, …, r + k − 1 of Step 3 on a state satisfying every (∗_s): no choice is ever made, the state is unchanged and the run is empty.

theorem Hironaka.Monomial.MonomialState.step3_eq_of_star (st : MonomialState) (h : ∀ (s : ℕ), st.Star s) : st.step3 = (st, [])

The combinatorial Step 3 on a state that already satisfies (∗_s) for every s (every face has sum < m) is the empty run: Kollár's "eventually we reach the stage where the property (∗_r) also holds" of [Kol07, 111, Step 3.r] is reached at once.

theorem Hironaka.Monomial.PieceFamily.star_toState_of_maxOrd_lt {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} (Φ : PieceFamily X) {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} [CharZero k] [AlgebraicGeometry.QuasiCompact f] (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hV : Φ.IsValid n m) (h : (E.monomial Φ.exponentAt).maxOrd < ↑m) (s : ℕ) : (Φ.toState n m hV).Star s

When the marked monomial ideal of a piece family has max-ord < m, its state satisfies (∗_s) for every s: a face of the nerve is contained in the face of any point of its stratum, whose sum is the order of the monomial ideal there (ord_monomial_eq_total), hence < m. This is the Step 3 half of "Steps 2 and 3 do nothing" in the last paragraph of [Kol07, 111].

theorem Hironaka.Monomial.PieceFamily.realize_eq_nil {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) {n m : ℕ} (Φ : PieceFamily X) (hV : Φ.IsValid n m) (h : ∀ (s : ℕ), (Φ.toState n m hV).Star s) : Φ.realize n m hV = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

The geometric Step 3 of a family whose state satisfies (∗_s) for every s is the empty sequence, the fold of the empty run (step3_eq_of_star). The structure morphism f is present because every statement about realize is made over the structure morphism of X, the realisation being a construction on triples over k; the proof does not need it, since the run is empty and the fold of the empty run is nil on any scheme.