LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars12to15

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

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

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

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