Skip to main content

agl_collapse_via_transvections

Function agl_collapse_via_transvections 

Source
pub fn agl_collapse_via_transvections(n: usize) -> AglCollapse
Expand description

The AGL collapse via CNF-preserving affine moves — scales to n = 4. Since AGL = ⟨Bₙ, transvections⟩, uniting the Bₙ orbits connected by a single CNF-preserving transvection (its image stays a valid clause set, then Bₙ-canonicalized) merges genuine affine equivalences. The component count is an upper bound on the AGL-class count — every union is a real affine equivalence; only merges that must route through a non-CNF affine intermediate are missed — hence a rigorous lower bound on the collapse, exact when the walk is tight (checked against agl_collapse_exact at n = 3).