Round-six lemma `jcost_ax`