Kollár's Step 3 on the monomial state, and its termination

The phases 3.1, …, 3.n of [Kol07, 111, Step 3] on the combinatorial state of Hironaka/Resolution/Algebraic/Monomial/State.lean. phase r st hs runs phase r (Kollár's Step 3.r): while Kollár's choice at phase r is nonempty, blow up its centre. The recursion is well founded on measure r, which decreases at every blow-up (measure_blowUp_lt of Hironaka/Resolution/Algebraic/Monomial/Measure.lean), and the hypothesis hs, (∗_s) for s < r, is carried along by star_blowUp. step3 st runs the phases 1, …, n in order (structural recursion on the number of phases; (∗_1), …, (∗_r) hold when phase r + 1 starts). The result is the final state and the list of centres, in order.

Postconditions, Kollár's "eventually we reach the stage where the property (∗_r) also holds" and the end of Step 3.n: step3_star gives (∗_s) for every s, hence every face of the final nerve has sum < m (step3_maxOrd_lt, the combinatorial form of max-ord (M(I), m) < m). The run is recorded by IsRun: each centre of the list is Kollár's nonempty choice at some phase r ∈ [1, n] of the state reached before it, and the final state is the fold of the centres (step3_isRun, IsRun.fold).

phaseFuel/step3Fuel are executable copies with a fuel parameter (structural recursion) that agree with phase/step3 whenever the fuel suffices (phase_eq_of_phaseFuel, step3_eq_of_step3Fuel); the example computations of HironakaExamples/Monomial/Example112.lean and HironakaExamples/MonomialState.lean run them by decide, since a definition by well-founded recursion does not reduce in the kernel.

Kollár's text is the source of the phases and of the measure; the run as a list of centres, the predicate IsRun and the fuelled copies are bookkeeping not in the sources. The geometric realisation of a run, blow-up by blow-up, is Hironaka.Monomial.PieceFamily.realize (Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean); functoriality of step3 under restriction and refinement of the state is Hironaka/Resolution/Algebraic/Monomial/Restrict.lean and its submodules.

One phase

@[irreducible]

def Hironaka.Monomial.MonomialState.phase (r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) : MonomialState × List (Finset (Finset ℕ))

Phase r of Step 3 ([Kol07, 111, Step 3.r]): while Kollár's choice at phase r is nonempty, blow up its centre; well-founded recursion on measure r, with (∗_s) for s < r preserved along the run (star_blowUp). Returns the final state of the phase and its list of centres.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Monomial.MonomialState.phase_of_nonempty {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) (h : (st.choice r).Nonempty) : phase r st hs = ((phase r (st.blowUp (st.choice r)) ⋯).1, st.choice r :: (phase r (st.blowUp (st.choice r)) ⋯).2)

theorem Hironaka.Monomial.MonomialState.phase_of_not_nonempty {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) (h : ¬(st.choice r).Nonempty) : phase r st hs = (st, [])

inductive Hironaka.Monomial.MonomialState.IsRun : MonomialState → List (Finset (Finset ℕ)) → MonomialState → Prop

A run of Step 3: each centre is Kollár's nonempty choice at some phase r, 1 ≤ r ≤ n, of the state reached before it.

• nil (st : MonomialState) : st.IsRun [] st
• cons {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (r : ℕ) (hr : 1 ≤ r) (hrn : r ≤ st.n) (h : (st.choice r).Nonempty) (hL : (st.blowUp (st.choice r)).IsRun L st') : st.IsRun (st.choice r :: L) st'

theorem Hironaka.Monomial.MonomialState.IsRun.exists_get_eq_choice {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') (i : Fin L.length) : ∃ (r : ℕ), 1 ≤ r ∧ r ≤ (List.foldl blowUp st (List.take (↑i) L)).n ∧ ((List.foldl blowUp st (List.take (↑i) L)).choice r).Nonempty ∧ L.get i = (List.foldl blowUp st (List.take (↑i) L)).choice r

Every centre of a run is Kollár's choice at some size r on the state reached so far (the fold of the preceding centres), nonempty and within the dimension bound.

theorem Hironaka.Monomial.MonomialState.IsRun.append {st st₁ st₂ : MonomialState} {L₁ L₂ : List (Finset (Finset ℕ))} (h₁ : st.IsRun L₁ st₁) (h₂ : st₁.IsRun L₂ st₂) : st.IsRun (L₁ ++ L₂) st₂

theorem Hironaka.Monomial.MonomialState.IsRun.fold {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') : st' = List.foldl blowUp st L

The final state of a run is the fold of its centres.

theorem Hironaka.Monomial.MonomialState.IsRun.n_eq {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') : st'.n = st.n

theorem Hironaka.Monomial.MonomialState.IsRun.m_eq {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') : st'.m = st.m

theorem Hironaka.Monomial.MonomialState.phase_isRun {r : ℕ} (hr : 1 ≤ r) (st : MonomialState) (hs : ∀ s < r, st.Star s) (hrn : r ≤ st.n) : st.IsRun (phase r st hs).2 (phase r st hs).1

The run of one phase, when the phase is within the dimension bound.

theorem Hironaka.Monomial.MonomialState.phase_star {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) : (phase r st hs).1.Star r

At the end of phase r, (∗_r) holds: Kollár's "eventually we reach the stage where the property (∗_r) also holds" of [Kol07, 111, Step 3.r].

theorem Hironaka.Monomial.MonomialState.phase_star_of_lt {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) {s : ℕ} (hsr : s < r) : (phase r st hs).1.Star s

(∗_s), s < r, still holds at the end of phase r (star_blowUp along the run).

theorem Hironaka.Monomial.MonomialState.phase_n {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) : (phase r st hs).1.n = st.n

theorem Hironaka.Monomial.MonomialState.phase_m {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) : (phase r st hs).1.m = st.m

The phases r, r + 1, … and Step 3

theorem Hironaka.Monomial.MonomialState.phase_star_succ {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) (s : ℕ) : s < r + 1 → (phase r st hs).1.Star s

(∗_s) for s < r + 1 from (∗_s) for s < r at the end of phase r.

def Hironaka.Monomial.MonomialState.phases (k r : ℕ) (st : MonomialState) : (∀ s < r, st.Star s) → MonomialState × List (Finset (Finset ℕ))

k consecutive phases starting at phase r.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Monomial.MonomialState.phases 0 x✝² x✝¹ x✝ = (x✝¹, [])

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

theorem Hironaka.Monomial.MonomialState.phases_succ (k r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) : phases (k + 1) r st hs = ((phases k (r + 1) (phase r st hs).1 ⋯).1, (phase r st hs).2 ++ (phases k (r + 1) (phase r st hs).1 ⋯).2)

theorem Hironaka.Monomial.MonomialState.phases_n (k r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) : (phases k r st hs).1.n = st.n

theorem Hironaka.Monomial.MonomialState.phases_m (k r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) : (phases k r st hs).1.m = st.m

theorem Hironaka.Monomial.MonomialState.phases_star (k r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) (s : ℕ) : s < r + k → (phases k r st hs).1.Star s

After the phases r, …, r + k - 1, (∗_s) holds for every s < r + k.

theorem Hironaka.Monomial.MonomialState.phases_isRun (k r : ℕ) (hr : 1 ≤ r) (st : MonomialState) (hs : ∀ s < r, st.Star s) (hk : r + k ≤ st.n + 1) : st.IsRun (phases k r st hs).2 (phases k r st hs).1

theorem Hironaka.Monomial.MonomialState.star_of_lt_one (st : MonomialState) (s : ℕ) : s < 1 → st.Star s

(∗_0) holds since faces are nonempty (star_zero).

def Hironaka.Monomial.MonomialState.step3 (st : MonomialState) : MonomialState × List (Finset (Finset ℕ))

Step 3 of [Kol07, 111]: the phases 1, …, n in order, each by well-founded recursion on (m_r, n_r); the final state and the list of centres.

Equations

• st.step3 = Hironaka.Monomial.MonomialState.phases st.n 1 st ⋯

theorem Hironaka.Monomial.MonomialState.step3_n (st : MonomialState) : st.step3.1.n = st.n

theorem Hironaka.Monomial.MonomialState.step3_m (st : MonomialState) : st.step3.1.m = st.m

theorem Hironaka.Monomial.MonomialState.step3_star (st : MonomialState) (s : ℕ) : st.step3.1.Star s

At the end of Step 3, (∗_s) holds for every s.

theorem Hironaka.Monomial.MonomialState.step3_maxOrd_lt (st : MonomialState) {T : Finset ℕ} (hT : T ∈ st.step3.1.nerve) : st.step3.1.total T < st.m

The postcondition of [Kol07, 111, Step 3] ("at the end of Step 3.n we are done"): every face of the final nerve has sum < m. On the geometric side this is max-ord (M(I), m) < m.

theorem Hironaka.Monomial.MonomialState.step3_isRun (st : MonomialState) : st.IsRun st.step3.2 st.step3.1

The list of centres of Step 3 is a run: each centre is Kollár's nonempty choice at a phase r ∈ [1, n] of the state before it, and the final state is their fold.

Executable copies with fuel

def Hironaka.Monomial.MonomialState.phaseFuel : ℕ → ℕ → MonomialState → Option (MonomialState × List (Finset (Finset ℕ)))

phase with fuel: none when the fuel runs out.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Monomial.MonomialState.phaseFuel 0 x✝¹ x✝ = none

theorem Hironaka.Monomial.MonomialState.phase_eq_of_phaseFuel {r fuel : ℕ} {st : MonomialState} (hs : ∀ s < r, st.Star s) {res : MonomialState × List (Finset (Finset ℕ))} (h : phaseFuel fuel r st = some res) : phase r st hs = res

def Hironaka.Monomial.MonomialState.phasesFuel (fuel : ℕ) : ℕ → ℕ → MonomialState → Option (MonomialState × List (Finset (Finset ℕ)))

phases with fuel per phase.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Monomial.MonomialState.phasesFuel fuel 0 x✝¹ x✝ = some (x✝, [])

theorem Hironaka.Monomial.MonomialState.phases_eq_of_phasesFuel {fuel k r : ℕ} {st : MonomialState} (hs : ∀ s < r, st.Star s) {res : MonomialState × List (Finset (Finset ℕ))} (h : phasesFuel fuel k r st = some res) : phases k r st hs = res

def Hironaka.Monomial.MonomialState.step3Fuel (fuel : ℕ) (st : MonomialState) : Option (MonomialState × List (Finset (Finset ℕ)))

step3 with fuel per phase.

Equations

• Hironaka.Monomial.MonomialState.step3Fuel fuel st = Hironaka.Monomial.MonomialState.phasesFuel fuel st.n 1 st

theorem Hironaka.Monomial.MonomialState.step3_eq_of_step3Fuel {fuel : ℕ} {st : MonomialState} {res : MonomialState × List (Finset (Finset ℕ))} (h : step3Fuel fuel st = some res) : st.step3 = res

theorem Hironaka.Monomial.MonomialState.step3_map_eq_of_step3Fuel {fuel : ℕ} {st : MonomialState} {α : Type u_1} (f : MonomialState × List (Finset (Finset ℕ)) → α) {x : α} (h : Option.map f (step3Fuel fuel st) = some x) : f st.step3 = x

Any function f of the run read off the fuelled copy (for decide: the final state has function fields, so it is compared through f).