Round-six lemma `phiFE_runs`