LeanPool.TwoColoringOneRound.LowerBound.N1000000Relaxation #

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.n :

ℕ

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.n = Distributed2Coloring.LowerBound.N1000000Data.n

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.SymN :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.SymN = Distributed2Coloring.LowerBound.Sym Distributed2Coloring.LowerBound.N1000000Relaxation.n

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.G :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.G = Distributed2Coloring.LowerBound.Correlation.G Distributed2Coloring.LowerBound.N1000000Relaxation.n

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.Q :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.Q = ℚ

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.Var :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.Var = Distributed2Coloring.LowerBound.N1000000WeakDuality.Var

Instances For

source

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N1000000Relaxation.instFintypeG :

Fintype G

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.instFintypeG = inferInstance

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.LabelTriple :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.LabelTriple = Distributed2Coloring.LowerBound.N1000000Witness.LabelTriple

Instances For

source

instance Distributed2Coloring.LowerBound.N1000000Relaxation.instNeZeroNatN :

NeZero n

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.symOfNat (k : ℕ) :

SymN

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.symOfNat k = Fin.ofNat Distributed2Coloring.LowerBound.N1000000Relaxation.n k

Instances For

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.symOfNat_injective_of_lt {a b : ℕ} (ha : a < n) (hb : b < n) :

symOfNat a = symOfNat b → a = b

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.labelGet (t : LabelTriple) (i : Fin 3) :

SymN

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.N1000000Relaxation.tupleOfLabels (t : LabelTriple) :

Tuple 3 n

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.tupleOfLabels t i = Distributed2Coloring.LowerBound.N1000000Relaxation.labelGet t i

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.labelGetNat (t : LabelTriple) (i : Fin 3) :

ℕ

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.labelGetNat t i = match ↑i with | 0 => t.1 | 1 => t.2.1 | x => t.2.2

Instances For

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.labelGet_eq_symOfNat_labelGetNat (t : LabelTriple) (i : Fin 3) :

labelGet t i = symOfNat (labelGetNat t i)

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.LabelsDistinct (t : LabelTriple) :

Prop

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.LabelsDistinct t = (t.1 ≠ t.2.1 ∧ t.1 ≠ t.2.2 ∧ t.2.1 ≠ t.2.2)

Instances For

source

@[implicit_reducible]

instance Distributed2Coloring.LowerBound.N1000000Relaxation.instDecidableLabelsDistinct (t : LabelTriple) :

Decidable (LabelsDistinct t)

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.instDecidableLabelsDistinct t = id inferInstance

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.LabelsInRange (t : LabelTriple) :

Prop

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

@[implicit_reducible]

instance Distributed2Coloring.LowerBound.N1000000Relaxation.instDecidableLabelsInRange (t : LabelTriple) :

Decidable (LabelsInRange t)

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.instDecidableLabelsInRange t = id inferInstance

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.labelGetNat_lt (t : LabelTriple) (hr : LabelsInRange t) (i : Fin 3) :

labelGetNat t i < n

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.labelGetNat_injective_of_labelsDistinct (t : LabelTriple) (h : LabelsDistinct t) :

Function.Injective (labelGetNat t)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.tupleOfLabels_injective_of_labelsDistinct (t : LabelTriple) (h : LabelsDistinct t) (hr : LabelsInRange t) :

Function.Injective (tupleOfLabels t)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepU_injective (i : Var) :

Function.Injective (tupleOfLabels N1000000Witness.varRepU [↑i]!)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepV_injective (i : Var) :

Function.Injective (tupleOfLabels N1000000Witness.varRepV [↑i]!)

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.varRepUAt (i : Var) :

LabelTriple

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.varRepUAt i = Distributed2Coloring.LowerBound.N1000000Witness.varRepU [↑i]!

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Relaxation.varRepVAt (i : Var) :

LabelTriple

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.varRepVAt i = Distributed2Coloring.LowerBound.N1000000Witness.varRepV [↑i]!

Instances For

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepUAt_labelsDistinct (i : Var) :

LabelsDistinct (varRepUAt i)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepVAt_labelsDistinct (i : Var) :

LabelsDistinct (varRepVAt i)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepUAt_labelsInRange (i : Var) :

LabelsInRange (varRepUAt i)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepVAt_labelsInRange (i : Var) :

LabelsInRange (varRepVAt i)

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepUAt_injective (i : Var) :

Function.Injective (tupleOfLabels (varRepUAt i))

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.varRepVAt_injective (i : Var) :

Function.Injective (tupleOfLabels (varRepVAt i))

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.varRepVertexU (i : Var) :

Vertex n

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.N1000000Relaxation.varRepVertexV (i : Var) :

Vertex n

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.N1000000Relaxation.xFromColoring (f : Coloring n) :

Var → 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.N1000000Relaxation.edgeVarVar :

Var

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

Equations

Distributed2Coloring.LowerBound.N1000000Relaxation.edgeVarVar = ⟨Distributed2Coloring.LowerBound.N1000000Data.edgeVar, Distributed2Coloring.LowerBound.N1000000Relaxation.edgeVarVar._proof_1 ⟩

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.edgeRepTuple :

Tuple 4 n

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.N1000000Relaxation.edgeRepTuple_injective :

Function.Injective edgeRepTuple

source

def Distributed2Coloring.LowerBound.N1000000Relaxation.edgeRep :

Edge n

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.N1000000Relaxation.edgeRep_src :

edgeRep.src = varRepVertexV edgeVarVar

source

theorem Distributed2Coloring.LowerBound.N1000000Relaxation.edgeRep_dst :

edgeRep.dst = varRepVertexU edgeVarVar

This file currently defines the reduced orbit variables xFromColoring and the concrete edge representative edgeRep. The remaining objective link

xEdge (xFromColoring f) = edgeCorrelation f

is deferred to a separate module (it uses orbit-stabilizer / pretransitivity for the action of Sym(n) on Edge n).