Function prove_certify_check_bounded 

pub fn prove_certify_check_bounded(
    premises: &[ProofExpr],
    goal: &ProofExpr,
    max_depth: usize,
) -> VerifiedProof

Like prove_certify_check but caps the backward-chainer search depth, so a goal the kernel cannot reach fails FAST instead of exhausting the default depth. Keeps “prove-with-ours-first” cheap when answering a grid cell by cell: a shallow kernel attempt certifies what it can, then falls through to the oracle.