Step 2.1 of Theorem 103 as a compatible family #

Step 2.1 of the proof of [Kol07, Theorem 103] applies Lemma 102 to the nonempty boundary members in turn, each application on the triple induced at the end of the previous one. In the compatible-family form the data of Lemma 102 are compatible families (BDanFamData ψ₀ s, FamilyData.lean), whose values can only be read on relatively compact opens; the value step21FamOn bd T hT U hU of Step 2.1 on a relatively compact open U is therefore computed along a finite shrinking chain of the opens M_{n₀+r} ⋑ ⋯ ⋑ M_{n₀} ⊇ closure U of a compact exhaustion of M, r the number of nonempty members: the k-th member's family is read on the last stage of the sequence built so far, at the range of the lift of the inclusion M_{n₀+r-k-1} ⊆ M_{n₀+r-k} (relatively compact by the properness of the blow-downs, FamilyChain.lean), the sequence built so far is restricted to the smaller open and the value appended (shrinkAppend); at the end the sequence is restricted to U and its empty blow-ups deleted ([Kol07, 32]). The triple carried along the chain is the pull-back along the lifts of the induced triples (AnalyticTriple.induced), a member of the class by boClass_induced and the stability of the class under pull-back; it equals the induced triple of the restricted sequence (induced_pullback), which the proofs of the clauses use.

Conventions. The compact exhaustion of M is chosen once (exhaustion M), and the value uses one fixed chain; step21FamOn_chain_indep (Step21FamIndep.lean) shows that the value does not depend on the chain up to empty blow-ups.

isCompact_closure_preimage_val_of_closure_subset, isCompact_closure_range_restrictLE — relatively compact opens inside an open restriction;
exhaustion, exhaustionIdx, chainOpens — the compact exhaustion, an index n₀ with closure U ⊆ M_{n₀}, and the chain W k := M_{n₀ + (r − k)};
ChainState T s W — the state of the chain over W: the sequence built so far on M.restrict W with its order clause; ChainState.init; ChainState.linkWith (the generic link: a compatible family C on the induced triple at the last stage, with the order clause of its value on the reading open readOpen, restricts the sequence so far to the smaller open and appends the value, shrinkAppend, keeping the order clause); ChainState.link (one step of Step 2.1, at one member: linkWith at Lemma 102's family);
step21FamAux, memberCount, step21FamChain, step21FamOn — the recursion over a list of members, the number of nonempty members, the chain over them, and the value on U;
step21FamOn_isOfOrderGe, step21FamOn_isOfOrder, step21FamOn_noEmptyCenters — the value on U is a smooth blow-up sequence of order ≥ s, indeed of order exactly s, starting with the triple restricted to U, without empty blow-ups.

The remaining clauses are proved in Step21FamCosupp.lean (the cosupport misses the transforms of the members), Step21FamIndep.lean (independence of the chain, compatibility under restriction, commutation with local analytic isomorphisms) and Step21FamIndiff.lean (indifference to empty boundary members); the compatible family of Step 2.1 and Step 2.2 in this form are assembled in Step22Fam.lean.

Step 2.1 of Theorem 103 as a compatible family #

Relatively compact opens inside an open restriction #

The chain of exhaustion opens #

The chain state #