Round-six lemma `coreCost_le`