The two stop clauses of the modified first step, assembled

The modified first step of [Wlo09, Theorem 7.4.1] is the assembly of Kollár's Step 2 at the datum stepBData: the chain of Step 2.1 from the unmodified marked order reduction one dimension down (hfStep2FamChain), the link of Step 2.2 at the greatest member H_r with the modified core (hfStep22FamOn), appended, restricted and cleaned of empty blow-ups (hfStep2SeqFamOn); the local functor hfLocalFunctorFam 1 on the local maximal-contact class; the descent stepBFunctor to the class of BO_{n,1}. This module proves the stopped clause and the output clause of ClauseTools.lean along that assembly from three pieces: the chain's stopped clause (ClauseStep21.lean), the clauses of the data of the step with respect to the boundary without the member (ClausePhaseBCore.lean), and the bridges and composition lemmas (ClauseBridge.lean, ClauseCompose.lean, ClauseTools.lean).

• membersSubset_emptyMember_idxHOf_induced: the boundary E^{exc} + H_r of the triple of [Kol07, Theorem 103, Step 2.2] without H_r is a sub-family of the full transformed boundary (its members are the exceptional divisors, at the indices exceptionalEmb): the hypothesis of StoppedClause.of_membersSubset for the link.
• exists_hyp_emptyMember_eq_of_le_ord, exists_hyp_emptyMember_eq_of_le_ord': a member of the full boundary through a point of order ≥ 1 at the end of the link is a member of the boundary of Step 2.2 without H_r. The transforms of the original members are excluded by the chain's cosupport clause: the point lies over a point of order ≥ 1 on such a transform (ord_markedTransformSeq_stageMapAdd_eq_zero, notMem_strictTransformSeq_of_stageMapAdd). This is the hypothesis of OutputClause.of_forall_mem.
• hfStep22FamOn_stoppedClause_induced, hfStep22FamOn_outputClause_induced: the link's two clauses for the restricted induced triple: the clauses of the data of the step at the re-tuned triple of Step 2.2 and its greatest member (greatestIdx_eq; the maximal contact of H_r by maximalContact_persistsFam_tuned; the tuning is the identity at the mark 1, tuned_one), the boundary changed by StoppedClause.of_membersSubset and OutputClause.of_forall_mem with the order clause at E − H_r (HFamData.IsOfOrderGeEmptyMemberFam) and at the full boundary (hfStep22FamOn_isOfOrderGe_full).
• hfStep2SeqFamOn_stoppedClause, hfStep2SeqFamOn_outputClause: the value of Step 2 on the open: the chain's stopped clause and the link's clauses composed at the last link (stoppedClause_shrinkAppend, outputClause_shrinkAppend), restricted (stoppedClause_pullback, outputClause_pullback) and cleaned (stoppedClause_eraseEmpty, outputClause_eraseEmpty), as in hfStep2SeqFamOn_isOfOrderGe.
• hfStep2FamOn_stoppedClause, hfStep2FamOn_outputClause, hfLocalFunctorFamOn_stoppedClause, hfLocalFunctorFamOn_outputClause: with the class's hypersurface of maximal contact, and at the mark 1 on the tuned triple (tuned_pullback, tuned_one at the restricted triple).
• stepBLocalFunctorFam_stoppedClauseFam, stepBLocalFunctorFam_outputClauseFam, stepBFunctor_stoppedClauseFam, stepBFunctor_outputClauseFam: the local functor of the modified first step and its descent along the maximal-contact cover (stoppedClauseFam_of_agreeFam, outputClauseFam_of_agreeFam), from the clauses hR8 and hR1 of the functor one dimension down.

Sources: the modified first step of [Wlo09, Theorem 7.4.1]; [Kol07, Theorem 103, Steps 2–3] and [Kol07, 104, Step 2.1] (the full boundary from the boundary of Step 2.2); [Kol07, Corollary 85]. The statements themselves are not in the sources.

