An integer-affine function nonnegative everywhere has zero slope

Proved

Smooth4Algebra.integer_affine_nonnegative

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

orderedalgebrarealanalysis

Let $a,b\in\mathbb R$ . If

a+nb\ge0\qquad\text{for every }n\in\mathbb Z,

then $b=0$ .

This is the elementary all-integer affine-rigidity step used in the norm-invariance discussion. It does not assert the topology, the Laurent factorization, or the Alexander-polynomial theorem.

Preamble

import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.Data.Real.Basic
set_option autoImplicit false

Formal statement

theorem Smooth4Algebra.integer_affine_nonnegative
    (a b : ℝ) (h : ∀ n : ℤ, 0 ≤ a + (n : ℝ) * b) : b = 0 := by sorry

Source

Newly authored from cycle7_band_twist_theory.md, norm-invariance/affine nonnegativity discussion; SHA-256 e81d47cad862e6538d0997826a67a43c367fd4096fd62119714e70def075e8b3. This is a new Lean formalization, not an existing source-project theorem split.

Read-back

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

For every pair of real numbers $a,b$ , if $0\leq a+nb$ for every integer $n$ , where $n$ is regarded as a real number in the expression, then $b=0$ . The quantified integers include zero and all positive and negative integers; in particular the hypothesis at $n=0$ requires $a\geq0$ , and there is no assumption that either $a$ or $b$ is nonzero.

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