Prove2Me

A nonzero finitely supported sequence has no nonzero period

Proved
Smooth4Algebra.finite_support_shift_rigidity

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

finitesupportlaurentpolynomialslinearalgebra

Let RR be any type with a distinguished zero, and let f:Z→Rf:\mathbb Z\to R have finite support and be nonzero. If an integer kk satisfies

f(m+k)=f(m)for every m∈Z,f(m+k)=f(m)\qquad\text{for every }m\in\mathbb Z,

then k=0k=0.

The result requires no order, addition, multiplication, positivity or cancellation law on the coefficient type. It records the finite-support rigidity used for Laurent dimension polynomials.

Preamble
import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Int.Basic
set_option autoImplicit false
Formal statement
theorem Smooth4Algebra.finite_support_shift_rigidity
    {R : Type*} [Zero R] (f : ℤ →₀ R) (hf : f ≠ 0)
    (k : ℤ) (h_shift : ∀ m : ℤ, f (m + k) = f m) : k = 0 := by sorry
Source
Newly authored from cycle17_phantom_independent.md, section “Arbitrary-matrix two-cell lemma”, equations (1)–(3) and the finite-support sentence following (3); unpublished local research note, no public URL. SHA-256 f9d2af34ac68d1728b6386e624221f43a9eccffe678f50af3103f1b8c1cbbf92.
Read-back

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

For every type RR with a specified element 00, every finitely supported function f:Z→Rf:\mathbb Z\to R that is not identically zero, and every integer kk, if f(m+k)=f(m)f(m+k)=f(m) for every integer mm, then k=0k=0. Finite support means that only finitely many integers have a value different from the specified zero, and no addition, multiplication, or other algebraic structure on RR is assumed. Both positive and negative candidate shifts are included, as is the zero shift. If every element of RR equals its specified zero, the nonzero-function hypothesis cannot be satisfied.

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