Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000PairTransitivity

LeanPool.TwoColoringOneRound.LowerBound.N1000000PairTransitivity #

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

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

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

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

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

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

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

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

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

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            noncomputable instance Distributed2Coloring.LowerBound.N1000000PairTransitivity.instFintypeG :
            Fintype G
            Equations
            source
            @[reducible, inline]
            abbrev Distributed2Coloring.LowerBound.N1000000PairTransitivity.i0 :
            Fin 3

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

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Distributed2Coloring.LowerBound.N1000000PairTransitivity.i1 :
              Fin 3

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

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Distributed2Coloring.LowerBound.N1000000PairTransitivity.i2 :
                Fin 3

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

                Equations
                Instances For
                  source
                  def Distributed2Coloring.LowerBound.N1000000PairTransitivity.bit (k : ℕ) :
                  ℕ

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

                  Equations
                  Instances For
                    source
                    def Distributed2Coloring.LowerBound.N1000000PairTransitivity.dirMask (u v : V) :
                    Mask

                    The directed overlap mask between two vertices, as a 3×3 partial permutation bitmask.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem Distributed2Coloring.LowerBound.N1000000PairTransitivity.testBit_bit (k t : ℕ) :
                      (bit k).testBit t = decide (k = t)
                      source
                      theorem Distributed2Coloring.LowerBound.N1000000PairTransitivity.dirMask_testBit (u v : V) (i j : Fin 3) :
                      Nat.testBit (dirMask u v) (↑i * 3 + ↑j) = decide (↑u i = ↑v j)
                      source
                      theorem Distributed2Coloring.LowerBound.N1000000PairTransitivity.dirMask_lt (u v : V) :
                      dirMask u v < 1 <<< 9

                      This module intentionally contains only the low-level dirMask encoding lemmas.

                      The higher-level results that were once planned here are proved in N1000000Transitivity as: