CP3 along Step 2 and at every stage of the tower

Step 2 of the proof of [Kol07, Theorem 103] is Step 2.1 followed by Step 2.2 (step2Seq); the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along it (cp3For_step2Seq) is cp3For_concat of cp3For_step21Seq and cp3For_step22. The tower step (cp3BOAt_succ_of_cp3BMOAt) is that of CP1 (cp1BOAt_succ_of_cp1BMOAt, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step2): BO_{n+1,1} is evaluated through the local cover of [Kol07, Theorem 105], on whose pieces a hypersurface of maximal contact exists and the run is Step 2 on the tuned triple (functor_seq_localClass, maxContactCase at max-ord I = 1, the tuning at the mark 1 being the identity); CP3 on the pieces descends to the triple (cp3For_of_pullback_cover), and the inductive input is the stage-n marked family read through the amalgam (amalgam_seq, seq_congr_mark). The induction of [Kol07, 70] closes: the base cp3BMOAt_zero, the Step 2 descent, and the Step 1 reduction cp3BMOAt_succ_of_cp3BOAt (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1) give cp3BMOAt; 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 every centre of bmoOneRun T hm is classified at each of its points (cp3For_bmoOneRun). This completes the proof of CP3 in its universal form. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5.

theorem Hironaka.Resolution.cp3For_step2Seq {k : Type u} [Field k] [CharZero k] {N : ℕ} (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (N - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE N) (hmax : T.I.maxOrd ≤ 1) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 H) (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → CP3For ((B k).seq T' hT') T'.I T'.E) : CP3For (BO.step2Seq T hn hmax (fun (m j : ℕ) => BD.bdData N m j Dom B ⋯ hB hsm hbc) ⋯ hH hle) T.I T.E

CP3 along Step 2 with the data bdData (Step 2 of the proof of [Kol07, Theorem 103]): cp3For_concat of cp3For_step21Seq and cp3For_step22.

theorem Hironaka.Resolution.cp3For_step2Seq_of_eq_one {k : Type u} [Field k] [CharZero k] {N : ℕ} (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (N - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE N) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (m : ℕ) (hm1 : m = 1) (hmax' : T.I.maxOrd ≤ ↑m) (hm : 1 ≤ m) (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → CP3For ((B k).seq T' hT') T'.I T'.E) : CP3For (BO.step2Seq T hn hmax' (fun (m j : ℕ) => BD.bdData N m j Dom B ⋯ hB hsm hbc) hm hH hle') T.I T.E

Step 2 at a mark m = 1 carried as a variable (the mark of the tuned triple).

theorem Hironaka.Resolution.cp3BOAt_succ_of_cp3BMOAt {k : Type u} [Field k] [CharZero k] (n : ℕ) (h : CP3BMOAt k n) : CP3BOAt k (n + 1)

The Step 2 descent along the tower ([Kol07, Theorem 105], [Kol07, 70]): CP3 for BO_{n+1,1} from CP3 for BMO_{n,1} through the local cover of Theorem 105, on whose pieces the run is Step 2 on the tuned triple.

theorem Hironaka.Resolution.cp3BMOAt {k : Type u} [Field k] [CharZero k] (n : ℕ) : CP3BMOAt k n

CP3 in its universal form along the tower ([Kol07, 70]): the base cp3BMOAt_zero, the Step 2 descent cp3BOAt_succ_of_cp3BMOAt, the Step 1 reduction cp3BMOAt_succ_of_cp3BOAt.

theorem Hironaka.Resolution.cp3For_bmoOneRun {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) : CP3For (bmoOneRun T hm) T.I T.E

CP3 in its universal form for the dimension-free run (dimFreeBMO_seq, bmoClass_of_bmoClassFree): every centre of bmoOneRun T hm is classified at each of its points.