CP1 across the deletion of empty blow-ups

Step 2.2 of the order reduction is the deletion of the empty blow-ups from the blow-up of Z₋₁ followed by the pushforward of the run on the hypersurface ([Kol07, 34.1] and [Kol07, 32] for the deletion; Hironaka.OrderReduction.Step22*). CP1 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1For) passes across the deletion: an empty centre (⊤) contains no nonempty strict transform, and the strict transform of the component stays nonempty before its absorption (the generic lift, exists_genericLift), so the first containing indices correspond (centerContains_eraseEmpty_iff, eraseIdx, exists_eraseIdx_eq); the stage data agree through eraseEmpty_take, the _eraseEmpty_last identities along the last-stage isomorphism eraseEmptyLastHom and the bridges of Hironaka.Scheme.BlowUpSequence.TakeLast, and the induced family of the erased sequence differs from the pullback of the original's by unit members only (eraseEmbeds_eraseEmpty), which the chain form ignores (chainRelativeAt_of_extendsByEmpty, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainExtendsByEmpty). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3EraseEmpty.

theorem Hironaka.Resolution.eraseIdx_lt_of_ne_top_of_lt {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {l m : ℕ} (hl : l < S.length) : S.center ⟨l, hl⟩ ≠ ⊤ → l < m → eraseIdx S l < eraseIdx S m

A non-empty centre advances the erased index: for l < m with Z_l ≠ ⊤, eraseIdx S l < eraseIdx S m.

theorem Hironaka.Resolution.cp1For_eraseEmpty {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) {η : ↥X} (hη : η ∈ I.support.genericPoints) (hηE : ∀ (j : E.ι), η ∉ (E.component j).support) (hIc : I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (hS : S.IsOrderGeSeq f I 1 E) (h : CP1For S I E η) : CP1For S.eraseEmpty I E η

CP1 across the deletion of empty blow-ups: CP1 along a run of order ≥ 1 for (I, 1, E) passes to the erased run. The member hypotheses (cp1For_concat's) keep the component's strict transform nonempty before its absorption, so that a deleted centre never counts as containing it.