Prove2Me

Polynomial consequence of two conjugate acyclic cells

Proved
Smooth4Algebra.two_cell_phantom_gap

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

finitesupportlaurentpolynomialslinearalgebra

Let A,C:Z→NA,C:\mathbb Z\to\mathbb N be finitely supported coefficient sequences with A≠0A\ne0, and let gg be a positive integer. Suppose that for every integer mm,

A(m)=C(m−1),C(m)=A(m−(1−2g)).A(m)=C(m-1),\qquad C(m)=A\bigl(m-(1-2g)\bigr).

Then g=1g=1.

Equivalently, writing the sequences as Laurent dimension polynomials, the hypotheses are A=qCA=qC and C=q1−2gAC=q^{1-2g}A. This is the exact algebraic consequence used for two-cell conjugate phantom rows.

Preamble
import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Int.Basic
set_option autoImplicit false
Formal statement
theorem Smooth4Algebra.two_cell_phantom_gap
    (A C : ℤ →₀ ℕ) (hA : A ≠ 0)
    (gap : ℤ) (h_gap : 0 < gap)
    (h_forward : ∀ m : ℤ, A m = C (m - 1))
    (h_conjugate : ∀ m : ℤ, C m = A (m - (1 - 2 * gap))) :
    gap = 1 := 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 pair of finitely supported functions A,C:Z→NA,C:\mathbb Z\to\mathbb N with AA not identically zero, and every integer gg satisfying 0<g0<g, if A(m)=C(m−1)A(m)=C(m-1) and C(m)=A(m−(1−2g))C(m)=A\bigl(m-(1-2g)\bigr) hold for every integer mm, then g=1g=1. Finite support means that each function is zero at all but finitely many integer indices. The values of the functions are natural numbers and may be zero, while all shifts and subtractions in their arguments are integer operations without truncation; the hypotheses range over all positive, zero, and negative indices. The zero function AA and nonpositive values of gg are excluded by the explicit 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