A negative Laurent coefficient forces total mass at least three

Proved

Smooth4Laurent.negative_mass_ge_three

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

finitecoefficientslaurentpolynomialspositivity

Let W(q)=∑ wⱼqʲ be an integer Laurent polynomial with finite support. Suppose wⱼ+wⱼ₋₁≥0 and wⱼ+wⱼ₋₂≥0 for every integer j, equivalently (1+q)W and (1+q²)W are coefficientwise nonnegative. If any coefficient of W is negative, then the signed coefficient sum W(1) is at least3.

Preamble

import Mathlib

set_option autoImplicit false

/-- The integer-coefficient, finite-support positivity threshold from Cycle9 §1. -/

Formal statement

theorem Smooth4Laurent.negative_mass_ge_three
    (w : ℤ →₀ ℤ)
    (hOne : ∀ j : ℤ, 0 ≤ w j + w (j - 1))
    (hTwo : ∀ j : ℤ, 0 ≤ w j + w (j - 2))
    (hNegative : ∃ j : ℤ, w j < 0) :
    3 ≤ w.sum (fun _ a => a) := 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 there exists at least one integer $j$ with $w(j)<0$ , then the sum of $w(j)$ over its finite support is at least $3$ . The entries and the total sum are integers, all index subtractions are integer operations, and every positive, zero, and negative index is covered. The two pair-sum conditions allow equality, but the hypothesis on an individual entry is strictly negative, so a zero function or a function with only nonnegative entries does not satisfy all 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