A recursive Buchstab switching improvement for the greatest prime factor of n^2+1

Immutable release v1.2.2 of the public verification archive accompanying the working paper “A recursive Buchstab switching improvement for the greatest prime factor of n^2+1”. DOI: https://doi.org/10.5281/zenodo.22172072 Concept DOI: https://doi.org/10.5281/zenodo.22140874 GitHub: https://github.com/CGandGameEngineLearner/landau-fourth-problem-1.323/releases/tag/v1.2.2 Contents include a Lean 4 project (toolchain v4.22.0 / Mathlib v4.22.0), a fixed-width C++ certificate, and an arbitrary-precision Python audit for the finite numerical inequalities used in the sieve budget (canonical grid 1200×300×160; reported saving_lower=0.032303187971, CERTIFIED=YES). These materials check the finite certificate layer only. They do not prove the Grimmelt–Merikoski Type I/II analytic inputs, the Mellin–Perron transfer, or the main theorem by themselves. Verification code is GPL-2.0-only; manuscript prose is CC BY 4.0.