LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSi

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasisSymm_var_matches_Si (r : Block) (i : Var) : compBasisSymm r (varOrbit i) = N1000000WedderburnData.blockScales[↑r]! • N1000000WeakDuality.Si r i