An alternating Turán inequality for normalized Euler numbers

We prove Sokal Conjecture 3.3 for every starting index n>=0 and positive shifts j,k, using the actual normalized Taylor coefficients of sec(t)+tan(t). Classical partial fractions, a uniform positive-error contraction and four parity cases establish the sign. The generating-function identity, all coefficient bridges and the complete source inequality are proved in Lean. Known subsequence results, partial fractions and finite experiments are credited rather than counted separately. 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: Bounded independent prior-art screen; twelve citing bodies inspected, some typeset bodies and comprehensive database coverage unavailable; no worldwide-priority claim.