Four interior roots in Yuster's entropy polynomial

At k=48, the canonically parameterized polynomial in Yuster Conjecture 3.9 has at least four distinct roots strictly between zero and one. Rational parameter enclosures and five exact sign checks give the certificate. Lean proves the literal coefficients, parameter condition, four real roots and root-count contradiction. No smallest example, exact total root count or refutation of the separate known entropy inequality 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 prior root-count refutation located. Full later Yuster–Yashfe manuscript not located; Wakhare publisher full body not separately read. Closest actual primary arXiv sources and known true entropy theorem compared and credited.