Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000OrbitCounting

LeanPool.TwoColoringOneRound.LowerBound.N1000000OrbitCounting #

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

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

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

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

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

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

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

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

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

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            noncomputable instance Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeAvailFrom3 :
            Fintype AvailFrom3
            Equations
            source
            def Distributed2Coloring.LowerBound.N1000000OrbitCounting.FreeCol (k : DirIdx) :
            Type

            Free columns for a directed type k: coordinates not equal to any base symbol.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[implicit_reducible]
              noncomputable instance Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeFreeCol (k : DirIdx) :
              Fintype (FreeCol k)
              Equations
              source
              def Distributed2Coloring.LowerBound.N1000000OrbitCounting.BaseOrbit (k : DirIdx) :
              Type

              Vertices in the orbit of the base vertex with directed type k.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implicit_reducible]
                noncomputable instance Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeBaseOrbit (k : DirIdx) :
                Fintype (BaseOrbit k)
                Equations
                source
                theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.baseOrbit_freeCoord_outside {k : DirIdx} (u : BaseOrbit k) (j : FreeCol k) :
                3 ≤ ↑(↑↑u ↑j)
                source
                noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeTuple (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) :
                Tuple 3 n

                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.N1000000OrbitCounting.decodeTuple_of_colMatch_none (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) (j : Fin 3) (hc : N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt k) j = none) :
                  decodeTuple k g j = ↑(g ⟨j, hc⟩)
                  source
                  theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeTuple_of_colMatch_some (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) (j i : Fin 3) (hc : N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt k) j = some i) :
                  decodeTuple k g j = ↑N1000000OrbitalBasis.baseVertex i
                  source
                  noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeVertex (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) :
                  V

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

                  Equations
                  Instances For
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeVertex_mask (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) :
                    N1000000PairTransitivity.dirMask N1000000OrbitalBasis.baseVertex (decodeVertex k g) = N1000000StructureConstants.maskAt k
                    source
                    noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeBaseOrbit (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) :
                    BaseOrbit k

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

                    Equations
                    Instances For
                      source
                      theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.base_eq_of_colMatch {k : DirIdx} (u : BaseOrbit k) {j i : Fin 3} (h : N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt k) j = some i) :
                      ↑↑u j = ↑N1000000OrbitalBasis.baseVertex i
                      source
                      noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.baseOrbitEquivEmbedding (k : DirIdx) :
                      BaseOrbit k ≃ (FreeCol k ↪ AvailFrom3)

                      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.N1000000OrbitCounting.baseOrbit_card (k : DirIdx) :
                        Fintype.card (BaseOrbit k) = N1000000StructureConstants.baseTypeCount k