Warm-up: n = 9 gives > 20%

This file proves a small “warm-up” theorem matching the report:

• the 5-cycle argument gives monoCount f ≥ 605 for every f : Coloring 9;
• a parity lemma shows monoCount f is even, hence monoCount f ≥ 606;
• therefore monoFraction f ≥ 606/3024 = 101/504 > 1/5.

All proofs are kernel-checked (no native_decide).

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.n : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N9.n = 9

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.Sym9 : Type

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.Coloring9 : Type

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.Emb4 : Type

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

Equations

• Distributed2Coloring.LowerBound.N9.Emb4 = (Fin 4 ↪ Distributed2Coloring.LowerBound.N9.Sym9)

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.Emb5 : Type

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

Equations

• Distributed2Coloring.LowerBound.N9.Emb5 = (Fin 5 ↪ Distributed2Coloring.LowerBound.N9.Sym9)

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N9.instFintypeEmb4 : Fintype Emb4

Equations

• Distributed2Coloring.LowerBound.N9.instFintypeEmb4 = inferInstance

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N9.instFintypeEmb5 : Fintype Emb5

Equations

• Distributed2Coloring.LowerBound.N9.instFintypeEmb5 = inferInstance

A cyclic 5-cycle model on Emb5

For t : Emb5 (five distinct symbols) and k : Fin 5, define the directed edge obtained from the ordered quadruple of consecutive symbols starting at position k (cyclically).

We also record the “missing” index in the 5-tuple.

def Distributed2Coloring.LowerBound.N9.idx4 (k : Fin 5) : Fin 4 → Fin 5

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

Equations

• Distributed2Coloring.LowerBound.N9.idx4 k i = k + Fin.castAdd 1 i

def Distributed2Coloring.LowerBound.N9.next (k : Fin 5) : Fin 5

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

Equations

• Distributed2Coloring.LowerBound.N9.next k = k + 1

def Distributed2Coloring.LowerBound.N9.remIndex (k : Fin 5) : Fin 5

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

Equations

• Distributed2Coloring.LowerBound.N9.remIndex k = k + 4

noncomputable def Distributed2Coloring.LowerBound.N9.edgeAt (t : Emb5) (k : Fin 5) : Edge n

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

Equations

• Distributed2Coloring.LowerBound.N9.edgeAt t k = ⟨fun (i : Fin 4) => t (Distributed2Coloring.LowerBound.N9.idx4 k i), ⋯⟩

An odd cycle has a monochromatic edge

We use brute-force case splitting on 5 booleans (32 cases), which is small and kernel-checked.

Double-counting the cycle-edge pairs

We count pairs (t,k) where the k-th edge in the 5-cycle from t is monochromatic. For n = 9, every edge participates in exactly 5 * (9-4) = 25 such pairs, hence

Fintype.card (CycleMonoPairs f) = 25 * monoCount f.

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.CyclePairs : Type

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

Equations

• Distributed2Coloring.LowerBound.N9.CyclePairs = (Distributed2Coloring.LowerBound.N9.Emb5 × Fin 5)

def Distributed2Coloring.LowerBound.N9.CycleMonoPairs (f : Coloring9) : Type

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

Equations

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

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N9.instFintypeCycleMonoPairs (f : Coloring9) : Fintype (CycleMonoPairs f)

Equations

• Distributed2Coloring.LowerBound.N9.instFintypeCycleMonoPairs f = id inferInstance

noncomputable def Distributed2Coloring.LowerBound.N9.edgeEmb (e : Edge n) : Emb4

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

Equations

• Distributed2Coloring.LowerBound.N9.edgeEmb e = { toFun := ↑e, inj' := ⋯ }

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.Extra (e : Edge n) : Set Sym9

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

Equations

• Distributed2Coloring.LowerBound.N9.Extra e = (Set.range ⇑(Distributed2Coloring.LowerBound.N9.edgeEmb e))ᶜ

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N9.instFintypeElemSym9Extra (e : Edge n) : Fintype ↑(Extra e)

Equations

• Distributed2Coloring.LowerBound.N9.instFintypeElemSym9Extra e = id inferInstance

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N9.EdgeExtraK : Type

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

Equations

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

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N9.instFintypeEdgeExtraK : Fintype EdgeExtraK

Equations

• Distributed2Coloring.LowerBound.N9.instFintypeEdgeExtraK = inferInstance

noncomputable def Distributed2Coloring.LowerBound.N9.cyclePairToEdgeExtraK : CyclePairs → EdgeExtraK

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

Equations

• Distributed2Coloring.LowerBound.N9.cyclePairToEdgeExtraK (t, k) = ⟨(Distributed2Coloring.LowerBound.N9.edgeAt t k, t (Distributed2Coloring.LowerBound.N9.remIndex k), k), ⋯⟩

noncomputable def Distributed2Coloring.LowerBound.N9.edgeExtraKToCyclePair : EdgeExtraK → CyclePairs

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

Equations

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

noncomputable def Distributed2Coloring.LowerBound.N9.cyclePairEquiv : CyclePairs ≃ EdgeExtraK

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

Equations

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

Parity lemma: monoCount is even

We show (monoCount f : ZMod 2) = (edgeCount 9 : ZMod 2), hence monoCount f is even since edgeCount 9 = 3024 is even.

theorem Distributed2Coloring.LowerBound.N9.monoFraction_ge_101_504 (f : Coloring9) : 101 / 504 ≤ monoFraction f

theorem Distributed2Coloring.LowerBound.N9.monoFraction_gt_one_fifth (f : Coloring9) : 1 / 5 < monoFraction f