Round-six lemma `jcost_arith`