Step 2 of Theorem 103 as a compatible family: Step 2.2 and the assembly on an open #

Step 2 of the proof of [Kol07, Theorem 103] runs on a triple (X, I, E) with a global hypersurface of maximal contact H: Step 2.1 clears the transforms of the boundary members from the cosupport by applying Lemma 102 member by member, and Step 2.2 "restricts everything to the birational transform of H", that is, applies Lemma 102 once more to (X_r, I_r, H_r + E_r) at the member H_r, after replacing I_r by its tuning once more ([Kol07, 104, Step 2.2]). This module builds Step 2 in the compatible-family form ([Wlo09, Theorem 2.0.3 (1), (4)]), where the value on a triple is a finite blow-up sequence on every relatively compact open subset U, and Lemma 102's data are themselves compatible families (FamilyData.lean), whose values can only be read on relatively compact opens.

CompatibleFamily.changeTriple — a compatible family for T read as one for another triple on the same manifold (the fields do not mention the triple); it feeds the family on the tuned triple back to the class of the original.
BO.stepHFamFunctor, hfStep22Functor — Lemma 102's family at the greatest member of the boundary, as a family functor on the class stepHClass s of triples with a greatest member (Step22Defs.lean); and the family functor of Step 2.2: the data at the greatest member at the re-tuned mark tuningParam s, applied to the tuned triple and read back on the original.
The triple of Step 2.2 over an arbitrary sequence L of order ≥ s (step22TripleOf, Step22Pullback.lean): its boundary E^{exc}_r + H_r has simple normal crossings (isSnc_step22BoundaryOf), because every centre of L lies in the transforms of H ([Kol07, Theorem 80 (1)]) so that the exceptional divisors meet H_r properly (the new exceptional divisors "have simple normal crossings with the birational transforms of H", Step 2.1 of the proof); the triple lies in BOClass s and in stepHClass s, its greatest member being H_r (idxHOf).
Step 2 on a relatively compact open U (BO.step2SeqFamOn): the chain of Step 2.1 (Step21Fam.lean) is run over the exhaustion opens M_{n₀+r+1} ⊋ ⋯ ⊋ M_{n₀+1} ⊋ M_{n₀} ⊇ closure U (r the number of nonempty boundary members) and read at its state over M_{n₀+1} (step2FamChain), a sequence L on M_{n₀+1} of order ≥ s; the triple of Step 2.2 over L (step22TripleFam) is fed to the family functor of Step 2.2, whose value is read on the lifted range of M_{n₀} ⊆ M_{n₀+1} at the last stage of L (step2ReadOpen, step22FamOn); the result is appended to L (shrinkAppend, FamilyChain.lean), the whole is restricted to U and its empty blow-ups are deleted ([Kol07, 32]). The triple of Step 2.2 needs the order clause of Step 2.1's sequence on the open (the controlled transform is nonzero, the boundary has simple normal crossings), which is the invariant carried by the chain's state.
The values on the class LocalMCClass s (hfStep2FamOn, with the class's own hypersurface of maximal contact chosen) and of the local functor (localFunctorFamOn: Step 2 at the mark tuningParam m on the tuned triple, Step 1 of the proof), with the absence of empty centres.

Every construction comes in two forms: hf…, over arbitrary data d : HFData ψ₀ s of Step 2 (HFamData.lean: Step 2.1's data d.bd₁ and the data d.hf for the hypersurface step at the re-tuned mark), and the plain form, its instance at Lemma 102's data HFData.ofBDanFamData bd s for bd : ∀ s, BDanFamData ψ₀ s, which is how Kollár proceeds. The general form is what the modified algorithm of Włodarczyk (the proof of [Wlo09, Theorem 7.4.1]) requires, where the hypersurface step is taken from the modified marked resolution (Modified/StepBData.lean).

The clauses of Theorem 103 for these values are proved in Step22FamFull.lean (order ≥ s with the full boundary), Step22FamOrdLt.lean (the order drops), Step22FamFunctoriality.lean, Step2Assembly.lean (compatibility under restriction), Step2AssemblyComm.lean (commutation with local analytic isomorphisms, indifference to empty members) and FamilyIndependence.lean (independence of the hypersurface of maximal contact); the compatible family of the local functor is assembled in LocalFunctorFam.lean.

Step 2 of Theorem 103 as a compatible family: Step 2.2 and the assembly on an open #

Lemma 102's family at the greatest member #

The triple of Step 2.2 over a sequence of order ≥ s #

Step 2 on a relatively compact open #

The values on the class with a global hypersurface of maximal contact #

The triple of Step 2.2 over a sequence of order `≥ s` #