pub fn symmetric_resolution_growth(
cover: &Cover,
generators: &[CubeSym],
rounds: usize,
) -> Vec<(usize, usize)>Expand description
Symmetric resolution closure — rules beget rules, collapsed by symmetry. From a cover’s blockers, repeatedly resolve all pairs (each resolvent a new rule) and record, per round, both the raw count of distinct derived rules and the count of their orbit representatives under the automorphism group. The widening gap between the two is the symmetry collapse of the resolution proof: raw resolution explodes, but modulo symmetry only a handful of essentially-distinct rules are ever derived — the geometric reason symmetric proof systems refute pigeonhole in polynomial size where plain resolution cannot.