Function is_fractional_automorphism 

pub fn is_fractional_automorphism(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    partition: &[usize],
) -> bool

Verify that block-averaging over partition gives a doubly-stochastic matrix B commuting with the co-occurrence matrix A. B is doubly-stochastic by construction (each row/column sums to 1), so this checks BA = AB, which holds iff partition is equitable — the exact (integer) certificate. The identity (1/|cell(u)|)·Σ_{x∈cell(u)} A[x][w] = (1/|cell(w)|)·Σ_{x∈cell(w)} A[u][x] is verified cross-multiplied.