Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000MaskAtFacts

LeanPool.TwoColoringOneRound.LowerBound.N1000000MaskAtFacts #

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000MaskAtFacts.Mask :
Type

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

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

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

    Equations
    Instances For
      source
      theorem Distributed2Coloring.LowerBound.N1000000MaskAtFacts.maskAt_testBit_eq_decide_colMatch (d : DirIdx) (i j : Fin 3) :
      Nat.testBit (N1000000StructureConstants.maskAt d) (↑i * 3 + ↑j) = decide (N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt d) j = some i)
      source
      theorem Distributed2Coloring.LowerBound.N1000000MaskAtFacts.maskAt_testBit_eq_decide_rowMatch (d : DirIdx) (i j : Fin 3) :
      Nat.testBit (N1000000StructureConstants.maskAt d) (↑i * 3 + ↑j) = decide (N1000000StructureConstants.rowMatch (N1000000StructureConstants.maskAt d) i = some j)