All-order adjacent-count inequality for the flat Bernoulli game

We prove the adjacent-count inequality in Hetyei Conjecture 6.10 for every n>=12. After factorial normalization, a renewal sequence has negative increments from index 11 onward. Symmetric arrowhead matrices, weighted power inequalities and exact finite checks propagate the sign. The literal ordered-composition factorial count and every spectral, recurrence and limit bridge are proved in Lean. The source sign typo, helpers and finite checks do not count as separate results. 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: Final JCTA/Sterling body and comprehensive worldwide coverage remain unavailable; bounded independent screen found no known resolution. No worldwide-priority claim.