LeanPool.TwoColoringOneRound.LowerBound.N1000000MuWitness

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.LabelTriple : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000MuWitness.LabelTriple = (ℕ × ℕ × ℕ)

structure Distributed2Coloring.LowerBound.N1000000MuWitness.PairMapData : Type

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

• swap : Bool

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

• srcU : LabelTriple

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

• srcV : LabelTriple

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

• tgtU : LabelTriple

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

• tgtV : LabelTriple

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

• srcSyms : List ℕ

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

• tgtSyms : List ℕ

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

• idxV : LabelTriple

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muWitU : Array LabelTriple

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muWitV : Array LabelTriple

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muWitW : Array LabelTriple

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muKind : Array ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000MuWitness.muKind = #[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1]

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muBoxVar : Array ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000MuWitness.muBoxVar = #[0, 1, 2, 4, 6, 8, 9, 10, 13, 16, 17, 18, 19, 20, 21, 3, 5, 7, 11, 12, 14, 15, 22, 0, 0, 0, 0]

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muBoxCoeff : Array ℤ

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

Equations

• Distributed2Coloring.LowerBound.N1000000MuWitness.muBoxCoeff = #[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, -1, -1, -1, -1, -1, -1, -1, -1, 0, 0, 0, 0]

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muTriForm : Array ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000MuWitness.muTriForm = #[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 3, 1, 1]

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muTriVars : Array (ℕ × ℕ × ℕ)

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muMapUv : Array PairMapData

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muMapUw : Array PairMapData

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000MuWitness.muMapVw : Array PairMapData

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

Equations

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