OuterRows.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Balanced rows for bounded-multiplicity words

Order each label fibre consecutively, then distribute the resulting enumeration cyclically among the rows. This proves the row decomposition used in the first family of outer-coloring tests, without assuming a balanced decomposition.

def OAI.QuantitativeVanDerWaerden.earlierLabels line 30
Source documentation
Labels occurring before b in a fixed enumeration.
```
def earlierLabels (b : β) : Finset β := by
…
```
def OAI.QuantitativeVanDerWaerden.blockOffset line 35
Source documentation
Starting index of the block belonging to b.
```
def blockOffset (c : β → ℕ) (b : β) : ℕ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.blockOffset_add_le_total line 38
theorem OAI.QuantitativeVanDerWaerden.blockOffset_add_le_of_lt line 48
def OAI.QuantitativeVanDerWaerden.groupedIndex line 69
Source documentation
The position of an element in the concatenation of the label fibres.
```
def groupedIndex (p : Σ b, A b) : Fin (∑ b, Fintype.card (A b)) :=
…
```
theorem OAI.QuantitativeVanDerWaerden.groupedIndex_injective line 75
def OAI.QuantitativeVanDerWaerden.groupedEquiv line 102
Source documentation
A bijective enumeration which keeps each label fibre contiguous.
```
def groupedEquiv : (Σ b, A b) ≃ Fin (∑ b, Fintype.card (A b)) :=
…
```
theorem OAI.QuantitativeVanDerWaerden.groupedEquiv_val line 107
theorem OAI.QuantitativeVanDerWaerden.exists_balanced_rows line 116
Source documentation
Bounded label multiplicities admit a partition into equally populated rows, with at most one occurrence of each label in each row. The cardinal bound is the integer floor, so it applies also to empty rows and words.
```
theorem exists_balanced_rows (f : α → β) (w : ℕ) (hw : 0 < w)
    (hm : ∀ b, Fintype.card {a : α // f a = b} ≤ w) :
    ∃ row : α → Fin w,
      (∀ r, Set.InjOn f {a | row a = r}) ∧
      (∀ r, Fintype.card α / w ≤ Fintype.card {a : α // row a = r}) := by
…
```

theorem OAI.QuantitativeVanDerWaerden.exists_balanced_row_finsets line 159

Source documentation

Explicit finite-set form: the rows partition the positions.

theorem exists_balanced_row_finsets (f : α → β) (w : ℕ) (hw : 0 < w)
    (hm : ∀ b, Fintype.card {a : α // f a = b} ≤ w) :
    ∃ rows : Fin w → Finset α,
      (∀ a, ∃! r, a ∈ rows r) ∧
      (∀ r, Set.InjOn f (rows r)) ∧
      (∀ r, Fintype.card α / w ≤ (rows r).card) := by
…

theorem OAI.QuantitativeVanDerWaerden.exists_light_row_finsets line 180

Source documentation

Light positions in a word admit rows of size at least M / 10, once their number is at least one tenth of k and every label has multiplicity at most w with M * w ≤ k.

theorem exists_light_row_finsets (f : α → β) (M w k : ℕ) (hw : 0 < w)
    (hm : ∀ b, Fintype.card {a : α // f a = b} ≤ w)
    (hwidth : M * w ≤ k) (hlight : k ≤ 10 * Fintype.card α) :
    ∃ rows : Fin w → Finset α,
      (∀ a, ∃! r, a ∈ rows r) ∧
      (∀ r, Set.InjOn f (rows r)) ∧
      (∀ r, M / 10 ≤ (rows r).card) := by
…

theorem OAI.QuantitativeVanDerWaerden.row_balance_aggregate line 195

Source documentation

Balance on each fibre of a row assignment implies balance on all positions. The factor q = 4 is the quarter-balance used in the outer coloring.

theorem row_balance_aggregate (row : α → ι) (p : α → Prop) [DecidablePred p]
    (q : ℕ)
    (hrow : ∀ r,
      (Finset.univ.filter (fun a => row a = r)).card ≤
        q * ((Finset.univ.filter (fun a => row a = r)).filter p).card) :
    Fintype.card α ≤ q * (Finset.univ.filter p).card := by
…

theorem OAI.QuantitativeVanDerWaerden.partition_balance_aggregate line 223

Source documentation

Explicit partition version of row_balance_aggregate. The only partition hypothesis is unique membership; its disjointness and completeness are used.

theorem partition_balance_aggregate (rows : ι → Finset α)
    (hpart : ∀ a, ∃! r, a ∈ rows r) (p : α → Prop) [DecidablePred p]
    (q : ℕ) (hrow : ∀ r, (rows r).card ≤ q * ((rows r).filter p).card) :
    Fintype.card α ≤ q * (Finset.univ.filter p).card := by
…