LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars12to15

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

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

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

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