feat: add Higman infinite finitely-presented simple group eval problem

[kim-em]

This PR adds Higman's infinite finitely-presented simple group theorem as an eval problem: there exists an infinite, finitely presented, simple group — some n and a finite relator set rels ⊆ FreeGroup (Fin n) for which PresentedGroup rels is both IsSimpleGroup and Infinite.

Pure existence of a pathological finite presentation. The first such examples come from Graham Higman's 1974 monograph Finitely Presented Infinite Simple Groups — the Higman–Thompson groups G_{n,r} (for integers n ≥ 2, r ≥ 1) as groups of piecewise-linear bijections of certain Cantor-like spaces. Higman's 1951 paper had earlier constructed a finitely generated infinite simple group as a simple quotient of the four-generator group ⟨a, b, c, d | bab⁻¹ = a², cbc⁻¹ = b², dcd⁻¹ = c², ada⁻¹ = d²⟩ (no nontrivial finite quotients) — but did not give a finite presentation for the simple quotient.

Mathlib v4.30 has FreeGroup, PresentedGroup, IsSimpleGroup, Infinite, the normal-closure substrate (Subgroup.IsNormalClosureFG), HNN extensions, and Britton's lemma (Mathlib/GroupTheory/HNNExtension.lean), but no Higman–Thompson construction, no Higman embedding theorem, and no construction of an infinite finitely-presented simple group on hand.

§122 of Knill's Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

🤖 Prepared with Claude+Codex+Aristotle