Function ns_lower_bound_witness_on_basis 

pub fn ns_lower_bound_witness_on_basis(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    degree: usize,
    in_basis: &dyn Fn(Mono) -> bool,
) -> Option<Vec<u64>>

ns_lower_bound_witness restricted to a sub-basis of monomials: the functional L is sought only on monomials m with in_basis(m) (and L = 0 elsewhere), while the constraints ⟨L, m·p_C⟩ = 0 still range over all generators. Some(L) is a fully valid, check_ns_lower_bound-verifiable witness (the restriction only limits the search, not the check); None here means “no witness on this sub-basis” — which, unlike the full-basis version, does not imply a refutation exists. This exposes the structure of a lower bound: e.g. for pigeonhole, the partial-matching sub-basis already carries the certificate.