The end of Step 2.1 for a round of order 1

Step 2.1 of the proof of [Kol07, Theorem 103] (item 104, Step 2.1) passes over the members of the boundary; at its end the birational transform of every original member misses the cosupport of the weak transform (disjoint_cosupp_step21_final, Hironaka.Resolution.Algebraic.OrderReduction.Step21Disjoint). For a round of order 1 the marked transform with mark 1 is the weak transform ([Kol07, Remark 67], IsOrderGeSeq.markedTransformSeq_eq_weakTransformSeq) and the cosupport {x | 1 ≤ ord x} is the support (one_le_ord_iff), so the transforms of the members miss the SUPPORT of the marked transform. This is the input at the end of Step 2.1 for the passage of the statements CP1 and CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) from the exceptional sub-family to the full boundary along Step 2.2 (disjoint_support_markedTransformSeq_strictTransformSeq). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step22.

theorem Hironaka.Resolution.disjoint_support_markedTransformSeq_step21_final {k : Type u} [Field k] [CharZero k] {n : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ 1) (bd : (j : ℕ) → BDData n 1 j) (hm : T.I.maxOrd = 1) {i : ℕ} (hi : i < Fintype.card T.E.ι) : Disjoint ↑((↑(BO.step21Seq T hn hmax bd (Fintype.card T.E.ι))).markedTransformSeq T.I 1 (Fin.last (↑(BO.step21Seq T hn hmax bd (Fintype.card T.E.ι))).length)).support ↑((↑(BO.step21Seq T hn hmax bd (Fintype.card T.E.ι))).strictTransformSeq (T.E.nth ⟨i, hi⟩) (Fin.last (↑(BO.step21Seq T hn hmax bd (Fintype.card T.E.ι))).length)).support

At the end of Step 2.1 of a round of order 1 (T.I.maxOrd = 1), the birational transform of every original member misses the support of the marked transform of (T.I, 1) ([Kol07, 104, Step 2.1] with [Kol07, Remark 67]): disjoint_cosupp_step21_final on the weak transform, markedTransformSeq_eq_weakTransformSeq and one_le_ord_iff.