Mass-two positivity from two positive Laurent products

Proved

Smooth4Laurent.mass_two_positive

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

finitecoefficientslaurentpolynomialspositivity

Let W(q)=∑ wⱼqʲ have integer coefficients and finite support. If (1+q)W and (1+q²)W are coefficientwise nonnegative and the signed sum W(1)=2, then every coefficient of W is nonnegative. Negative exponents are allowed and no degree or support-width bound is imposed.

Preamble

import Mathlib

set_option autoImplicit false

/-- Mass two forces positivity when both specified Laurent products are positive. -/

Formal statement

theorem Smooth4Laurent.mass_two_positive
    (w : ℤ →₀ ℤ)
    (hOne : ∀ j : ℤ, 0 ≤ w j + w (j - 1))
    (hTwo : ∀ j : ℤ, 0 ≤ w j + w (j - 2))
    (hMass : w.sum (fun _ a => a) = 2) :
    ∀ j : ℤ, 0 ≤ w j := 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

For every finitely supported function $w:\mathbb Z\to\mathbb Z$ , if $w(j)+w(j-1)\geq0$ and $w(j)+w(j-2)\geq0$ for every integer $j$ , and if the sum of $w(j)$ over its finite support is exactly $2$ , then $w(j)\geq0$ for every integer $j$ . The entries and the sum are integers, all shifts use integer subtraction, and the conditions range over negative indices as well as zero and positive indices. Entries may be zero and the inequalities are non-strict; the zero function cannot satisfy the sum hypothesis.

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