Function certify_linear_rigidity_within 

pub fn certify_linear_rigidity_within(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    budget: &Budget,
) -> Result<LinearRigidityCert, Refusal>

Certify the linear (GF(2)) rigidity of F, failing closed to budget: a system that exceeds the budget’s Gaussian cap returns Refusal::OverBudgetGaussian — the operational Chaitin ceiling — rather than a certificate we could not re-check.