A fortieth-derivative obstruction to the Mills-ratio complete-monotonicity conjecture

For the actual Gaussian Mills ratio r, the quotient -r^2/r' has negative fortieth derivative throughout some interval of strictly positive regular inputs. This refutes Ferreira–Simon Conjecture 3 already at n=0. A degree-21 integer polynomial in pi/2, rational Bernstein bounds and continuity supply the certificate. The Gaussian tail, derivative identification and interior conclusion are proved in Lean. No minimal derivative order or contradiction of the square-root-input proposition 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: No MathSciNet/zbMATH/direct Scopus sweep; OpenAlex3 records are not exhaustive; one Fox linkage erroneous; actual bodies and additional leads compared; No absolute worldwide priority claim