Marked words, permutation words and the gluing inequalities

This file is the pure word combinatorics behind the Erdős–Sós theorem; no graph appears in it.

A marked word is one whose last letter satisfies a predicate N. For families A, B, C of letter sets with C ⊆ A and A R → B X → C (R ∪ X) for disjoint R, X, the exact counting inequality marked_word_gluing_count bounds the marked cuts qualifying for A plus those qualifying for B by the ambient allowed cuts plus those qualifying for C. It is proved by rotating the first A-and-not-C prefix of a cut past the rest of the prefix, an injective operation into the allowed cuts that do not qualify for B.

permutationWords l is the finite set of permutations of a repetition-free word l, of cardinality l.length !; the marked cuts of l are counted by its marked letters (marked_prefix_card), and the allowed cuts are the marked ones plus one empty cut per word (allowedWordCuts_card).

A full word b :: q has a distinguished first letter b (the root image) and a cut in the remaining word q. fullWordCount counts the qualifying cuts of all permutation words of a fixed word l₀; fullWordCount_eq_sum decomposes it by root, full_word_gluing_count lifts the gluing inequality to full words, and full_word_transfer_count bounds one family by another through the cut-reversal involution reverseCutPair, losing at most one first cut per word.

Reversible prefix-block rotation for finite marked-word counting.

def Erdos548.MarkedEnd {α : Type u_1} (N : α → Prop) (l : List α) : Prop

A nonempty marked last letter.

Equations

• Erdos548.MarkedEnd N l = ∃ (a : α), l.getLast? = some a ∧ N a

theorem Erdos548.markedEnd_not_nil {α : Type u_1} {N : α → Prop} {l : List α} (h : MarkedEnd N l) : l ≠ []

theorem Erdos548.markedEnd_append_right {α : Type u_1} {N : α → Prop} {r x : List α} (h : MarkedEnd N (r ++ x)) (hx : x ≠ []) : MarkedEnd N x

def Erdos548.FirstPrefix {α : Type u_1} (P : List α → Prop) (r : List α) : Prop

The displayed word is the first qualifying prefix of any extension.

Equations

• Erdos548.FirstPrefix P r = (P r ∧ ∀ j < r.length, ¬P (List.take j r))

theorem Erdos548.firstPrefix_unique {α : Type u_1} {P : List α → Prop} {r y r' y' : List α} (hr : FirstPrefix P r) (hr' : FirstPrefix P r') (he : r ++ y = r' ++ y') : r = r' ∧ y = y'

theorem Erdos548.firstPrefix_rotation_injective {α : Type u_1} {P : List α → Prop} {r x y r' x' y' : List α} (hr : FirstPrefix P r) (hr' : FirstPrefix P r') (he : (x ++ (r ++ y), x.length) = (x' ++ (r' ++ y'), x'.length)) : (r ++ x ++ y, r.length + x.length) = (r' ++ x' ++ y', r'.length + x'.length)

theorem Erdos548.marked_prefix_rotation_exists {α : Type u_1} [DecidableEq α] (N : α → Prop) (A B C : Finset α → Prop) (hglue : ∀ (R X : Finset α), Disjoint R X → A R → B X → C (R ∪ X)) (l : List α) (hl : l.Nodup) (k : ℕ) (hk : k ≤ l.length) (hm : MarkedEnd N (List.take k l)) (hA : A (List.take k l).toFinset) (hC : ¬C (List.take k l).toFinset) : ∃ (r : List α) (x : List α) (y : List α), l = r ++ x ++ y ∧ k = r.length + x.length ∧ FirstPrefix (fun (q : List α) => MarkedEnd N q ∧ A q.toFinset ∧ ¬C q.toFinset) r ∧ (x = [] ∨ MarkedEnd N x) ∧ ¬B x.toFinset

Cut at the first qualifying marked prefix and rotate it past the rest of an input prefix. Its new prefix is a disjoint difference and hence cannot belong to the second family.

def Erdos548.PrefixRotation {α : Type u_1} (P : List α → Prop) (u v : List α × ℕ) : Prop

The relation records the reversible block rotation, without choosing a particular implementation of the first-prefix search.

Equations

• Erdos548.PrefixRotation P u v = ∃ (r : List α) (x : List α) (y : List α), u = (r ++ x ++ y, r.length + x.length) ∧ v = (x ++ (r ++ y), x.length) ∧ Erdos548.FirstPrefix P r

