SelectorDelay.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Delaying one moved coordinate by one color

When a moved coordinate has final color i, replacing it by i.succ removes exactly that coordinate from the prefixSet at cut i. Every other cut stays unchanged, and total movement decreases by one.

def OAI.TalagrandThreshold.Selector.delayColor line 23
Source documentation
Raise the final color of x to the color immediately after cut i.
```
def delayColor (z : Coloring α s) (x : α) (i : Fin s) : Coloring α s :=
…
```
Mentions: OAI.TalagrandThreshold.Coloring
theorem OAI.TalagrandThreshold.Selector.delayColor_apply_self line 27
theorem OAI.TalagrandThreshold.Selector.delayColor_apply_of_ne line 32
theorem OAI.TalagrandThreshold.Selector.earlier_delayColor line 37
theorem OAI.TalagrandThreshold.Selector.changes_delayColor_subset line 50
Source documentation
Delaying a coordinate cannot introduce a newly moved vertex.
```
theorem changes_delayColor_subset (a z : Coloring α s) (x : α) (i : Fin s)
    (hx : (z x).val = i.val) : changes a (delayColor z x i) ⊆ changes a z := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.changes, OAI.TalagrandThreshold.Selector.delayColor
theorem OAI.TalagrandThreshold.Selector.prefix_delayColor_self line 65
theorem OAI.TalagrandThreshold.Selector.prefix_delayColor_of_ne line 89
theorem OAI.TalagrandThreshold.Selector.crossings_delayColor_self line 104
Source documentation
Exactly one crossing disappears at the affected cut.
```
theorem crossings_delayColor_self (a z : Coloring α s) (x : α) (i : Fin s)
    (hx : (z x).val = i.val) (hmove : (z x).val < (a x).val) :
    crossings a (delayColor z x i) i + 1 = crossings a z i := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.crossings, OAI.TalagrandThreshold.Selector.delayColor
theorem OAI.TalagrandThreshold.Selector.crossings_delayColor_of_ne line 113
theorem OAI.TalagrandThreshold.Selector.movement_delayColor_add_one line 120
Source documentation
The delay removes precisely one unit of total movement.
```
theorem movement_delayColor_add_one (a z : Coloring α s) (x : α) (i : Fin s)
    (hx : (z x).val = i.val) (hmove : (z x).val < (a x).val) :
    movement a (delayColor z x i) + 1 = movement a z := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.movement, OAI.TalagrandThreshold.Selector.delayColor