Group Approximation
The remote verified branch is automatically fast-forwarded after every complete Lean Prover CI success on main. Use that for the most recent correct Lean code.
A non-MF group
non_mf_groups_exist.tex proves that not every group is MF. non_mf_group_notes.tex is an archived research notebook for an earlier construction and is not a companion to the current manuscript.
Lean library
The Lean code is organized as a reusable library. Generic definitions and theorems are separated from concrete presentations and finite certificates, so other projects can import only the layers they need. GroupApproximation.lean imports the complete library.
| Area | Directories | Contents |
|---|---|---|
| Group theory | Algebra/, GroupTheory/, Higman/, Covers/ | Presentations, normal forms, free products, HNN extensions, quotients, embeddings, and torsion |
| Finite approximation | Sofic/, Criterion/, Stability/, Domination/, Matching/ | MF, sofic, and hyperlinear interfaces; finite models; residuals; matrix coronas; permanence and obstruction theorems |
| Rigidity | PropertyT/, Kazhdan/, PropertyTT/ | Fixed-point methods, relative property (T), spectral and Hodge certificates, and property (TT)/T |
| Analysis | Analysis/, KOne/, Leavitt/, Steinberg/ | Matrix estimates, projections, traces, C*-algebras, K-theory, and noncommutative rings |
| Other group constructions | Kun/, KunThom/, Quantum/, Monsters/ | Graph, permutation, quantum, and embedding constructions |
| Public and checked interfaces | Endpoint/, Meta/, Computability/, Manuscript/ | Stable exports, certificate replay, computability wrappers, statement matching, and axiom audits |
Modules named Literal* contain fully specified examples and certificate data; the generic modules do not depend on any particular presentation.