Function lex_leader_clauses 

pub fn lex_leader_clauses(
    num_vars: usize,
    aux_start: usize,
    sigma: &Perm,
) -> (Vec<Vec<Lit>>, usize)

Build the full lex-leader symmetry-breaking predicate for sigma over the moved-variable order, enforcing x ≤ₗₑₓ σ(x). Returns the clauses (over base variables plus fresh auxiliary “tied-so-far” variables e_i, allocated starting at aux_start) and the number of aux variables used. This is the linear-size encoding that prunes the entire non-leader half of every σ-orbit — the real search-collapse predicate.