The generating-function smallness bound gives injectivity of both mixed-coordinate maps on the same buffered source domain.

theorem KamProject.Arnold1963.generating_small_sixteenth {n : ℕ} (hn : 0 < n) {r : NNReal} (hr : 0 < r) {M : ℝ} (hM : M < ↑r ^ 2 / (16 * ↑n)) : M / ↑r / ↑r < 1 / 16

theorem KamProject.Arnold1963.generating_injOn {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {V : Set (ComplexPhaseSpace n)} {r : NNReal} {M : ℝ} (hr : 0 < r) (hS : AnalyticOnNhd ℂ S V) (hM : NormBoundOn S V M) (hsmall : M / ↑r / ↑r < 1 / 16) : Set.InjOn (generatingInput S) (erosion V r) ∧ Set.InjOn (generatingOutput S) (erosion V r)