Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeBase

Algebraic cancellation lemma used to keep integer cross-multiplication checks from ballooning: we replace a term (s : ℚ) / (D : ℚ) by the reduced fraction obtained by cancelling g = gcd(|s|, D).

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Q :
Type

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

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

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

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

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

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

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

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.qOfNat (m : ℕ) :
          Q

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

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.iOfNat (m : ℕ) :
            ℤ

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

            Equations
            Instances For
              source
              def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.invDir (d : DirIdx) :
              DirIdx

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

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.basisDen (r : Block) :
                ℕ

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

                Equations
                Instances For
                  source
                  def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.bValNum (r : Block) (j : Fin 3) (k : DirIdx) :
                  ℤ

                  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
                    def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.bVal (r : Block) (j : Fin 3) (k : DirIdx) :
                    Q

                    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
                      def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasis (r : Block) (d : DirIdx) :
                      Matrix (Fin 3) (Fin 3) Q

                      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.N1000000BCompressionCompute.div_by_D_eq_div_by_div_gcd (s : ℤ) :
                        have g := s.natAbs.gcd N1000000Data.D; ↑s / ↑N1000000Data.D = ↑s / ↑↑g / ↑(N1000000Data.D / g)
                        source
                        def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasisIntEntry (r : Block) (d : DirIdx) (p q : Fin 3) :
                        ℤ

                        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.N1000000BCompressionCompute.basisDenQ_ne_zero (r : Block) :
                          ↑(basisDen r) ≠ 0
                          source
                          theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasis_entry_eq_div (r : Block) (d : DirIdx) (p q : Fin 3) :
                          compBasis r d p q = ↑(compBasisIntEntry r d p q) / (↑(basisDen r) * ↑(basisDen r))
                          source
                          def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasisSymm (r : Block) (d : DirIdx) :
                          Matrix (Fin 3) (Fin 3) Q

                          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
                            def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.idDirIdx :
                            DirIdx

                            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
                              def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.varOrbit (i : Var) :
                              DirIdx

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

                              Equations
                              Instances For