The stopped clause of the rounds on the nonmonomial part

The modified second step of [Wlo09, Theorem 7.4.1] at m = 1 runs, along a shrinking chain of opens, rounds of order reduction on the nonmonomial part N(𝓘) at the bound d, d descending from max ord N(𝓘) to 2 (stepAChainState), then the monomial phase. 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. The centres of the rounds are of order ≥ d ≥ 2 for the transforms of (N(𝓘), d) (roundValue_isOfOrderGe_nonmonomial); at a predicate point off the boundary the marked transform of (𝓘, 1) has order ≤ 1 (ord_le_one_of_isSmoothTransversalIdealAt) and equals its own nonmonomial part (the stalk of the monomial part is the unit ideal off the boundary), which the transform identity hid ([Kol07, 111, Step 1]) makes the transform of (N(𝓘), d); so the centre misses the point. Stage by stage the points over such a point keep the predicate (IsSmoothTransversalIdealAt.stageMapAdd_of_forall_notMem_center) and stay off the boundary (notMem_totalTransformSeqFrom_of_forall_notMem_center), hence miss every centre.

• FiniteSuccession.StoppedClause.of_forall_notMem_center_of_isSmoothTransversalIdealAt: the generic shape: if no centre contains a predicate point off the boundary of its stage, the stopped clause holds, by a strong induction on the number of steps.
• notMem_center_of_isSmoothTransversalIdealAt_of_nonmonomial: the fact about one round: a list of order ≥ d ≥ 2 for (N(𝓘), d), d bounding ord N(𝓘), has no centre through a predicate point off the boundary (ord_le_one_of_isSmoothTransversalIdealAt, stalkIdeal_nonmonomialPart, componentFactor_stalkIdeal_top_of_notMem, hid, ordAlongIdeal_le_ord_of_mem_support).
• BState.roundValue_stoppedClause, descentStateAux_stoppedClause, stepAFamOn_stoppedClause, stepAFunctor_stoppedClauseFam: one round, the descent (stoppedClause_shrinkAppend), the value on an open (stoppedClause_pullback, stoppedClause_eraseEmpty), the functor (stepAFunctor_fam_seqOn).
• stepACFunctor_stoppedClauseFam: the stopped clause of the composite of the rounds and the monomial phase (composeInduced_stoppedClauseFam with step2bFunctor_stoppedClauseFam).

Sources: the modified second step of [Wlo09, Theorem 7.4.1]; [Kol07, Definition 66 (4′)] for the order of a centre and the transform identity of [Kol07, 111, Step 1]; the persistence lemmas of StopPersistence.lean. The statements themselves are not in the sources.

theorem AnalyticManifold.FiniteSuccession.StoppedClause.of_forall_notMem_center_of_isSmoothTransversalIdealAt {𝕜 : 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} (hge : S.IsOfOrderGe I 1 F.idealSheaf) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hc : ∀ (i : Fin S.length) (z : (S.stage i.castSucc).carrier), Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ₀ (S.totalTransformSeqFrom F i.castSucc) (S.markedTransformSeq I 1 i.castSucc) z → (∀ (j : (S.totalTransformSeqFrom F i.castSucc).ι), z ∉ (S.totalTransformSeqFrom F i.castSucc).hyp j) → z ∉ Manifold.IdealSheaf.support (S.center i)) : StoppedClause ψ₀ S I F

Centres missing every predicate point off the boundary give the stopped clause: if no centre of S contains a point of its stage at which the stop predicate holds and which lies on no member of the boundary there, the clause holds. The points over such a point keep the predicate (IsSmoothTransversalIdealAt.stageMapAdd_of_forall_notMem_center) and stay off the boundary (notMem_totalTransformSeqFrom_of_forall_notMem_center), stage by stage (a strong induction on the number of steps), hence miss the centres.

theorem Hironaka.Manifold.BMOmod.notMem_center_of_isSmoothTransversalIdealAt_of_nonmonomial {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (hid : NonmonomialTransformIdentity ψ₀) (S : Manifold.AnalyticTriple ψ₀ M) (R : AnalyticManifold.BlowUpSequence ψ₀ M) {d : ℕ} (hd : 2 ≤ d) (hmax : ∀ (x : ↑↧M.carrier), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple S).I x ≤ ↑d) (hR : R.toSuccession.IsOfOrderGe (BMO.nonmonomialTriple S).I d S.F.idealSheaf) (i : Fin R.toSuccession.length) {z : (R.toSuccession.stage i.castSucc).carrier} (hP : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ₀ (R.toSuccession.totalTransformSeqFrom S.F i.castSucc) (R.toSuccession.markedTransformSeq S.I 1 i.castSucc) z) (hz : ∀ (j : (R.toSuccession.totalTransformSeqFrom S.F i.castSucc).ι), z ∉ (R.toSuccession.totalTransformSeqFrom S.F i.castSucc).hyp j) : z ∉ Manifold.IdealSheaf.support (R.toSuccession.center i)

