Sharp maximal index for separately sorted arithmetic and geometric means in every dimension at least five

For each probability vector in dimension d>=5, form and independently sort all d^2 ordered arithmetic means and all d^2 ordered geometric means. The sum of their respective largest k entries is at most d for every probability vector exactly when k<=2d-5. Incidence bounds, Cauchy–Schwarz and a sharpness family prove the classification. The complete separately sorted source statement is certified in Lean. 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 earlier resolution found in inspected primary and full-body citing sources. Citation indexes are incomplete; one published citing body and subscription indexes remain unread. Author listings are not full-body surveys. Parent addendum qualifies review scope; no absolute worldwide priority certified.