Computing the invariant circle and its stable manifolds for a 2‑D map by the parameterization method: effective algorithms and rigorous proofs of convergence

The paper proves an a posteriori Nash–Moser theorem for the invariance equation F[W,a,λ]=0 on anisotropic scales X^{r,δ}, using automatic reducibility, cohomological equations, and a quasi-Newton iteration interleaved with Cr smoothing. The candidate solution follows the same overarching scheme: (i) define smoothing on X^{r,δ}, (ii) use the reducibility identity Df(W)DW − (DW∘A)B = De, (iii) solve the lower–triangular transport system via Neumann-series cohomological inverses, and (iv) run a preconditioned Newton–smoothing iteration with superexponential decay of the defect and an a posteriori bound. These match the paper’s core ideas and its statement of Theorem 4 under Condition-0, including the series inversions and the superexponential convergence of the smoothed scheme. However, the candidate differs on two technical points: it asserts a right inverse that loses up to two derivatives and treats F as C^2 tame on X^{r,δ}, whereas the paper emphasizes that the linearized solve entails no loss of regularity (within a restricted range of r) and that composition in Cr is not differentiable as a map Cr→Cr; the abstract theorem is designed to accommodate this by estimating DF, D^2F in lower norms and by an approximate inverse η[u] that is bounded on the same r-level. Despite these differences, the conclusions (existence, superexponential convergence, a posteriori bound) agree.