Distributed2Coloring: Main results

This file collects the public-facing theorems connecting:

• the certified finite lower bound at n = 1_000_000, and
• one-round ClassicalAlgorithms on the directed cycle.

We also package these bounds as statements about an infimum p⋆ over all measurable local rules.

noncomputable def Distributed2Coloring.ClassicalAlgorithm.pStar : ENNReal

The optimal monochromatic-edge probability over all one-round ClassicalAlgorithms.

This corresponds to the quantity p⋆ := inf_f p(f) in theory/report/manuscript.tex, where the infimum ranges over all measurable local rules.

Equations

• Distributed2Coloring.ClassicalAlgorithm.pStar = sInf (Set.range Distributed2Coloring.ClassicalAlgorithm.p)

theorem Distributed2Coloring.ClassicalAlgorithm.le_pStar_of_forall_le {c : ENNReal} (hc : ∀ (alg : ClassicalAlgorithm), c ≤ alg.p) : c ≤ pStar

If c is a lower bound for ClassicalAlgorithm.p for every algorithm, then c ≤ pStar.

theorem Distributed2Coloring.ClassicalAlgorithm.pStar_le_of_exists_le {c : ENNReal} (hc : ∃ (alg : ClassicalAlgorithm), alg.p ≤ c) : pStar ≤ c

If there exists an algorithm achieving p ≤ c, then pStar ≤ c.

In particular, any explicit construction gives an upper bound on pStar.

Numerical bounds (as in the manuscript)

The bridge step is Distributed2Coloring.p_ge_23879 from Distributed2Coloring/Reduction.lean.

theorem Distributed2Coloring.pStar_ge_23879 : ENNReal.ofReal (23879 / 100000) ≤ ClassicalAlgorithm.pStar

Every one-round algorithm has monochromatic-edge probability at least 0.23879.

theorem Distributed2Coloring.pStar_le_24118 : ClassicalAlgorithm.pStar ≤ ENNReal.ofReal (24118 / 100000)

An explicit one-round algorithm achieves monochromatic-edge probability at most 0.24118.

theorem Distributed2Coloring.pStar_lt_24118 : ClassicalAlgorithm.pStar < ENNReal.ofReal (24118 / 100000)