Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000Main

LeanPool.TwoColoringOneRound.LowerBound.N1000000Main #

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000.n :
ℕ

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Distributed2Coloring.LowerBound.N1000000.Q :
    Type

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

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Distributed2Coloring.LowerBound.N1000000.Block :
      Type

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

      Equations
      Instances For
        source
        theorem Distributed2Coloring.LowerBound.N1000000.monoFraction_ge_23879 (f : Coloring n) :
        23879 / 100000 ≤ monoFraction f

        Main deliverable (kernel-checked):

        For n = 1,000,000, every Coloring n has monochromatic-edge fraction at least 23879/100000.

        Definitions:

        • Coloring / monoFraction / Edge.monochromatic are in Distributed2Coloring.LowerBound.Defs.
        • The proof combines a precomputed exact rational dual certificate with weak duality, and shows the required PSD constraints for xFromColoring f via a compression/congruence argument.