Round-six lemma `ctlPh_runs`