# P2448: Eventual unimodality of ternary subset-sum polynomials - ID: `P2448` - Reference: `ternary-subset-polynomial-unimodality` - Page: https://theoremdb.org/statements/P2448 - Record maturity: Reviewed problem with recorded work ## Problem For \(n\ge 1\), define \(P_n(x)=\prod_{k=1}^n(1+x^k+x^{2k})\). Is the coefficient sequence of \(P_n\) unimodal for every \(n\ge 11\)? ### Problem setup - **Definition.** A finite sequence is unimodal when it weakly increases up to some index and weakly decreases afterward. - **Remark.** The coefficients are symmetric because P_n is reciprocal up to its total degree. ### What counts as a solution - Prove coefficient unimodality for every n >= 11, or exhibit the least later failure. ## The answer The candidate is the r = 3 case of a unimodality theorem proved by Gert Almkvist in 1989. [1](#reference-1) **Review status:** Supported. **Lean verification:** not Lean-verified. ### Resolution argument For every positive integer \(n\), \[ P_n(q)=\prod_{k=1}^n(1+q^k+q^{2k}) =\prod_{k=1}^n\frac{1-q^{3k}}{1-q^k}. \] Almkvist studied the more general polynomial \[ f_{n,r}(q)=\prod_{k=1}^n\frac{1-q^{rk}}{1-q^k}. \] His 1989 paper proves the conjectured unimodality for \(3\leq r\leq20\), as well as \(r=100,101\), with the odd-\(r\) range beginning at \(n=11\). Setting \(r=3\) gives the candidate verbatim. Hence the coefficient sequence of \(P_n\) is unimodal for every \(n\geq11\). Dong and Ji identify the result explicitly in their introduction: their Conjecture 1.1 is the displayed product, and the paragraph after equation (1.5) records Almkvist's proved cases \(3\leq r\leq20\). The candidate is a rediscovery of this classical result. ## Work ### Proof and evidence for the resolution **Proposition 1 (Almkvist's theorem settles every n at least 11).** The candidate is the r = 3 case of a unimodality theorem proved by Gert Almkvist in 1989. For every positive integer \(n\), \[ P_n(q)=\prod_{k=1}^n(1+q^k+q^{2k}) =\prod_{k=1}^n\frac{1-q^{3k}}{1-q^k}. \] Almkvist studied the more general polynomial \[ f_{n,r}(q)=\prod_{k=1}^n\frac{1-q^{rk}}{1-q^k}. \] His 1989 paper proves the conjectured unimodality for \(3\leq r\leq20\), as well as \(r=100,101\), with the odd-\(r\) range beginning at \(n=11\). Setting \(r=3\) gives the candidate verbatim. Hence the coefficient sequence of \(P_n\) is unimodal for every \(n\geq11\). Dong and Ji identify the result explicitly in their introduction: their Conjecture 1.1 is the displayed product, and the paragraph after equation (1.5) records Almkvist's proved cases \(3\leq r\leq20\). The candidate is a rediscovery of this classical result. ### Background and intake notes Attempts should record the exact overlap inequality used between the three shifted coefficient sequences. Symmetry alone leaves local valleys near the shift boundaries. - Original intake status: Novelty and status remain unverified. Products of q-integers have a substantial unimodality literature. - Induction by convolving with 1+x^n+x^(2n) is the attractive route. - Sparse convolution does not preserve unimodality without overlap inequalities. The failures at n=8,9,10 occur late enough to defeat an induction that checks only symmetry and a central maximum. - Recorded example: Unimodality fails at n=2,4,6,8,9,10 and holds at n=1,3,5,7 within the small cases. ### Supporting results - **Proposition 2** (supported): Almkvist's theorem and exact small cases classify every positive order. [1](#reference-1) ### Runnable artifacts - **Artifact 1** (reproduced): Standard-library Python checks symmetry, total mass, and every adjacent coefficient through order 300. [1](#reference-1) ### Computational notes - Coefficients were generated by exact integer convolution for every 1 <= n <= 100. The failure set in this range was exactly {2,4,6,8,9,10}. ### Working on this Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `ternary-subset-polynomial-unimodality`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome. ## Lean verification An informal proof is recorded. A Lean formalization still needs to be attached. [Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20ternary-subset-polynomial-unimodality%0A%0AExact%20title%3A%20Eventual%20unimodality%20of%20ternary%20subset-sum%20polynomials%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fternary-subset-polynomial-unimodality%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.). ## References 1. Gert Almkvist, “Proof of a conjecture about unimodal polynomials”. Journal of Number Theory 32(1) (1989), 43-57. DOI 10.1016/0022-314X(89)90096-6. G. Almkvist, Proof of a conjecture about unimodal polynomials, Journal of Number Theory 32 (1989), 43-57, r = 3 specialization; cross-identified in Dong and Ji, Unimodality of partition polynomials related to Borwein's conjecture, Introduction, Conjecture 1.1 and the paragraph after equation (1.5) https://doi.org/10.1016/0022-314X(89)90096-6 - Also cited at Almkvist's all-n result for n at least 11, combined with the exact finite computation in tspu-artifact-sweep-300 - Also cited at Inline CPython 3 source below, executed on 2026-07-24 - journal_article; primary source; checked 2026-08-01 - Source use: original_summary - For Eventual unimodality of ternary subset-sum polynomials, the reviewed source scope is G. Almkvist, Proof of a conjecture about unimodal polynomials, Journal of Number Theory 32 (1989), 43-57, r = 3 specialization; cross-identified in Dong and Ji, Unimodality of partition polynomials related to Borwein's conjecture, Introduction, Conjecture 1.1 and the paragraph after equation (1.5). The packet makes no inference beyond that cited scope. - Source named by the research packet.