LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars4to7

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var4 (p q : Fin 3) : SiIntGoal ⟨4, ⋯⟩ ⟨4, ⋯⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var5 (p q : Fin 3) : SiIntGoal ⟨4, ⋯⟩ ⟨5, ⋯⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var6 (p q : Fin 3) : SiIntGoal ⟨4, ⋯⟩ ⟨6, ⋯⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var7 (p q : Fin 3) : SiIntGoal ⟨4, ⋯⟩ ⟨7, ⋯⟩ p q