The bridge from the CP loop to the clauses of the theorem

Hironaka.Resolution.Algebraic.Wlo05.EmbeddedEndBridge derives the clauses of Wlo05, Theorem 1.0.2 for BED from the end data EmbeddedEnd ⟨TX, 1⟩ (componentIdeals TX) ∅ (BED TX) as a hypothesis: the final strict transform of Y is the product of the final strict transforms of its components, snc with the boundary, hence smooth. This module obtains the end data from the statements CP1–CP6 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) instead of the hypotheses ClaimKC, StratumBlowUp and CentersInNonmonomialSupportOrStratum. The CP side of the end data: the snc clause for every member (hasSncWith_strictTransformSeq_bedAux_last_of_invCE) — Włodarczyk's "the strict transforms Ỹᵢ of Yᵢ are smooth and disjoint" and clause (c) of [Wlo05, Theorem 1.0.2], from the loop theorem of CP5 at the round where the member is absorbed — and the remaining clauses, the final strict transforms of the members pairwise disjoint and the marked transform of the ideal their product, which are the end identity of CP6 (markedTransformSeq_bedAux_last_eq_prod, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop). The assembly embeddedEnd_bedAux_of_invCE and its instance embeddedEnd_BED_of_invCE at the entry (X, I_Y, ∅) feed the clauses through Hironaka.Resolution.Algebraic.Wlo05.EmbeddedEndBridge (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses). The conclusions are those of [Wlo05, Theorem 4.7.1]; the route through CP1–CP6 is not in the literature.

theorem Hironaka.Resolution.hasSncWith_strictTransformSeq_bedAux_last_of_invCE {k : Type u} [Field k] [CharZero k] (N : ℕ) (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) : C.card = N → InvCE T.I T.E C → ∀ c ∈ C, ((bedAux T hm C).totalTransformSeq T.E (Fin.last (bedAux T hm C).length)).HasSncWith ((bedAux T hm C).strictTransformSeq c (Fin.last (bedAux T hm C).length))

Every member of a state satisfying InvCE is absorbed in some round of the loop; from that round on its strict transform is protected (the entry protectedState_isolatedTriple_of_absorbed, then the loop theorem protected_bedAux), so at the end of the loop it has simple normal crossings with the final boundary ([Wlo05, Theorem 4.7.1]). Strong induction on the number of members along bedAux: a member still live at the absorbing stage of the round is a remaining member of the isolated state (invCE_isolatedTriple), and no member survives a round without absorption (exists_centerContains_bmoOneRun_of_invCE).

theorem Hironaka.Resolution.embeddedEnd_bedAux_of_invCE {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) : EmbeddedEnd T C ∅ (bedAux T hm C)

The end result of the loop from CP1–CP6 ([Wlo05, Theorem 4.7.1]): on a state satisfying InvCE the loop ends with the final strict transforms of the members pairwise disjoint and the marked transform of the ideal their product (the end identity of CP6, markedTransformSeq_bedAux_last_eq_prod), each final strict transform snc with the final boundary (hasSncWith_strictTransformSeq_bedAux_last_of_invCE, CP5), and nothing protected.

theorem Hironaka.Resolution.embeddedEnd_BED_of_invCE {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (hE : IsEmpty TX.E.ι) [AlgebraicGeometry.IsReduced TX.I.subscheme] : EmbeddedEnd { toTriple := TX, m := 1 } (componentIdeals TX) ∅ (BED TX)

The end result of the loop for BED at the entry (X, I_Y, ∅) with the irreducible components of the reduced Y as members (embeddedStateData_componentIdeals): the end data of BED TX from CP1–CP6. Clause (c) of [Wlo05, Theorem 1.0.2] follows through BED_strictTransform_last_smooth_of_embeddedEnd and BED_hasSncWith_strictTransform_last_of_embeddedEnd.