An odd-degree identity for polynomial values at derivative roots

We prove Wojnar, Wojnar and Brin Conjecture 2 for every complex polynomial of odd degree, with derivative roots counted with multiplicity. Normalized Newton moments extend the means polynomially in the remaining degree; an apolar self-pairing and finite differences yield the identity. The literal source means and arbitrary-polynomial endpoint are proved in Lean. Classical Newton, apolarity and finite-difference ingredients are credited. 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: Toda1934 full body unread; actual1936/1940 neighboring formulas and classical apolarity read/credited. Independent review found no explicit old stronger source endpoint and recommends acceptance under documented-prior/no-known-resolution standard with this material limitation. Absolute priority not certified.