LeanPool.TwoColoringOneRound.LowerBound.N1000000OrbitCounting

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitCounting.n : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.n = Distributed2Coloring.LowerBound.N1000000Data.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitCounting.SymN : Type

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitCounting.V : Type

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

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitCounting.DirIdx : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.DirIdx = Distributed2Coloring.LowerBound.N1000000StructureConstants.DirIdx

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000OrbitCounting.AvailFrom3 : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.AvailFrom3 = Distributed2Coloring.LowerBound.N1000000AvailFrom.AvailFrom 3

@[instance_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeAvailFrom3 : Fintype AvailFrom3

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeAvailFrom3 = inferInstance

@[implicit_reducible]

def Distributed2Coloring.LowerBound.N1000000OrbitCounting.FreeCol (k : DirIdx) : Type

Free columns for a directed type k: coordinates not equal to any base symbol.

Equations

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

@[instance_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeFreeCol (k : DirIdx) : Fintype (FreeCol k)

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeFreeCol k = id inferInstance

def Distributed2Coloring.LowerBound.N1000000OrbitCounting.BaseOrbit (k : DirIdx) : Type

Vertices in the orbit of the base vertex with directed type k.

Equations

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

@[instance_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeBaseOrbit (k : DirIdx) : Fintype (BaseOrbit k)

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.instFintypeBaseOrbit k = id inferInstance

theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.baseOrbit_freeCoord_outside {k : DirIdx} (u : BaseOrbit k) (j : FreeCol k) : 3 ≤ ↑(↑↑u ↑j)

def Distributed2Coloring.LowerBound.N1000000OrbitCounting.encodeBaseOrbit (k : DirIdx) (u : BaseOrbit k) : FreeCol k ↪ AvailFrom3

Encode the free coordinates of a base orbit as an embedding into available symbols.

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.encodeBaseOrbit k u = { toFun := fun (j : Distributed2Coloring.LowerBound.N1000000OrbitCounting.FreeCol k) => ⟨↑↑u ↑j, ⋯⟩, inj' := ⋯ }

noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeTuple (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) : Tuple 3 n

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

Equations

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

theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeTuple_of_colMatch_none (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) (j : Fin 3) (hc : N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt k) j = none) : decodeTuple k g j = ↑(g ⟨j, hc⟩)

theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeTuple_of_colMatch_some (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) (j i : Fin 3) (hc : N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt k) j = some i) : decodeTuple k g j = ↑N1000000OrbitalBasis.baseVertex i

noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeVertex (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) : V

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeVertex k g = ⟨Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeTuple k g, ⋯⟩

theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeVertex_mask (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) : N1000000PairTransitivity.dirMask N1000000OrbitalBasis.baseVertex (decodeVertex k g) = N1000000StructureConstants.maskAt k

noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeBaseOrbit (k : DirIdx) (g : FreeCol k ↪ AvailFrom3) : BaseOrbit k

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

Equations

• Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeBaseOrbit k g = ⟨Distributed2Coloring.LowerBound.N1000000OrbitCounting.decodeVertex k g, ⋯⟩

theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.base_eq_of_colMatch {k : DirIdx} (u : BaseOrbit k) {j i : Fin 3} (h : N1000000StructureConstants.colMatch (N1000000StructureConstants.maskAt k) j = some i) : ↑↑u j = ↑N1000000OrbitalBasis.baseVertex i

noncomputable def Distributed2Coloring.LowerBound.N1000000OrbitCounting.baseOrbitEquivEmbedding (k : DirIdx) : BaseOrbit k ≃ (FreeCol k ↪ AvailFrom3)

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

Equations

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

theorem Distributed2Coloring.LowerBound.N1000000OrbitCounting.baseOrbit_card (k : DirIdx) : Fintype.card (BaseOrbit k) = N1000000StructureConstants.baseTypeCount k