LeanPool.TwoColoringOneRound.LowerBound.N1000000OrbitalBasis

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.n : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.n = Distributed2Coloring.LowerBound.N1000000Data.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.Q : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.Q = ℚ

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.SymN : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.SymN = Distributed2Coloring.LowerBound.Sym Distributed2Coloring.LowerBound.N1000000OrbitalBasis.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.V : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.V = Distributed2Coloring.LowerBound.Vertex Distributed2Coloring.LowerBound.N1000000OrbitalBasis.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.G : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.G = Distributed2Coloring.LowerBound.Correlation.G Distributed2Coloring.LowerBound.N1000000OrbitalBasis.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.Mask : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.Mask = Distributed2Coloring.LowerBound.Mask

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.DirIdx : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.DirIdx = Distributed2Coloring.LowerBound.N1000000StructureConstants.DirIdx

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i0 : Fin 3

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i0 = ⟨0, Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i0._proof_1⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i1 : Fin 3

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i1 = ⟨1, Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i1._proof_1⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i2 : Fin 3

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i2 = ⟨2, Distributed2Coloring.LowerBound.N1000000OrbitalBasis.i2._proof_1⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s0 : SymN

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s0 = ⟨0, Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s0._proof_1⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s1 : SymN

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s1 = ⟨1, Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s1._proof_1⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s2 : SymN

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s2 = ⟨2, Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s2._proof_1⟩

def Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseTuple : Tuple 3 n

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseTuple ⟨0, isLt⟩ = Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s0
• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseTuple ⟨1, isLt⟩ = Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s1
• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseTuple ⟨2, isLt⟩ = Distributed2Coloring.LowerBound.N1000000OrbitalBasis.s2

theorem Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseTuple_injective : Function.Injective baseTuple

def Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseVertex : V

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.N1000000OrbitalBasis.baseSet : Finset SymN

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.N1000000OrbitalBasis.outside (x : SymN) : Prop

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.outside x = (x ∉ Distributed2Coloring.LowerBound.N1000000OrbitalBasis.baseSet)

@[implicit_reducible]

instance Distributed2Coloring.LowerBound.N1000000OrbitalBasis.instDecidablePredSymNOutside : DecidablePred outside

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitalBasis.instDecidablePredSymNOutside x = id inferInstance

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitalBasis.OutsideSym : Type

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.N1000000OrbitalBasis.A (d : DirIdx) : Matrix V V Q

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

Equations

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

@[simp]

theorem Distributed2Coloring.LowerBound.N1000000OrbitalBasis.A_apply (d : DirIdx) (u v : V) : A d u v = if N1000000PairTransitivity.dirMask v u = N1000000StructureConstants.maskAt d then 1 else 0

def Distributed2Coloring.LowerBound.N1000000OrbitalBasis.ASymm (d : DirIdx) : Matrix V V Q

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

Equations

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