Round-six lemma `partP_spec`