Function ns_lower_bound_witness 

pub fn ns_lower_bound_witness(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    degree: usize,
) -> Option<Vec<u64>>

A re-checkable degree-d Nullstellensatz LOWER-bound certificate. Where nullstellensatz_refutes decides whether a degree-d refutation exists, this witnesses its NON-existence: a GF(2) linear functional L on the degree-≤ d monomials (a *degree-d pseudo-expectation) with L(1) = 1andL(m · p_C) = 0for every generator. Such anLexists iff1is **not** in theGF(2)-span of the generators, i.e. iff there is no degree-drefutation — soSome(L)certifies the lower boundNS-degree(F) > d, independently re-checkable by [check_ns_lower_bound] (no trust in the solver). The certificate is returned as the list of monomials on which Lis1. None means a degree-drefutation exists (no lower bound atd). Multi-word linear algebra, so the monomial basis is not size-capped — only num_vars ≤ 20` for the explicit basis enumeration.