Function symmetry_break_certified 

pub fn symmetry_break_certified(
    num_vars: usize,
    formula: &[Vec<Lit>],
    generators: &[Perm],
) -> (Vec<Vec<Lit>>, usize, Vec<ProofStep>)

Solve formula with FULL certified lex-leader symmetry breaking. For each generator, add the complete lex-leader chain (enforcing x ≤ₗₑₓ σ(x)) as PR steps — each clause certified by a principled witness — then solve and append the learned clauses as RUP steps. This prunes the non-leader half of every σ-orbit (real search collapse), with the whole refutation checked against formula alone. A generator whose chain cannot be fully certified is skipped (fail-closed); the result stays sound. Augment formula with the certified full lex-leader symmetry-breaking clauses for each generator, committing a generator’s chain only when every clause of it certifies (else the generator is skipped — fail-closed). Returns the augmented clause set, the extended variable count (base + auxiliaries), and the PR proof steps that justify the added clauses. This is the symmetry-breaking front half shared by certified solving and by search-collapse measurement.