theorem Hironaka.Manifold.BO.membersSubset_emptyMember_idxHOf_induced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (O : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) : (((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.emptyMember (idxHOf T s L hL hsnc)).MembersSubset ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F

The boundary of Step 2.2 without H_r is a sub-family of the full transformed boundary (restricted to an open): its members are the exceptional divisors E^{exc}_k, members of the full boundary at the indices exceptionalEmb k (hyp_exceptionalEmb), and the emptied slot of H_r. The hypothesis of StoppedClause.of_membersSubset for the link of Step 2.2.

theorem Hironaka.Manifold.BO.exists_hyp_emptyMember_eq_of_le_ord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (O : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) (hs : s = 1) (hdis : ∀ (j : T.F.ι), Disjoint {x : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq T.I s (Fin.last L.toSuccession.length)) x} (L.toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last L.toSuccession.length))) (S' : ((L.stage (Fin.last L.length)).restrict O).FiniteSuccession) (hge : S'.IsOfOrderGe ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).I 1 ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.idealSheaf) (x : (S'.stage (Fin.last S'.length)).carrier) (hord : 1 ≤ Manifold.IdealSheaf.ord (S'.markedTransformSeq ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).I 1 (Fin.last S'.length)) x) (k : ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.ι) (hk : x ∈ (S'.totalTransformSeqFrom ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length)).hyp (S'.originalIdx ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length) k)) : ∃ (k' : (S'.totalTransformSeqFrom (((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.emptyMember (idxHOf T s L hL hsnc)) (Fin.last S'.length)).ι), (S'.totalTransformSeqFrom (((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.emptyMember (idxHOf T s L hL hsnc)) (Fin.last S'.length)).hyp k' = (S'.totalTransformSeqFrom ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length)).hyp (S'.originalIdx ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length) k)

A member of the full transformed boundary through a point of order ≥ 1 at the last stage of the run of Step 2.2 is a member of the boundary of Step 2.2 without H_r (the hypothesis of OutputClause.of_forall_mem): by originalIdxAux_or_exceptionalEmb the member is the run's transform of a member of the full boundary below or an exceptional divisor of the run; a member below is the chain's transform of an original member, which is excluded, since the point lies over a point of order ≥ 1 (ord_markedTransformSeq_stageMapAdd_eq_zero) on that transform (notMem_strictTransformSeq_of_stageMapAdd), against the chain's cosupport clause hdis, or an exceptional divisor of the chain, a member of the boundary of Step 2.2 (hyp_originalIdx, hyp_exceptionalEmb).

theorem Hironaka.Manifold.BO.exists_hyp_emptyMember_eq_of_le_ord' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (O : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) (hs : s = 1) (hdis : ∀ (j : T.F.ι), Disjoint {x : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq T.I s (Fin.last L.toSuccession.length)) x} (L.toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last L.toSuccession.length))) (S' : ((L.stage (Fin.last L.length)).restrict O).FiniteSuccession) (hge : S'.IsOfOrderGe ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).I 1 ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.idealSheaf) (x : (S'.stage (Fin.last S'.length)).carrier) (hord : 1 ≤ Manifold.IdealSheaf.ord (S'.markedTransformSeq ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).I 1 (Fin.last S'.length)) x) (m : (S'.totalTransformSeqFrom ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length)).ι) (hm : x ∈ (S'.totalTransformSeqFrom ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length)).hyp m) : ∃ (k' : (S'.totalTransformSeqFrom (((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.emptyMember (idxHOf T s L hL hsnc)) (Fin.last S'.length)).ι), (S'.totalTransformSeqFrom (((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.emptyMember (idxHOf T s L hL hsnc)) (Fin.last S'.length)).hyp k' = (S'.totalTransformSeqFrom ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F (Fin.last S'.length)).hyp m

exists_hyp_emptyMember_eq_of_le_ord for every member index of the run's last boundary (the exceptional divisors of the run are members of both boundaries at the same index).

theorem Hironaka.Manifold.BO.hfStep22FamOn_stoppedClause_induced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (d : HFData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (hs : s = 1) (hhf8 : d.hf.StoppedClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (hfStep22FamOn T s d hT U hU hH hle).toSuccession (((T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).induced s (hfStep2FamChain T s d hT U hU).L ⋯).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).I (((T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).induced s (hfStep2FamChain T s d hT U hU).L ⋯).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).F

The stopped clause of the link of Step 2.2 for the restricted induced triple (the mark 1): the clause of the data of the step (HFamData.StoppedClauseFam) at the re-tuned triple of Step 2.2 (tuned_one: the tuning is the identity at the mark 1) at its greatest member H_r (greatestIdx_eq), whose maximal contact is maximalContact_persistsFam_tuned; with respect to the boundary without H_r, hence with respect to the full transformed boundary by StoppedClause.of_membersSubset with membersSubset_emptyMember_idxHOf_induced and the order clause at that boundary (HFamData.IsOfOrderGeEmptyMemberFam).

theorem Hironaka.Manifold.BO.hfStep22FamOn_outputClause_induced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (d : HFData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (hs : s = 1) (hhf1 : d.hf.OutputClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.OutputClause ψ₀ (hfStep22FamOn T s d hT U hU hH hle).toSuccession (((T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).induced s (hfStep2FamChain T s d hT U hU).L ⋯).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).I (((T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).induced s (hfStep2FamChain T s d hT U hU).L ⋯).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).F

The output clause of the link of Step 2.2 for the restricted induced triple: the clause of the data of the step (HFamData.OutputClauseFam) as in hfStep22FamOn_stoppedClause_induced, with respect to the full transformed boundary by OutputClause.of_forall_mem with exists_hyp_emptyMember_eq_of_le_ord' (the chain's cosupport clause step21FamAux_cosupp_disjoint, an empty member having empty strict transform) and the full-boundary order clause hfStep22FamOn_isOfOrderGe_full.

theorem Hironaka.Manifold.BO.hfStep2SeqFamOn_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (d : HFData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (hs : s = 1) (hbd : d.bd₁.StoppedClauseFam) (hhf8 : d.hf.StoppedClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (hfStep2SeqFamOn T s d hT U hU hH hle).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The stopped clause of the value of Step 2 on the open (the field stopped_never_blownUp of BMOmodFam for the local value of the modified first step): the chain's clause (hfStep2FamChain_stoppedClause) and the link's (hfStep22FamOn_stoppedClause_induced) composed by stoppedClause_shrinkAppend, restricted (stoppedClause_pullback) and cleaned (stoppedClause_eraseEmpty), the triples rewritten by pullback_inclusion_restrictLE, as in hfStep2SeqFamOn_isOfOrderGe.

theorem Hironaka.Manifold.BO.hfStep2SeqFamOn_outputClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (d : HFData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (hs : s = 1) (hhf1 : d.hf.OutputClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.OutputClause ψ₀ (hfStep2SeqFamOn T s d hT U hU hH hle).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The output clause of the value of Step 2 on the open (the field output_isSmoothSubmanifoldIdeal of BMOmodFam for the local value of the modified first step): the link's clause (hfStep22FamOn_outputClause_induced) through outputClause_shrinkAppend, outputClause_pullback and outputClause_eraseEmpty.

theorem Hironaka.Manifold.BO.hfStep2FamOn_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (s : ℕ) (hs : s = 1) (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.LocalMCClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hbd : d.bd₁.StoppedClauseFam) (hhf8 : d.hf.StoppedClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (hfStep2FamOn s d T hT U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The stopped clause of Step 2 with the class's hypersurface of maximal contact (hfStep2FamOn, the chosen witness of the class).

theorem Hironaka.Manifold.BO.hfStep2FamOn_outputClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (s : ℕ) (hs : s = 1) (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.LocalMCClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hhf1 : d.hf.OutputClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.OutputClause ψ₀ (hfStep2FamOn s d T hT U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The output clause of Step 2 with the class's hypersurface of maximal contact.

theorem Hironaka.Manifold.BO.hfLocalFunctorFamOn_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (d : HFData ψ₀ (IsLocalRing.tuningParam 1)) (T : Manifold.AnalyticTriple ψ₀ M) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hbd : d.bd₁.StoppedClauseFam) (hhf8 : d.hf.StoppedClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (hfLocalFunctorFamOn 1 d T hL U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The stopped clause of the local functor's value at the mark 1 (hfLocalFunctorFamOn 1): Step 2 at the mark 1! = 1 on the tuned triple, the tuning being the identity (tuned_pullback, tuned_one at the restricted triple, as in BDanFam_stoppedClause).

theorem Hironaka.Manifold.BO.hfLocalFunctorFamOn_outputClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (d : HFData ψ₀ (IsLocalRing.tuningParam 1)) (T : Manifold.AnalyticTriple ψ₀ M) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hhf1 : d.hf.OutputClauseFam) (hhfo : d.hf.IsOfOrderGeEmptyMemberFam) : AnalyticManifold.FiniteSuccession.OutputClause ψ₀ (hfLocalFunctorFamOn 1 d T hL U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The output clause of the local functor's value at the mark 1.

theorem Hironaka.Manifold.BMOmod.stepBLocalFunctorFam_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (hR8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepBLocalFunctorFam R ⋯ ⋯ ⋯ bmo₁)

The stopped clause of the local functor of the modified first step (stepBLocalFunctorFam): hfLocalFunctorFamOn_stoppedClause at the datum stepBData, from the clause of the data of Step 1a (bdanFamDataOne_stoppedClauseFam) and that of the data of the modified step (hFamDataMod_stoppedClauseFam, from the clause hR8 of the functor one dimension down).

theorem Hironaka.Manifold.BMOmod.stepBLocalFunctorFam_outputClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (hR1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepBLocalFunctorFam R ⋯ ⋯ ⋯ bmo₁)

The output clause of the local functor of the modified first step: hfLocalFunctorFamOn_outputClause at stepBData with hFamDataMod_outputClauseFam (from hR1).

theorem Hironaka.Manifold.BMOmod.stepBFunctor_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (hR8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepBFunctor R ⋯ ⋯ ⋯ bmo₁)

The stopped clause of the functor of the modified first step on the class of BO_{n,1} (stepBFunctor): the local clause descended along the maximal-contact cover (stoppedClauseFam_of_agreeFam, as in stepBFunctor_isOfOrderGe).

theorem Hironaka.Manifold.BMOmod.stepBFunctor_outputClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (hR1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (stepBFunctor R ⋯ ⋯ ⋯ bmo₁)

The output clause of the functor of the modified first step on the class of BO_{n,1} (outputClauseFam_of_agreeFam).