Odd-total lower bound for simple SOC representations

If positive integer weights have odd total, every literal simple second-order-cone representation of their weighted geometric mean has at least as many constraints as original variables. This answers Wang's 2024 Section 7 open question (2), rather than newly resolving the older cardinality bound in the related MathDB record. The proof initially allows repeated indices, self-loops and cycles; the structural and parity conclusions follow from soundness. The full representation endpoint is proved 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: Alzalg2026 technical full body unread; No MathSciNet/zbMATH sweep; No absolute worldwide priority claim