The measure decreases under Kollár's choice

The termination argument of [Kol07, 111, Step 3.2 and 3.r] on the combinatorial state of Hironaka/Resolution/Algebraic/Monomial/State.lean. Throughout, r ≥ 1, (∗_s) holds for every s < r, S = choice st r is Kollár's centre at phase r (faces of size r, common sum m_r ≥ m, common label tuple), and primes denote the state after blowUp st S.

• total_newFace_lt: a new face T₁ ∪ {c_P}, P ∈ S, and any c ∈ P \ T₁ give the old face T₁ ∪ {c} of the same size with a'(T₁ ∪ {c_P}) + m = a(T₁ ∪ {c}) + a(P \ {c}) and a(P \ {c}) < m by (∗_{r-1}) (for r = 1 the empty sum), hence a'(T₁ ∪ {c_P}) < a(T₁ ∪ {c}). This is Kollár's inequality a_{i₁} + ⋯ + a_{i_{r-1}} + a_{j_ℓ} < a_{j₁} + ⋯ + a_{j_r}, stated for faces of every size, not only of size r, and with the comparison face T₁ ∪ {c} named.
• measure_blowUp_lt: (m'_r, n'_r) < (m_r, n_r) in ℕ ×ₗ ℕ, the r-faces of the new state being the old r-faces outside S (same sums) and new faces of sums < m_r; so m_r does not increase, and if it is unchanged the number of maximizers drops by |S| ≥ 1.
• star_blowUp: (∗_s) is preserved for s < r. Kollár uses this throughout Step 3.r without stating it; not in the sources as a separate statement.
• measure_blowUp_le: no pair (m_s, n_s) increases. Not in the sources; it is the strengthening that makes the measure vectors of the example runs monotone (HironakaExamples/Monomial/Example112.lean).

measure_blowUp_lt is the decreasing measure of the well-founded recursion defining a phase, and star_blowUp carries the hypothesis of the phase along it (Hironaka/Resolution/Algebraic/Monomial/Step3Phases.lean).

theorem Hironaka.Monomial.MonomialState.total_newFace_lt (st : MonomialState) {r : ℕ} {P T₁ : Finset ℕ} {c : ℕ} (hs : ∀ s < r, st.Star s) (hP : P ∈ st.choice r) (hT₁ : T₁ ∪ P ∈ st.nerve) (hc : c ∈ P) (hcT₁ : c ∉ T₁) : insert c T₁ ∈ st.nerve ∧ (insert c T₁).card = (insert (st.newComp (st.choice r) P) T₁).card ∧ (st.blowUp (st.choice r)).total (insert (st.newComp (st.choice r) P) T₁) + st.m = st.total (insert c T₁) + st.total (P.erase c) ∧ st.total (P.erase c) < st.m ∧ (st.blowUp (st.choice r)).total (insert (st.newComp (st.choice r) P) T₁) < st.total (insert c T₁)

The inequality of [Kol07, 111, Step 3.2 and 3.r], for faces of every size: for a new face T₁ ∪ {c_P} of the blow-up along Kollár's centre at phase r and a component c ∈ P \ T₁, the old face T₁ ∪ {c} has the same size, a'(T₁ ∪ {c_P}) + m = a(T₁ ∪ {c}) + a(P \ {c}), and a(P \ {c}) < m by (∗_{r-1}); hence a'(T₁ ∪ {c_P}) < a(T₁ ∪ {c}).

theorem Hironaka.Monomial.MonomialState.total_le_maxTotal_of_mem_blowUp_faces (st : MonomialState) {r : ℕ} (hs : ∀ s < r, st.Star s) {s : ℕ} {T : Finset ℕ} (hT : T ∈ (st.blowUp (st.choice r)).faces s) : (st.blowUp (st.choice r)).total T ≤ st.maxTotal s ∧ ((st.blowUp (st.choice r)).total T = st.maxTotal s → T ∈ st.faces s ∧ st.total T = st.maxTotal s ∧ T ∉ st.choice r)

Every face of the new state of size s is an old face outside the center with its old sum, or has sum strictly below that of an old face of size s: in either case its sum is at most m_s, and a new face achieving m_s is an old s-face outside the center achieving m_s.

theorem Hironaka.Monomial.MonomialState.measure_blowUp_lt (st : MonomialState) {r : ℕ} (hs : ∀ s < r, st.Star s) (h : (st.choice r).Nonempty) : (st.blowUp (st.choice r)).measure r < st.measure r

[Kol07, 111, Step 3.2 and 3.r]: a blow-up along Kollár's centre at phase r strictly decreases (m_r, n_r) in ℕ ×ₗ ℕ.

theorem Hironaka.Monomial.MonomialState.star_blowUp (st : MonomialState) {r : ℕ} (hs : ∀ s < r, st.Star s) {s : ℕ} (hsr : s < r) : (st.blowUp (st.choice r)).Star s

A phase-r blow-up preserves (∗_s) for s < r. Kollár uses this throughout [Kol07, 111, Step 3.r] without stating its preservation; not in the sources as such.

theorem Hironaka.Monomial.MonomialState.measure_blowUp_le (st : MonomialState) {r : ℕ} (hs : ∀ s < r, st.Star s) (s : ℕ) : (st.blowUp (st.choice r)).measure s ≤ st.measure s

Under a phase-r blow-up no pair (m_s, n_s) increases. Not in the sources: a strengthening of the decrease of (m_r, n_r), by the same case analysis of the faces of the new state.