Documentation

LeanPool.TwoColoringOneRound.LowerBound.EdgePatterns

Reusable lemmas for counting edges with coordinate-wise constraints relative to a threshold two.

These are used in auxiliary “sanity check” and “upper bound” files to avoid repeating large case-bashy equivalence proofs.

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.EdgePatterns.Small {n : ℕ} (two : Sym n) :
Type

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Distributed2Coloring.LowerBound.EdgePatterns.Big {n : ℕ} (two : Sym n) :
    Type

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

    Equations
    Instances For
      source
      def Distributed2Coloring.LowerBound.EdgePatterns.Pat0000 {n : ℕ} (two : Sym n) (e : Edge n) :
      Prop

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

      Equations
      Instances For
        source
        def Distributed2Coloring.LowerBound.EdgePatterns.Pat1111 {n : ℕ} (two : Sym n) (e : Edge n) :
        Prop

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

        Equations
        Instances For
          source
          def Distributed2Coloring.LowerBound.EdgePatterns.Pat1001 {n : ℕ} (two : Sym n) (e : Edge n) :
          Prop

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

          Equations
          Instances For
            source
            def Distributed2Coloring.LowerBound.EdgePatterns.Pat0110 {n : ℕ} (two : Sym n) (e : Edge n) :
            Prop

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

            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Distributed2Coloring.LowerBound.EdgePatterns.instDecidablePredEdgePat0000 {n : ℕ} (two : Sym n) :
              DecidablePred (Pat0000 two)
              Equations
              source
              @[implicit_reducible]
              instance Distributed2Coloring.LowerBound.EdgePatterns.instDecidablePredEdgePat1111 {n : ℕ} (two : Sym n) :
              DecidablePred (Pat1111 two)
              Equations
              source
              @[implicit_reducible]
              instance Distributed2Coloring.LowerBound.EdgePatterns.instDecidablePredEdgePat1001 {n : ℕ} (two : Sym n) :
              DecidablePred (Pat1001 two)
              Equations
              source
              @[implicit_reducible]
              instance Distributed2Coloring.LowerBound.EdgePatterns.instDecidablePredEdgePat0110 {n : ℕ} (two : Sym n) :
              DecidablePred (Pat0110 two)
              Equations
              source
              theorem Distributed2Coloring.LowerBound.EdgePatterns.card_pat0000 {n : ℕ} (two : Sym n) :
              Fintype.card { e : Edge n // Pat0000 two e } = (Fintype.card (Small two)).descFactorial 4
              source
              theorem Distributed2Coloring.LowerBound.EdgePatterns.card_pat1111 {n : ℕ} (two : Sym n) :
              Fintype.card { e : Edge n // Pat1111 two e } = (Fintype.card (Big two)).descFactorial 4
              source
              theorem Distributed2Coloring.LowerBound.EdgePatterns.card_pat1001 {n : ℕ} (two : Sym n) :
              Fintype.card { e : Edge n // Pat1001 two e } = (Fintype.card (Big two)).descFactorial 2 * (Fintype.card (Small two)).descFactorial 2
              source
              theorem Distributed2Coloring.LowerBound.EdgePatterns.card_pat0110 {n : ℕ} (two : Sym n) :
              Fintype.card { e : Edge n // Pat0110 two e } = (Fintype.card (Big two)).descFactorial 2 * (Fintype.card (Small two)).descFactorial 2