The stop rule along a concatenation

The stop rule CenterContains S c i of Hironaka/Resolution/Algebraic/Kol07/Thm36/Affine.lean (the center at stage i contains the strict transform of the closed subscheme V(c); it locates the blow-up whose center has the generic point of the variety in the proof of [Kol07, Corollary 22]) read on a concatenation S.concat T: at an index below S.length it is the stop rule on S; at an index S.length + i it is the stop rule on T at i for the strict transform of c along S (strictTransformSeq_concat_last of Hironaka/Scheme/BlowUpSequence/ConcatTransforms.lean in the form the recursion needs). Structural recursion on S, as for centerContains_take_iff.

theorem Hironaka.Sequence.centerContains_concat_iff_of_lt {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (c : X.IdealSheafData) (i : ℕ) : i < S.length → (Resolution.CenterContains (S.concat T) c i ↔ Resolution.CenterContains S c i)

The stop rule on a concatenation below the first sequence's length is the stop rule on the first sequence.

theorem Hironaka.Sequence.centerContains_concat_add_iff {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (c : X.IdealSheafData) (i : ℕ) : Resolution.CenterContains (S.concat T) c (S.length + i) ↔ Resolution.CenterContains T (S.strictTransformSeq c (Fin.last S.length)) i

The stop rule on a concatenation at an index S.length + i is the stop rule on the second sequence at i for the strict transform along the first.