The stopped clause of the monomial phase

The monomial phase of the modified second step of [Wlo09, Theorem 7.4.1] blows up, while a boundary member is active, the positive locus of the greatest active member: a centre inside the boundary (step2bCenter_subset_support). The stopped clause of ClauseTools.lean (the field stopped_never_blownUp of BMOmodFam) asks that a point at which the stop predicate holds and which lies on no member of the boundary is never blown up later; for a phase whose centres lie in the boundary this follows from the persistence of "off the boundary" alone (notMem_totalTransformSeqFrom_of_forall_notMem_center, StopPersistence.lean): the points over such a point stay off the boundary stage by stage, hence outside every centre.

• FiniteSuccession.StoppedClause.of_forall_center_subset_support: the generic shape: centres in the support of the current boundary family give the stopped clause, by a strong induction on the number of steps. The predicate is part of the clause because the stop rule of [Wlo09, Theorem 7.4.1] speaks of the points where the algorithm stopped (the field stopped_never_blownUp); this proof does not need it, since with the centres inside the boundary every point off the boundary, stopped or not, is never blown up.
• center_support_subset_step2bPhase: the centres of the monomial phase lie in the boundary at every stage, along the recursion of step2bPhase (step2bPhase_succ_of_nonempty): the head centre in T.F.support, the tail's centres in the boundary from the triple after the step, whose family is the total transform (stepTriple_F, cons_totalTransformSeqFromAux_succ).
• step2bFunctor_stoppedClauseFam: the stopped clause of the functor step2bFunctor: the value on an open is the complete phase of the restricted triple (step2bFam_seqOn); the normal-crossings clause from isOfOrderGe_step2bPhase.

Sources: the monomial phase of [Wlo09, Theorem 7.4.1]; [Kol07, Definition 66]; the persistence lemmas of StopPersistence.lean. The statements themselves are not in the sources.

theorem AnalyticManifold.FiniteSuccession.StoppedClause.of_forall_center_subset_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (h3 : ∀ (i : Fin S.length), (S.boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith (S.center i)) (hc : ∀ (i : Fin S.length), Manifold.IdealSheaf.support (S.center i) ⊆ (S.totalTransformSeqFrom F i.castSucc).support) : StoppedClause ψ₀ S I F

Centres inside the boundary give the stopped clause: if every centre of S lies in the support of the current boundary family, no point over a point off the boundary is ever blown up. By notMem_totalTransformSeqFrom_of_forall_notMem_center the points over x stay off the boundary, stage by stage (a strong induction on the number of steps), hence outside the centres. The predicate is part of the clause because the stop rule of [Wlo09, Theorem 7.4.1] speaks of the points where the algorithm stopped (the field stopped_never_blownUp of BMOmodFam); this proof does not need it, since with the centres inside the boundary every point off the boundary, stopped or not, is never blown up.

theorem Hironaka.Manifold.BMOmod.center_support_subset_step2bPhase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (i : Fin (step2bPhase k T hT).toSuccession.length) : Manifold.IdealSheaf.support ((step2bPhase k T hT).toSuccession.center i) ⊆ ((step2bPhase k T hT).toSuccession.totalTransformSeqFrom T.F i.castSucc).support

The centres of the monomial phase lie in the boundary (the centres are the positive loci of active members, step2bCenter_subset_support), at every stage of the phase, along the recursion of step2bPhase: the head centre in T.F.support, the tail's centres in the boundary from the triple after the step, whose family is the total transform (stepTriple_F, cons_totalTransformSeqFromAux_succ).

theorem Hironaka.Manifold.BMOmod.step2bFunctor_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} : AnalyticFamilyFunctor.StoppedClauseFam ψ₀ (step2bFunctor ψ₀)

The stopped clause of the monomial phase (the field stopped_never_blownUp of BMOmodFam for step2bFunctor): the value on every open is the complete phase of the restricted triple (step2bFam_seqOn), its centres lie in the boundary (center_support_subset_step2bPhase), so StoppedClause.of_forall_center_subset_support applies with the normal-crossings clause of isOfOrderGe_step2bPhase.