Round-six lemma `KK_log`