Function affine_lex_leader_sbp 

pub fn affine_lex_leader_sbp(
    num_vars: usize,
    maps: &[Vec<(Vec<usize>, bool)>],
) -> (Vec<Vec<Lit>>, usize)

The lex-leader SBP for affine maps α: x ↦ Ax ⊕ b over GF(2) — the machinery that breaks the affine parity symmetries a variable/literal permutation SBP (lex_leader_sbp) structurally cannot express (an image bit is an XOR of several variables, not one literal). Each maps[k] is a per-output spec: maps[k][j] = (A_j, b_j) with α(x)[j] = ⊕_{i∈A_j} x_i ⊕ b_j. Each non-identity output is Tseitin-encoded as a fresh variable, then the standard prefix-equality chain [encode_lex_le] enforces x ≤_lex α(x). Satisfiability-preserving for any model-set affine symmetry (the lex-least model of each orbit survives). Returns the extra clauses and the new total variable count (aux appended above num_vars).