Round-six lemma `jsize_ax`