Reduction: local rules → finite coloring bound

This file formalizes the bridge in theory/report/manuscript.tex, Section "A reduction to an extremal digraph problem":

• a measurable ClassicalAlgorithm induces (from i.i.d. seeds) a random Coloring n of the finite digraph G_n from Distributed2Coloring.LowerBound.Defs,
• the local monochromatic-edge probability ClassicalAlgorithm.p is the expectation of the monochromatic-edge fraction monoFraction of that induced coloring,
• hence any certified lower bound on monoFraction transfers to a lower bound on p.

We use the already-formalized certified bound at n = 1_000_000 to conclude 0.23879 ≤ p for all ClassicalAlgorithms (we use ≤ rather than < throughout), and the already-formalized explicit construction to conclude p ≤ 0.24118 for some ClassicalAlgorithm.

@[reducible, inline]

abbrev Distributed2Coloring.Reduction.n1000000 : ℕ

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

Equations

• Distributed2Coloring.Reduction.n1000000 = Distributed2Coloring.LowerBound.N1000000.n

def Distributed2Coloring.Reduction.colorToBool : Color → Bool

Convert Fin 2 colors to Bool.

Equations

• Distributed2Coloring.Reduction.colorToBool = ⇑finTwoEquiv

theorem Distributed2Coloring.Reduction.colorToBool_injective : Function.Injective colorToBool

def Distributed2Coloring.Reduction.coloringOfSeeds {n : ℕ} (alg : ClassicalAlgorithm) (S : Samples n) : LowerBound.Coloring n

The deterministic LowerBound.Coloring n induced by a seed assignment S : Fin n → [0,1].

Equations

• Distributed2Coloring.Reduction.coloringOfSeeds alg S v = Distributed2Coloring.Reduction.colorToBool (alg.f (S v.a, S v.b, S v.c))

def Distributed2Coloring.Reduction.pick4 {n : ℕ} (emb : Fin 4 ↪ Fin n) : Samples n → Samples 4

Pick out the 4 coordinates of a seed assignment indexed by an embedding.

Equations

• Distributed2Coloring.Reduction.pick4 emb S i = S (emb i)

theorem Distributed2Coloring.Reduction.measurable_pick4 {n : ℕ} (emb : Fin 4 ↪ Fin n) : Measurable (pick4 emb)

theorem Distributed2Coloring.Reduction.measurePreserving_pick4 {n : ℕ} (emb : Fin 4 ↪ Fin n) : MeasureTheory.MeasurePreserving (pick4 emb) MeasureTheory.volume MeasureTheory.volume

def Distributed2Coloring.Reduction.edgeEvent (alg : ClassicalAlgorithm) {n : ℕ} (e : LowerBound.Edge n) : Set (Samples n)

The pEvent pulled back along the coordinates of an injective 4-tuple.

Equations

• Distributed2Coloring.Reduction.edgeEvent alg e = Distributed2Coloring.Reduction.pick4 { toFun := ↑e, inj' := ⋯ } ⁻¹' alg.pEvent

theorem Distributed2Coloring.Reduction.measurableSet_edgeEvent (alg : ClassicalAlgorithm) {n : ℕ} (e : LowerBound.Edge n) : MeasurableSet (edgeEvent alg e)

theorem Distributed2Coloring.Reduction.edgeEvent_measure_eq_p (alg : ClassicalAlgorithm) {n : ℕ} (e : LowerBound.Edge n) : MeasureTheory.volume (edgeEvent alg e) = alg.p

theorem Distributed2Coloring.Reduction.edgeMonochromatic_iff {n : ℕ} (alg : ClassicalAlgorithm) (S : Samples n) (e : LowerBound.Edge n) : LowerBound.Edge.monochromatic (coloringOfSeeds alg S) e ↔ S ∈ edgeEvent alg e

Instead of directly identifying p alg with the expectation of the fraction monoFraction (coloringOfSeeds alg S), we work with the (Nat-valued) count monoCount.

This avoids casting/division lemmas for ENNReal.ofReal that can lead to kernel-recursion issues when n is very large (here n = 1_000_000).

theorem Distributed2Coloring.Reduction.monoCount_eq_sum_edgeEvent_indicator {n : ℕ} (alg : ClassicalAlgorithm) (S : Samples n) : ↑(LowerBound.monoCount (coloringOfSeeds alg S)) = ∑ e : LowerBound.Edge n, (edgeEvent alg e).indicator (fun (x : Samples n) => 1) S

theorem Distributed2Coloring.Reduction.lintegral_monoCount_eq_edgeCount_mul_p {n : ℕ} (_hn : 4 ≤ n) (alg : ClassicalAlgorithm) : ∫⁻ (S : Samples n), ↑(LowerBound.monoCount (coloringOfSeeds alg S)) = ↑(LowerBound.edgeCount n) * alg.p

theorem Distributed2Coloring.Reduction.p_ge_23879 (alg : ClassicalAlgorithm) : ENNReal.ofReal (23879 / 100000) ≤ alg.p

theorem Distributed2Coloring.Reduction.exists_algorithm_p_le_24118 : ∃ (alg : ClassicalAlgorithm), alg.p ≤ ENNReal.ofReal (24118 / 100000)

theorem Distributed2Coloring.p_ge_23879 (alg : ClassicalAlgorithm) : ENNReal.ofReal (23879 / 100000) ≤ alg.p

Certified lower bound: every one-round ClassicalAlgorithm satisfies 0.23879 ≤ p.

theorem Distributed2Coloring.exists_algorithm_p_le_24118 : ∃ (alg : ClassicalAlgorithm), alg.p ≤ ENNReal.ofReal (24118 / 100000)

A one-round ClassicalAlgorithm exists with p ≤ 0.24118.