A strict valley in Keith's multicolor partition array

A three-color box-partition array for the 25 by 25 box at size 325 has three consecutive points on a line of step (1,-2) with coefficients 53130, 50600 and at least 52900. This refutes Keith's multicolor linear-cut unimodality conjecture. The actual generating polynomial and an injection establishing the last bound are proved in Lean. The original Dousse–Kim two-color conjecture remains untouched. 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: Actual arXiv source and predecessor inspected; independent search found no known prior multicolor resolution. Final typeset Keith body unread after403; Wagner thesis assessed through official abstract/chapter descriptions, complete body unread. Citing-body coverage bounded, no exhaustive2026/worldwide priority claim. Parent addendum clarifies report wording.