Higman showed that finitely generated groups embed in finitely presented groups exactly when they are recursively presented, and Leary showed that countable groups embed in groups of type FP_2. The question is whether these embedding results extend to higher finiteness degrees FP_n and F_n. This was asked by Fournier-Facio and Zaremsky and suggested by Gromov.

The finiteness degree is raised with ascending HNN extensions, via a degree-raising criterion (Theorem D) proved with mapping-cone arguments on partial resolutions. A complex-of-groups construction over a finite oriented triple system, built from the Fano plane with incidence-graph girth at least 12, makes the vertex groups embed. Products of endomorphisms with commuting images are controlled at the chain level. Oracle-relative Higman–Neumann–Neumann embeddings then give the universal groups.

For every n≥2, every countable group embeds in a group of type FP_n. There is a group of type F_n containing every recursively presented group, so a finitely generated group embeds in an F_n group iff it is recursively presented. The target groups can be chosen to be two-generated, and Theorem A was formalized in Lean/Mathlib.