{"id":"palomar/PALOMAR-2026-10-01-000005","url":"https://github.com/burkh4rt/Local-Conjugacy-Formalized/tree/a6ccde0b11cbef7dfd8344cbd21f5c6fd8edc887","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000005-v1.json","repo":"https://github.com/burkh4rt/Local-Conjugacy-Formalized","tags":["math.GR","msc:20E18","msc:20E45","msc:20J06","msc:05E18","group-theory","prosolvable-groups","cohomology","lean"],"score":0,"title":"Local conjugacy in prosolvable groups","trust":"high","domain":"math.GR","source":"palomar","authors":["Michael C. Burkhart"],"reviews":0,"subject":"math.GR","summary":"Lean 4 formalization of all eleven numbered results and both counterexamples in Local conjugacy in prosolvable groups, arXiv:2609.37678v1. Closed supplements of a pronilpotent normal subgroup are conjugate exactly when locally conjugate under the stated structural hypotheses. Continuous nonabelian cohomology has the stated primary restriction decomposition. Local inclusion and fixed-point results, the GL(2,3) quaternion counterexample, and the order-162 Heisenberg wreath-product counterexample are formalized.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"Local conjugacy in prosolvable groups","identifier":"arXiv:2609.37678v1","relationship":"formalizes"}]}