Upper bounds (explicit colorings)

The main formalized result of this project is a lower bound: every coloring has at least 23.879% monochromatic edges when n = 1_000_000.

This file provides small explicit upper bounds (i.e. constructions of colorings with relatively few monochromatic edges), to complement the lower bounds.

The coloring used here is the simple rounding-based local rule from the report:

• round each symbol a : Fin n to a bit r(a) depending on whether a < n/2;
• apply a fixed local rule g to the rounded bits.

n = 9

We use the rounding threshold 4, so Small = {0,1,2,3} and Big = {4,5,6,7,8}. The resulting coloring has monochromatic fraction exactly 13/63 ≈ 20.63%.

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.n : ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.n = 9

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.Sym9 : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.Sym9 = Distributed2Coloring.LowerBound.Sym Distributed2Coloring.LowerBound.UpperBound.N9.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.Coloring9 : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.Coloring9 = Distributed2Coloring.LowerBound.Coloring Distributed2Coloring.LowerBound.UpperBound.N9.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.two9 : Sym9

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.two9 = ⟨4, Distributed2Coloring.LowerBound.UpperBound.N9.two9._proof_1⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.Small9 : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.Small9 = ↑(Set.Iio Distributed2Coloring.LowerBound.UpperBound.N9.two9)

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.Big9 : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.Big9 = ↑(Set.Ici Distributed2Coloring.LowerBound.UpperBound.N9.two9)

theorem Distributed2Coloring.LowerBound.UpperBound.N9.card_Small9 : Fintype.card Small9 = 4

theorem Distributed2Coloring.LowerBound.UpperBound.N9.card_Big9 : Fintype.card Big9 = 5

def Distributed2Coloring.LowerBound.UpperBound.N9.round9 (a : Sym9) : Bool

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.N9.round9 a = decide (Distributed2Coloring.LowerBound.UpperBound.N9.two9 ≤ a)

@[simp]

theorem Distributed2Coloring.LowerBound.UpperBound.N9.round9_eq_true {a : Sym9} : round9 a = true ↔ two9 ≤ a

@[simp]

theorem Distributed2Coloring.LowerBound.UpperBound.N9.round9_eq_false {a : Sym9} : round9 a = false ↔ a < two9

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.N9.f9 : Coloring9

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Distributed2Coloring.LowerBound.UpperBound.N9.monoFraction_f9_le_13_63 : monoFraction f9 ≤ 13 / 63

theorem Distributed2Coloring.LowerBound.UpperBound.N9.exists_coloring_monoFraction_le_13_63 : ∃ (f : Coloring9), monoFraction f ≤ 13 / 63

A clean universal upper bound (≤ 1/4 for all n ≥ 5)

We give an explicit coloring (the same rounding-based rule as above) and show its monochromatic-edge fraction is at most 1/4 for every n ≥ 5.

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.Universal.two (n : ℕ) (hn : 5 ≤ n) : Sym n

The rounding threshold ⌊n/2⌋, viewed as an element of Fin n.

Equations

• Distributed2Coloring.LowerBound.UpperBound.Universal.two n hn = ⟨n / 2, ⋯⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.Universal.Small (n : ℕ) (hn : 5 ≤ n) : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.Universal.Small n hn = Distributed2Coloring.LowerBound.EdgePatterns.Small (Distributed2Coloring.LowerBound.UpperBound.Universal.two n hn)

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.Universal.Big (n : ℕ) (hn : 5 ≤ n) : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.Universal.Big n hn = Distributed2Coloring.LowerBound.EdgePatterns.Big (Distributed2Coloring.LowerBound.UpperBound.Universal.two n hn)

def Distributed2Coloring.LowerBound.UpperBound.Universal.round (n : ℕ) (hn : 5 ≤ n) (a : Sym n) : Bool

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.UpperBound.Universal.round n hn a = decide (Distributed2Coloring.LowerBound.UpperBound.Universal.two n hn ≤ a)

@[simp]

theorem Distributed2Coloring.LowerBound.UpperBound.Universal.round_eq_true {n : ℕ} (hn : 5 ≤ n) {a : Sym n} : round n hn a = true ↔ two n hn ≤ a

@[simp]

theorem Distributed2Coloring.LowerBound.UpperBound.Universal.round_eq_false {n : ℕ} (hn : 5 ≤ n) {a : Sym n} : round n hn a = false ↔ a < two n hn

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.UpperBound.Universal.f (n : ℕ) (hn : 5 ≤ n) : Coloring n

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Distributed2Coloring.LowerBound.UpperBound.Universal.monoFraction_f_le_one_quarter {n : ℕ} (hn : 5 ≤ n) : monoFraction (f n hn) ≤ 1 / 4

The rounding-based coloring has monochromatic fraction at most 1/4 for every n ≥ 5.

theorem Distributed2Coloring.LowerBound.UpperBound.Universal.exists_coloring_monoFraction_le_one_quarter {n : ℕ} (hn : 5 ≤ n) : ∃ (f : Coloring n), monoFraction f ≤ 1 / 4