Round-six lemma `recip_spec`