 Finite presentation of a centralizing HNN extension detects finite generation of its associated subgroup

For a finitely presented base group $G$ and subgroup $H$, the extension $⟨G,t\mid [t,h]=1(h\in H)⟩$ is finitely presented exactly when $H$ is finitely generated. Sufficiency follows by imposing commutation with finitely many subgroup generators. For necessity, any finite set normally generating the defining kernel uses only finitely many centralizing relators. If their subgroup $H_0$ is proper in $H$, Britton's lemma makes $t^{-1}ht{h}^{-1}$ nonidentity in the partial extension for $h\in H\setminus H_0$, contradicting the claimed kernel equality.

// Target: algebra.bigb