Function check_res_width_lower_bound 

pub fn check_res_width_lower_bound(
    clauses: &[Vec<Lit>],
    w: usize,
    convention: WidthConvention,
    closed: &BTreeSet<MaskClause>,
) -> bool

Re-check a resolution-width lower-bound certificate (zero trust in the producer). closed certifies “no width-w resolution refutation of clauses under convention” iff: (i) it contains every admissible axiom, (ii) it is tautology-free, (iii) it is closed under width-≤ w resolution, and (iv) it lacks the empty clause. Soundness is an induction over any purported width-w derivation: its every clause lies in closed, and ⊥ ∉ closed. A padded (superset) certificate still certifies — extra clauses only weaken the producer, never the bound.