CP1 at every stage of the tower and along bmoOneRun

The induction of [Kol07, 70] for the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): in dimension 0 the ideal of a triple is the unit ideal (Triple.I_eq_top_of_hasDimLE_zero), so V(I) has no generic point and CP1 holds vacuously (cp1BMOAt_zero); CP1BMOAt n gives CP1BOAt (n + 1) (the Step 2 descent, cp1BOAt_succ_of_cp1BMOAt of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step2) and CP1BOAt (n + 1) gives CP1BMOAt (n + 1) (the Step 1 reduction, cp1BMOAt_succ_of_cp1BOAt of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step1), so CP1 holds at every stage (cp1BMOAt). The run bmoOneRun of the loop BED (Hironaka.Resolution.Algebraic.Wlo05.Embedded) is the marked family of the tower at the triple's own dimension (dimFreeBMO_seq, by rfl), so CP1 holds along it for every generic point of V(I) off the boundary at which I is reduced (cp1For_bmoOneRun_of_cp1BMOAt), by the argument of claimKC_of_claimBMOAt (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimAt). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Main and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Absorbed.

theorem Hironaka.Resolution.cp1BMOAt_zero (k : Type u) [Field k] [CharZero k] : CP1BMOAt k 0

The base of the tower ([Kol07, 70]): in dimension 0 the ideal is the unit ideal, so V(I) has no generic point and CP1 holds vacuously.

theorem Hironaka.Resolution.cp1BMOAt (k : Type u) [Field k] [CharZero k] (n : ℕ) : CP1BMOAt k n

CP1 at every stage of the tower ([Kol07, 70]): the Step 2 descent, then the Step 1 reduction.

theorem Hironaka.Resolution.cp1For_bmoOneRun_of_cp1BMOAt {k : Type u} [Field k] [CharZero k] (h : ∀ (n : ℕ), CP1BMOAt k n) (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (bmoOneRun T hm) T.I T.E η

CP1 along bmoOneRun for every generic point of V(I) off the boundary at which I is the reduced ideal of its closure: bmoOneRun is the marked family of the tower at the triple's own dimension (dimFreeBMO_seq).