Function certify_gates_within 

pub fn certify_gates_within(
    grid: &Word,
    datapath: &Word,
    budget: u64,
) -> Result<PlacementCertificate, CertifyRefusal>

certify_gates_bounded against an EXPLICIT gate ceiling — the seam a lock shrinks to prove the budget is live code and not a constant nobody reads.