Davis all-degree rational-function conjecture via a fourth-moment bound

We prove Davis Conjecture 3.1 strictly throughout its stated degree and real-variable domain. A finite detailed-balance identity rewrites the source quotient through second and fourth moments. A general comparison covers degrees at least 43, and 38 exact polynomial certificates cover the remaining degrees. The explicit source equation-2.4 difference remainder and full bound are certified in Lean; Euclidean division is not separately formalized. No optimality or separate critical-point conjecture is claimed. AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review. The accompanying Lean certificate covers the precise scoped main statement; inspect the formal endpoint, assumptions and provenance in the supporting package. Prior-art investigations are documented bounded searches, not worldwide-priority certification. Original prose is offered under CC BY 4.0 and original code/Lean under MIT; third-party rights and existing notices are preserved. The public supporting ZIP contains original proof sources and verification evidence, with bibliographic links and hashes instead of redistributed third-party source manuscripts. Recorded prior-art/source-access limits: Final paginated IJMM5(2010)129-148 body unlocated; actual arXiv and revised author-hosted2010 manuscript read and agree verbatim on conjecture; Euclidean division not separately formalized; source explicit equation2.4 difference used without residual premise; Bounded independent primary-source/follow-up/subsumption screen; no known prior resolution found; No MathSciNet/Scopus/Google Scholar sweep; S2 429; zbMATH inconclusive; Zero indexed citers and empty MathDB not treated as global novelty certificate; no worldwide priority claim