Computer-assisted KAM stability of periodic orbits near the Earth–Moon triangular point in Sun-perturbed models, and where a measure estimate stops

Three elliptic periodic orbits near the Earth–Moon L4 point in Sun-perturbed models — PO2 and PO3 of the bicircular model and the 2:1 resonant orbit of the planar Hill four-body problem — are KAM stable in the sense of Kapela and Simó. We verify with interval arithmetic their four conditions for PO2 and PO3 in the planar bicircular model, for PO2 also with derived values (planar) and in the spatial model (standard values), and for the 2:1 orbit. By the KAM theorem for analytic symplectic maps near an elliptic fixed point, whose source (Arnold and Avez 1967, cited by Kapela and Simó) we could not read, every neighbourhood of the fixed point contains a positive-measure set of invariant tori. We record where an a posteriori estimate of the measure of the tori near PO2 (planar) stops, saying nothing about the tori: an aliasing bound makes the averaged torsion singular and a non-rigorous control misses by over a hundred orders of magnitude. What this work does not claim: it concerns the models, not the real Moon, and asserts neither Lyapunov stability nor anything about orbits outside the tori; it makes no claim of novelty. No recommendation for spacecraft operation or mission design is made. This record holds the paper (PDF, LaTeX source and template, the scripts that fill the numbers from the records and check them) together with the publication bundle: the certificates (CAPD programs and their outputs, the normal-form and verification scripts), the frozen records (claims, criteria, errata, project log), the bibliographic ledger (identifiers resolved mechanically; the abstracts of third-party records are removed from the public copy), and the findings and response tables of every independent review round. The paths quoted in the paper refer to the bundle. The certificates are frozen and re-runnable; every statement was reviewed by separate AI-model sessions sharing no context with the authoring system. The work was produced by AI language models under a written research constitution, with a human principal deciding at the stopping points; Appendix E of the paper (Disclosure) records the roles.