{"id":"palomar/PALOMAR-2026-09-26-000004","url":"https://github.com/yawara/t3-model-companion/tree/7d38e7d9fe9d131e713ce160853983321970e598","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-26-000004-v2.json","repo":"https://github.com/yawara/t3-model-companion","tags":["math.LO","math.GR","msc:03C60","msc:20A15","model-theory","group-theory","lean-formalization","exponent-three"],"score":0,"title":"Existence of a Model Companion for Groups of Exponent 3: Lean Formalization","trust":"high","domain":"math.LO","source":"palomar","authors":["Yawara Ishida"],"reviews":0,"subject":"math.LO","summary":"This project formalizes the existence of a model companion for the first-order theory of groups satisfying x^3 = 1. Its principal group-theoretic result gives a uniform, explicit bound on the number of generators needed to witness a failure of amalgamation with an existentially closed exponent-three group. The development follows the accompanying manuscript through free groups, associated graded Lie algebras, strict extensions, and the bounded-amalgamation criterion.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-26","reactions":{},"formalized":true,"formalizes":[{"title":"Existence of a Model Companion for Groups of Exponent 3","identifier":"https://arxiv.org/abs/2609.30061","relationship":"formalizes"}]}