The fact about one round ([Kol07, Definition 66 (4′)] at d ≥ 2 against the order bound ord_le_one_of_isSmoothTransversalIdealAt): along a list of order ≥ d for (N(𝓘), d) with d bounding ord N(𝓘) and the transform identity hid, a point of a stage at which the stop predicate holds for the marked transform of (𝓘, 1) and which lies on no member of the boundary is in no centre. The centre carries ord_C N_i ≥ d ≥ 2; the nonmonomial part equals the ideal off the boundary (the stalk of the monomial part is the unit ideal there); and the order of the mark-1 transform at a predicate point is at most 1.

theorem Hironaka.Manifold.BMOmod.BState.roundValue_stoppedClause {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {W : TopologicalSpace.Opens M.carrier} {d : ℕ} (st : BState T 1 W d) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hd : 2 ≤ d) : AnalyticManifold.FiniteSuccession.StoppedClause (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (roundValue bo st hV hVW hT ⋯).toSuccession ((ChainState.inducedTriple T 1 st.toChainState).pullback ((st.L.stage (Fin.last st.L.length)).inclusion (st.liftOpen hVW)) ⋯).I ((ChainState.inducedTriple T 1 st.toChainState).pullback ((st.L.stage (Fin.last st.L.length)).inclusion (st.liftOpen hVW)) ⋯).F

The stopped clause of one round at the bound d ≥ 2 (mark 1), for the restricted induced triple: StoppedClause.of_forall_notMem_center_of_isSmoothTransversalIdealAt with the order clause roundValue_isOfOrderGe and notMem_center_of_isSmoothTransversalIdealAt_of_nonmonomial at roundValue_isOfOrderGe_nonmonomial and nonmonomialOrdLe_restrict.

theorem Hironaka.Manifold.BMOmod.descentStateAux_stoppedClause {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (t : ℕ) (ht : 2 ≤ t) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (r : ℕ) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (D : ℕ) (hD : ∀ x ∈ ↑(W 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑D) (j : ℕ) (hj : j ≤ r) (hjt : j ≤ D + 1 - t) : AnalyticManifold.FiniteSuccession.StoppedClause (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (descentStateAux T 1 hT bo ⋯ ⋯ t ⋯ ⋯ W hW r hWsub D hD j hj hjt).L.toSuccession (T.pullback (M.inclusion (W j)) ⋯).I (T.pullback (M.inclusion (W j)) ⋯).F

The stopped clause along the descent (threshold t ≥ 2): the initial state is the empty list, and each link appends a round at a bound d ≥ t ≥ 2 (stoppedClause_shrinkAppend with BState.roundValue_stoppedClause).

theorem Hironaka.Manifold.BMOmod.stepAFamOn_stoppedClause {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.FiniteSuccession.StoppedClause (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepAFamOn T 1 hT bo ⋯ ⋯ 2 ⋯ ⋯ U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The stopped clause of the value of the rounds on U (the modified second step of [Wlo09, Theorem 7.4.1], t = 2): the final state of the descent (descentStateAux_stoppedClause at the canonical chain), restricted to U (stoppedClause_pullback) and cleaned of its empty blow-ups (stoppedClause_eraseEmpty).

theorem Hironaka.Manifold.BMOmod.stepAFunctor_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepAFunctor 1 bo ⋯ ⋯ 2 ⋯ ⋯)

The stopped clause of the functor of the rounds (stepAFunctor at m = 1, t = 2; stepAFunctor_fam_seqOn).

theorem Hironaka.Manifold.BMOmod.stepACFunctor_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepACFunctor bo ⋯ ⋯)

The stopped clause of the composite of the rounds and the monomial phase (stepACFunctor): composeInduced_stoppedClauseFam from stepAFunctor_stoppedClauseFam and step2bFunctor_stoppedClauseFam, with step2bFam_isOfOrderGe.