Function affine_canonicalize 

pub fn affine_canonicalize(num_vars: usize, clauses: &[Vec<Lit>]) -> AffineCanon

The affine SBP — the canonical RREF break. Recover the formula’s GF(2)-linear substructure and take its reduced row-echelon form (via gf2::solve_gf2, whose kernel basis is the affine translation symmetry). The RREF partitions variables into free generators and determined coordinates: every variable the kernel never moves is forced to a constant, and every set the kernel moves in lockstep is an equivalence class collapsing to one representative. Substituting those determined coordinates out yields an equisatisfiable formula over the free generators alone — the affine symmetry quotiented to a canonical representative, exactly as a permutation lex-leader collapses an orbit. An inconsistent core instead AffineCanon::Refuteds (certified). Sound: the eliminated relations are GF(2)-entailed by the formula, so AffineCanonical::lift turns any reduced model into a full one.