LeanPool.TwoColoringOneRound.LowerBound.N1000000StructureConstants

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000StructureConstants.n : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000StructureConstants.n = Distributed2Coloring.LowerBound.N1000000Data.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000StructureConstants.Q : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000StructureConstants.Q = ℚ

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000StructureConstants.Mask : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000StructureConstants.Mask = Distributed2Coloring.LowerBound.Mask

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000StructureConstants.DirIdx : Type

Directed overlap-type indices (0..33), in the canonical order used by the witness exporter.

Equations

• Distributed2Coloring.LowerBound.N1000000StructureConstants.DirIdx = Fin Distributed2Coloring.LowerBound.N1000000Witness.masks.size

def Distributed2Coloring.LowerBound.N1000000StructureConstants.maskAt (d : DirIdx) : Mask

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

Equations

• Distributed2Coloring.LowerBound.N1000000StructureConstants.maskAt d = Distributed2Coloring.LowerBound.N1000000Witness.masks[↑d]!

theorem Distributed2Coloring.LowerBound.N1000000StructureConstants.maskAt_lt_512 (d : DirIdx) : maskAt d < 1 <<< 9

def Distributed2Coloring.LowerBound.N1000000StructureConstants.colMatch (m : Mask) (j : Fin 3) : Option (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.

def Distributed2Coloring.LowerBound.N1000000StructureConstants.rowMatch (m : Mask) (i : Fin 3) : Option (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.

def Distributed2Coloring.LowerBound.N1000000StructureConstants.freeCols (m : Mask) : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000StructureConstants.freeCols m = {j : Fin 3 | Distributed2Coloring.LowerBound.N1000000StructureConstants.colMatch m j = none}.card

def Distributed2Coloring.LowerBound.N1000000StructureConstants.freeCoords (a d : Mask) : ℕ

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

Equations

• One or more equations did not get rendered due to their size.

def Distributed2Coloring.LowerBound.N1000000StructureConstants.consistentAt (k a d : Mask) (j : Fin 3) : Bool

Compatibility check for the triple of masks (k,a,d) in the representative intersection number N[k][a][d]: k is the type of (base,u), a is the type of (base,v), and d is the type of (v,u).

Equations

• One or more equations did not get rendered due to their size.

def Distributed2Coloring.LowerBound.N1000000StructureConstants.consistent (k a d : Mask) : Bool

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

Equations

• One or more equations did not get rendered due to their size.

def Distributed2Coloring.LowerBound.N1000000StructureConstants.baseTypeCount (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.

def Distributed2Coloring.LowerBound.N1000000StructureConstants.N (k a d : DirIdx) : ℕ

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

Equations

• One or more equations did not get rendered due to their size.