theorem Erdos548.prefixRotation_left_unique {α : Type u_1} {P : List α → Prop} {u u' v : List α × ℕ} (h : PrefixRotation P u v) (h' : PrefixRotation P u' v) : u = u'

noncomputable def Erdos548.allowedWordCuts {α : Type u_1} (W : Finset (List α)) (m : ℕ) (N : α → Prop) : Finset (List α × ℕ)

All cuts (l, k) of words l ∈ W with k ≤ m, where the cut is either empty or ends at a marked letter. This is the ambient family the gluing inequality is counted against.

Equations

• Erdos548.allowedWordCuts W m N = {p ∈ W ×ˢ Finset.range (m + 1) | p.2 = 0 ∨ Erdos548.MarkedEnd N (List.take p.2 p.1)}

noncomputable def Erdos548.goodWordCuts {α : Type u_1} [DecidableEq α] (W : Finset (List α)) (m : ℕ) (N : α → Prop) (A : Finset α → Prop) : Finset (List α × ℕ)

Cuts (l, k) of words l ∈ W with k ≤ m whose prefix ends at a marked letter and whose letter set satisfies A.

Equations

• Erdos548.goodWordCuts W m N A = {p ∈ W ×ˢ Finset.range (m + 1) | Erdos548.MarkedEnd N (List.take p.2 p.1) ∧ A (List.take p.2 p.1).toFinset}

theorem Erdos548.goodWordCuts_subset_allowed {α : Type u_1} [DecidableEq α] (W : Finset (List α)) (m : ℕ) (N : α → Prop) (A : Finset α → Prop) : goodWordCuts W m N A ⊆ allowedWordCuts W m N

theorem Erdos548.goodWordCuts_mono {α : Type u_1} [DecidableEq α] (W : Finset (List α)) (m : ℕ) (N : α → Prop) (A C : Finset α → Prop) (hCA : ∀ (X : Finset α), C X → A X) : goodWordCuts W m N C ⊆ goodWordCuts W m N A

theorem Erdos548.marked_word_gluing_count {α : Type u_1} [DecidableEq α] (W : Finset (List α)) (m : ℕ) (N : α → Prop) (A B C : Finset α → Prop) (hlen : ∀ l ∈ W, l.length = m) (hnodup : ∀ l ∈ W, l.Nodup) (hperm : ∀ l ∈ W, ∀ (l' : List α), l'.Perm l → l' ∈ W) (hCA : ∀ (X : Finset α), C X → A X) (hglue : ∀ (R X : Finset α), Disjoint R X → A R → B X → C (R ∪ X)) : (goodWordCuts W m N A).card + (goodWordCuts W m N B).card ≤ (allowedWordCuts W m N).card + (goodWordCuts W m N C).card

The exact finite marked-word gluing inequality. The ambient word family must be closed under permutation; every word is repetition-free.

Exact cardinalities of permutation words and marked prefixes.

noncomputable def Erdos548.permutationWords {α : Type u_1} [DecidableEq α] (l : List α) : Finset (List α)

The finite set of all words that are permutations of l.

Equations

• Erdos548.permutationWords l = l.permutations.toFinset

theorem Erdos548.mem_permutationWords {α : Type u_1} [DecidableEq α] (l q : List α) : q ∈ permutationWords l ↔ q.Perm l

theorem Erdos548.permutationWords_card {α : Type u_1} [DecidableEq α] (l : List α) (hl : l.Nodup) : (permutationWords l).card = l.length.factorial

theorem Erdos548.markedEnd_take_succ {α : Type u_1} (N : α → Prop) (l : List α) (i : ℕ) (hi : i < l.length) : MarkedEnd N (List.take (i + 1) l) ↔ N l[i]

theorem Erdos548.markedEnd_take_pos {α : Type u_1} {N : α → Prop} {l : List α} {k : ℕ} (h : MarkedEnd N (List.take k l)) : 0 < k

theorem Erdos548.markedEnd_take_iff {α : Type u_1} (N : α → Prop) (l : List α) (k : ℕ) (hk : k ≤ l.length) : MarkedEnd N (List.take k l) ↔ ∃ (h : 0 < k), N l[k - 1]

theorem Erdos548.marked_prefix_card {α : Type u_1} [DecidableEq α] (N : α → Prop) (l : List α) (hl : l.Nodup) : {k ∈ Finset.range (l.length + 1) | MarkedEnd N (List.take k l)}.card = (Finset.filter N l.toFinset).card

theorem Erdos548.goodWordCuts_true_card {α : Type u_1} [DecidableEq α] (W : Finset (List α)) (m : ℕ) (N : α → Prop) (hlen : ∀ l ∈ W, l.length = m) (hnodup : ∀ l ∈ W, l.Nodup) : (goodWordCuts W m N fun (x : Finset α) => True).card = ∑ l ∈ W, (Finset.filter N l.toFinset).card

theorem Erdos548.allowedWordCuts_card {α : Type u_1} [DecidableEq α] (W : Finset (List α)) (m : ℕ) (N : α → Prop) : (allowedWordCuts W m N).card = W.card + (goodWordCuts W m N fun (x : Finset α) => True).card

Full permutation words, grouped by their first letter, and the cut-reversal involution.

def Erdos548.FullWordQualifies {α : Type u_1} [DecidableEq α] (N : α → α → Prop) (A : α → Finset α → Prop) (l : List α) (k : ℕ) : Prop

The first letter is a distinguished root, and a marked cut is taken in the remaining word. The family is allowed to depend on that root.

Equations

• Erdos548.FullWordQualifies N A l k = ∃ (b : α) (q : List α), l = b :: q ∧ Erdos548.MarkedEnd (N b) (List.take k q) ∧ A b (List.take k q).toFinset

theorem Erdos548.fullWordQualifies_cons {α : Type u_1} [DecidableEq α] (N : α → α → Prop) (A : α → Finset α → Prop) (b : α) (q : List α) (k : ℕ) : FullWordQualifies N A (b :: q) k ↔ MarkedEnd (N b) (List.take k q) ∧ A b (List.take k q).toFinset

noncomputable def Erdos548.fullGoodWordCuts {α : Type u_1} [DecidableEq α] (l₀ : List α) (N : α → α → Prop) (A : α → Finset α → Prop) : Finset (List α × ℕ)

Full permutation words of l₀ with a cut position, restricted to the qualifying ones.

Equations

• Erdos548.fullGoodWordCuts l₀ N A = {p ∈ Erdos548.permutationWords l₀ ×ˢ Finset.range l₀.length | Erdos548.FullWordQualifies N A p.1 p.2}

noncomputable def Erdos548.fullWordCount {α : Type u_1} [DecidableEq α] (l₀ : List α) (N : α → α → Prop) (A : α → Finset α → Prop) : ℕ

The number of qualifying cut permutation words of l₀.

Equations

• Erdos548.fullWordCount l₀ N A = (Erdos548.fullGoodWordCuts l₀ N A).card

theorem Erdos548.mem_fullGoodWordCuts {α : Type u_1} [DecidableEq α] (l₀ : List α) (N : α → α → Prop) (A : α → Finset α → Prop) (l : List α) (k : ℕ) : (l, k) ∈ fullGoodWordCuts l₀ N A ↔ l.Perm l₀ ∧ k < l₀.length ∧ FullWordQualifies N A l k

theorem Erdos548.fullWordCount_eq_sum {α : Type u_1} [DecidableEq α] (l₀ : List α) (N : α → α → Prop) (A : α → Finset α → Prop) : fullWordCount l₀ N A = ∑ b ∈ l₀.toFinset, (goodWordCuts (permutationWords (l₀.erase b)) (l₀.length - 1) (N b) (A b)).card

theorem Erdos548.sum_outer_words_card {α : Type u_1} [DecidableEq α] (l₀ : List α) (hl : l₀.Nodup) (hne : l₀ ≠ []) : ∑ b ∈ l₀.toFinset, (permutationWords (l₀.erase b)).card = (permutationWords l₀).card

Sum of the numbers of outer words: exactly one full word for every choice of its head and its outer permutation.

theorem Erdos548.full_word_gluing_count {α : Type u_1} [DecidableEq α] (l₀ : List α) (hl : l₀.Nodup) (hne : l₀ ≠ []) (N : α → α → Prop) (A B C : α → Finset α → Prop) (hCA : ∀ (b : α) (X : Finset α), C b X → A b X) (hglue : ∀ (b : α) (R X : Finset α), Disjoint R X → A b R → B b X → C b (R ∪ X)) : fullWordCount l₀ N A + fullWordCount l₀ N B ≤ (fullWordCount l₀ N fun (x : α) (x_1 : Finset α) => True) + (permutationWords l₀).card + fullWordCount l₀ N C

Root-dependent gluing, summed over ALL full permutation words.

def Erdos548.reverseWordAt {α : Type u_1} (l : List α) (c : ℕ) : List α

Reverse the first c letters of a word and, separately, the remaining letters.

Equations

• Erdos548.reverseWordAt l c = (List.take c l).reverse ++ (List.drop c l).reverse

theorem Erdos548.reverseWordAt_perm {α : Type u_1} (l : List α) (c : ℕ) : (reverseWordAt l c).Perm l

theorem Erdos548.reverseWordAt_involutive {α : Type u_1} (l : List α) (c : ℕ) : reverseWordAt (reverseWordAt l c) c = l

def Erdos548.reverseCutPair {α : Type u_1} (p : List α × ℕ) : List α × ℕ

The cut-reversal involution on words with a cut position.

Equations

• Erdos548.reverseCutPair p = (Erdos548.reverseWordAt p.1 (p.2 + 1), p.2)

theorem Erdos548.reverseCutPair_involutive {α : Type u_1} : Function.Involutive reverseCutPair

theorem Erdos548.reverseCutPair_injective {α : Type u_1} : Function.Injective reverseCutPair

theorem Erdos548.reverseWordAt_decomposition {α : Type u_1} (b w : α) (p q : List α) : reverseWordAt (b :: (p ++ w :: q)) (p.length + 2) = w :: (p.reverse ++ b :: q.reverse)

theorem Erdos548.full_word_transfer_count {α : Type u_1} [DecidableEq α] (l₀ : List α) (N N' : α → α → Prop) (A B : α → Finset α → Prop) (hstep : ∀ (l : List α), l.Perm l₀ → ∀ k < l₀.length, FullWordQualifies N A l k → ∀ j < k, FullWordQualifies N A l j → FullWordQualifies N' B (reverseWordAt l (k + 1)) k) : fullWordCount l₀ N A ≤ fullWordCount l₀ N' B + (permutationWords l₀).card

A first-state loss of at most one per full word, followed by the cut reversal involution. This is purely finite counting.