Kollár's Example 112 and the split example, computed #

Finite computations on the concrete states of HironakaExamples/Monomial/Examples.lean, decided by the kernel (decide, never native_decide):

the maximal-multiplicity procedure maxMultRun is structural recursion and reduces directly;
Kollár's Step 3 (MonomialState.step3 of Hironaka/Resolution/Algebraic/Monomial/Step3Phases.lean) is defined by well-founded recursion on the measure (m_r, n_r) and does not reduce in the kernel, so every statement about it is read through the fuelled copy step3Fuel and the agreement theorem step3_map_eq_of_step3Fuel: decide evaluates (step3Fuel 20 st).map f = some x and the theorem transports the value to f (step3 st); fuel 20 is ample, the longest run here having four centres;
the measure pairs of intermediate states are read off explicit blowUp chains (the centres are those the _centers statements establish), and Sub splitU splitX is rfl on the six shared fields plus decide on the nerve inclusion.

What the numbers show. [Kol07, Example 112]: on a smooth surface with two curves E¹, E² through a point p and a₁ = a₂ = m + 1, blowing up the point of highest multiplicity, then E² ∩ E³, and so on, produces after r - 2 steps the exponents m + p_i, p_i the i-th Fibonacci number, so the multiplicities grow without bound. On the state, blowing up a face P creates a component of exponent a(P) − m; under the maximal-multiplicity rule the chosen face is always the newest double point {i, i+1}, whose sum (m + p_i) + (m + p_{i+1}) gives the new exponent m + p_i + p_{i+1} = m + p_{i+2} (maxMult_one, maxMult_two, maxMult_three; the other tie-break in maxMult_otherTieBreak_one). Under Kollár's order, phase 1 first blows up the curves themselves (the old component dies, the new one has exponent a − m), so before any double point is touched every exponent is < m and the sum of the pair is < 2m; the bound (∗₁) caps the exceptional exponent below the old ones (total_newFace_lt of Hironaka/Resolution/Algebraic/Monomial/Measure.lean), and the run stops after at most four steps (step3_one, …, step3_ten, with the measure traces measure_trace_one, measure_trace_two). The three-phase instance shows the pairs (m_s, n_s) of the later phases never increasing while the current one drops (threePhase_measure). In the split example the fine exponents 1, 0, 1, 0 give the same two trivial blow-ups on X and on U (split_fine_centers, split_restrictRun), whereas the coarse exponents 0, 0 on X leave Step 3 idle while on U it acts twice (split_coarse_runs): the coarse procedure does not commute with the open immersion U → X, which is the reason for the fine split recorded in Hironaka/Resolution/Algebraic/Monomial/State.lean.

The theorems splitX_centers/splitU_centers of HironakaExamples/MonomialRestrict.lean are the two halves of split_fine_centers, re-proved here because the root does not import the example modules. Nothing here is used elsewhere.

Kollár's Example 112 and the split example, computed #

The maximal-multiplicity procedure #

Kollár's Step 3 on Example 112 #

The three-phase instance #

The split example #