LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars0to3

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

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

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

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