Part III: The Bi-Lipschitz Case
Now X, T are metric spaces, X compact, with the hypotheses of Theorem B: each
slice f(p,\cdot) is a homeomorphism \mathrm{slice}(p) : X \to T; f is jointly
L-Lipschitz for the max-metric on P \times X; and every \mathrm{slice}(p)^{-1}
is L-Lipschitz. Note two consequences used repeatedly: each \mathrm{slice}(p) is
L-Lipschitz (freeze the first argument of f), and
d\bigl(\mathrm{slice}(p)(x), \mathrm{slice}(p')(x)\bigr) \le L\, d(p,p') \quad \text{for all } x
(freeze the second argument; both are instances of joint Lipschitzness under the max-metric).
The reduction to a reparametrization, the split into an easy regime (N \le k active
indices) and the main regime, and the degenerate cases (X = \emptyset, L = 0)
are handled in Section 9.1, whose Lean counterpart lives with the
reduction (the theorems reparam_biLip_exists and
biLipschitz_of_reparam). The main regime upgrades the constructions of Part II in
three ways — a Lipschitz partition of unity (Section 9.2), a near-identity handle
family (Section 9.3), and a reparametrization that is Lipschitz in x with a small
constant (Section 9.4) — and adds the fixed-point analysis of the slices
(Section 9.5).