Documentation

LeanPool.TwoColoringOneRound.LowerBound.Sanity

Small “sanity checks” intended to validate that the Lean definitions in Defs.lean match the intended combinatorial model.

This file proves, in a fully kernel-checked way, that for n = 5 there is an explicit coloring with monochromatic edge fraction exactly 1/5.

n = 5 #

We split the symbols into {0,1} (“small”) and {2,3,4} (“big”), round to a bit, and apply g. This yields 24 monochromatic edges out of 120, hence monoFraction = 1/5.

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.Sanity.two5 :
Sym 5

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

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

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

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

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

      Equations
      Instances For
        source
        def Distributed2Coloring.LowerBound.Sanity.round5 (a : Sym 5) :
        Bool

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

        Equations
        Instances For
          source
          @[simp]
          theorem Distributed2Coloring.LowerBound.Sanity.round5_eq_true {a : Sym 5} :
          round5 a = true ↔ two5 ≤ a
          source
          @[simp]
          theorem Distributed2Coloring.LowerBound.Sanity.round5_eq_false {a : Sym 5} :
          round5 a = false ↔ a < two5
          source
          @[reducible, inline]
          abbrev Distributed2Coloring.LowerBound.Sanity.f5 :
          Coloring 5

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Distributed2Coloring.LowerBound.Sanity.card_Small5 :
            Fintype.card Small5 = 2
            source
            theorem Distributed2Coloring.LowerBound.Sanity.card_Big5 :
            Fintype.card Big5 = 3
            source
            theorem Distributed2Coloring.LowerBound.Sanity.edgeCount_5 :
            edgeCount 5 = 120
            source
            theorem Distributed2Coloring.LowerBound.Sanity.monoCount_f5 :
            monoCount f5 = 24
            source
            theorem Distributed2Coloring.LowerBound.Sanity.monoFraction_f5 :
            monoFraction f5 = 1 / 5