Lemma 29 ([Retesting a finite chart recipe]). Enlarge a saturated flag by finitely many permitted insertions without converting its old active free nodes. Suppose the primitive data can be retested on this flag with Assumption 19 …

Retest the old primitives before making a new ordinary substitution. Initially the bounded parameters introduced by the refinement are passive ordinary inputs. Old free values at the real anchor are unchanged, and the actual real formulas and their ordinary derivatives are the same. Proceed through the finite old recipe. A raw operation is available by Theorem 4.1 ([Packet calculus]). Every previously positive normalization is still bounded on its real ordinary neighborhood, so Lemma 26 ([Bounds, limits, and free derivatives]) proves its positivity on the refined flag. Its old ordinary limit identifies its exponent-zero germ. Thus a previously regular analytic or implicit step retains its limiting Jacobian and can be performed by the same theorem. The additional passive inputs are held fixed in these comparisons. Induction proves the assertion for the entire recipe. Unused inserted levels contribute only identity transitions, and later pullback introduces their actual dependence in the prescribed order. Preservation of the old free nodes is supplied by Lemma 2 ([Finite saturation and preservation of free coordinates]) in the applications.