Prove2Me

Parity of alternating deletions in a sign sequence

Proved
ProofsInTheBook.Chapter39.signSeqDeletionParity

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

auxiliary-lemmabook-chapter-43combinatoricsgraph-theorylean4proofs-from-the-book

Write [a]={0,…,a−1}[a]=\{0,\ldots,a-1\} for a∈Na\in\mathbb N (empty when a=0a=0). Let k∈Nk\in\mathbb N and let s:[k+1]→{+1,−1}s:[k+1]\to\{+1,-1\}. Put ej=(−1)je_j=(-1)^j and define D(s)={i∈[k+1]:(∀j<i, sj=ej)∧(∀j>i, sj=−ej)}D(s)=\{i\in[k+1]:(\forall j<i,\ s_j=e_j)\land(\forall j>i,\ s_j=-e_j)\}. Then

∣D(s)∣ is odd⟺(∀j∈[k+1], sj=ej) ∨ (∀j∈[k+1], sj=−ej).|D(s)|\text{ is odd}\quad\Longleftrightarrow\quad(\forall j\in[k+1],\ s_j=e_j)\ \lor\ (\forall j\in[k+1],\ s_j=-e_j).
Preamble
import Init
import Mathlib
import Mathlib.Data.Fin.Tuple.Sort
import Definitions.Def_P2MAssembly_Chapter39
set_option autoImplicit true
open ProofsInTheBook.Chapter39
open SignedPermutation
Formal statement
theorem ProofsInTheBook.Chapter39.signSeqDeletionParity {k : ℕ} (s : Fin (k + 1) → Bool) :
    Odd (signSeqDoorSet s).card ↔ signSeqAltPos s ∨ signSeqAltNeg s := by sorry
Source
Original formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter39Tucker.lean#L915. Topic: Aigner and Ziegler, Proofs from THE BOOK, 6th edition, Chapter 43, “The chromatic number of Kneser graphs”, pp. 301–305 (https://doi.org/10.1007/978-3-662-57265-8_43).

View graph