Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000IntersectionCounting

LeanPool.TwoColoringOneRound.LowerBound.N1000000IntersectionCounting #

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

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

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

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

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

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

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

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

        Equations
        Instances For
          source
          def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.Inter {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) :
          Type

          The actual intersection fiber: vertices v with base-type a and relative-type d to u.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            noncomputable instance Distributed2Coloring.LowerBound.N1000000IntersectionCounting.instFintypeInter {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) :
            Fintype (Inter u a d)
            Equations
            source
            def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.FreeCoord (a d : DirIdx) :
            Type

            Free coordinates for the intersection number N[k][a][d]: positions j where v_j is neither a base symbol (a) nor a reused symbol from u (d).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[implicit_reducible]
              noncomputable instance Distributed2Coloring.LowerBound.N1000000IntersectionCounting.instFintypeFreeCoord (a d : DirIdx) :
              Fintype (FreeCoord a d)
              Equations
              source
              theorem Distributed2Coloring.LowerBound.N1000000IntersectionCounting.card_freeCoord (a d : DirIdx) :
              Fintype.card (FreeCoord a d) = N1000000StructureConstants.freeCoords (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d)
              source
              def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.AvailFor {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) :
              Type

              Available symbols for new coordinates: those not in baseSet and not used by u on its free columns.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implicit_reducible]
                noncomputable instance Distributed2Coloring.LowerBound.N1000000IntersectionCounting.instFintypeAvailFor {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) :
                Fintype (AvailFor u)
                Equations
                source
                theorem Distributed2Coloring.LowerBound.N1000000IntersectionCounting.card_availFor {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) :
                Fintype.card (AvailFor u) = n - (3 + N1000000StructureConstants.freeCols (N1000000StructureConstants.maskAt k))
                source
                theorem Distributed2Coloring.LowerBound.N1000000IntersectionCounting.card_embedding_freeCoord_availFor {k a d : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) :
                Fintype.card (FreeCoord a d ↪ AvailFor u) = (n - (3 + N1000000StructureConstants.freeCols (N1000000StructureConstants.maskAt k))).descFactorial (N1000000StructureConstants.freeCoords (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d))

                Intersection numbers.

                For u : BaseOrbit k, we show card (Inter u a d) = N k a d, where N is the closed-form structure-constant formula from N1000000StructureConstants.

                source
                @[reducible, inline]
                abbrev Distributed2Coloring.LowerBound.N1000000IntersectionCounting.AvailFrom3 :
                Type

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

                Equations
                Instances For
                  source
                  noncomputable def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.encodeInter {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (w : Inter u a d) :
                  FreeCoord a d ↪ AvailFor u

                  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
                    noncomputable def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.gOfEmbeddingVal {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (e : FreeCoord a d ↪ AvailFor u) :
                    N1000000OrbitCounting.FreeCol a → 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.N1000000IntersectionCounting.gOfEmbeddingVal_val_of_rowMatch_some {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (e : FreeCoord a d ↪ AvailFor u) (j : N1000000OrbitCounting.FreeCol a) (l : Fin 3) (hrow : N1000000StructureConstants.rowMatch (N1000000StructureConstants.maskAt d) ↑j = some l) :
                      ↑(gOfEmbeddingVal u a d hcons e j) = ↑↑u l
                      source
                      theorem Distributed2Coloring.LowerBound.N1000000IntersectionCounting.gOfEmbeddingVal_val_of_rowMatch_none {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (e : FreeCoord a d ↪ AvailFor u) (j : N1000000OrbitCounting.FreeCol a) (hrow : N1000000StructureConstants.rowMatch (N1000000StructureConstants.maskAt d) ↑j = none) :
                      ↑(gOfEmbeddingVal u a d hcons e j) = ↑(e ⟨↑j, ⋯⟩)
                      source
                      noncomputable def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.gOfEmbedding {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (e : FreeCoord a d ↪ AvailFor u) :
                      N1000000OrbitCounting.FreeCol a ↪ 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
                        noncomputable def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.decodeInter {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (e : FreeCoord a d ↪ AvailFor u) :
                        Inter u a d

                        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.N1000000IntersectionCounting.encode_decodeInter {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (e : FreeCoord a d ↪ AvailFor u) :
                          encodeInter u a d (decodeInter u a d hcons e) = e
                          source
                          theorem Distributed2Coloring.LowerBound.N1000000IntersectionCounting.decode_encodeInter {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) (w : Inter u a d) :
                          decodeInter u a d hcons (encodeInter u a d w) = w
                          source
                          noncomputable def Distributed2Coloring.LowerBound.N1000000IntersectionCounting.interEquivEmbedding {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) (hcons : N1000000StructureConstants.consistent (N1000000StructureConstants.maskAt k) (N1000000StructureConstants.maskAt a) (N1000000StructureConstants.maskAt d) = true) :
                          Inter u a d ≃ (FreeCoord a d ↪ AvailFor u)

                          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.N1000000IntersectionCounting.card_inter_eq_N {k : DirIdx} (u : N1000000OrbitCounting.BaseOrbit k) (a d : DirIdx) :
                            Fintype.card (Inter u a d) = N1000000StructureConstants.N k a d