A sharp mass-three counterexample

Proved

Smooth4Laurent.mass_three_sharpness

by ryanshin · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

finitecoefficientslaurentpolynomialspositivity

The Laurent polynomial W(q)=1+q−q²+q³+q⁴ has signed coefficient sum3 and coefficient−1 at exponent2, while both (1+q)W and (1+q²)W have nonnegative coefficients at every integer exponent.

Preamble

import Mathlib

set_option autoImplicit false

/-- The explicit sharp mass-three Laurent polynomial is 1+q-q²+q³+q⁴. -/

Formal statement

theorem Smooth4Laurent.mass_three_sharpness :
    let w : ℤ →₀ ℤ := Finsupp.single 0 1 + Finsupp.single 1 1 -
      Finsupp.single 2 1 + Finsupp.single 3 1 + Finsupp.single 4 1
    (∀ j : ℤ, 0 ≤ w j + w (j - 1)) ∧
      (∀ j : ℤ, 0 ≤ w j + w (j - 2)) ∧
      w.sum (fun _ a => a) = 3 ∧ w 2 = -1 := by
  sorry

Source

Ryan Shin research workspace, unpublished cycle9_positive_quotient_lemma.md (2026), section1, Integer Laurent positivity. Source SHA-256 73cb004e73b4f14e8a2a4bc5f1c4b345f69c8390f060a76e284b5d44b1d6a925. No public URL. These are newly authored coefficient-function interfaces to the manuscript statements.

Read-back

What the Lean code literally says, in plain math · Codex independent blind auditor; exact model identifier unavailable

Let $w:\mathbb Z\to\mathbb Z$ be the finitely supported function with $w(0)=w(1)=w(3)=w(4)=1$ , $w(2)=-1$ , and $w(j)=0$ at every other integer $j$ . The assertion is the conjunction of four statements: $w(j)+w(j-1)\geq0$ for every integer $j$ ; $w(j)+w(j-2)\geq0$ for every integer $j$ ; the sum of $w(j)$ over its finite support equals $3$ ; and $w(2)=-1$ . Both universal conditions include all negative indices, zero, and all positive indices, with every index subtraction performed in the integers. This declaration concerns that particular function and has no hypotheses.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by ryanshin · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph