Even alternating-deletion count for a noninjective label sequence
ProvedProofsInTheBook.Chapter39.labelSeq_deletionParity_of_not_injective_of_noOppositeauxiliary-lemmabook-chapter-43combinatoricsgraph-theorylean4proofs-from-the-book
Write for (empty when ). A signed label on is a pair with and ; negation reverses its sign. For a sequence , write when there exists a strictly increasing such that , and define by reversing all these signs. Here denotes the positive sign for even . These predicates concern the label set ordered by index, not the input order. Let and . Assume is not injective and for all . Let be the sequence obtained by deleting position and retaining the order of the other entries. Then
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.labelSeq_deletionParity_of_not_injective_of_noOpposite {k m : ℕ}
{L : Fin (k + 1) → SignedLabel m} (hnot : ¬ Function.Injective L)
(_hno : NoOppositeLabelSeq L) :
Even (labelSeqAltPosDeletionSet L).card ∧
¬ IsAltPosLabelSeq L ∧ ¬ IsAltNegLabelSeq L := by sorrySource
Original formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter39Tucker.lean#L2024. 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).