{"id":"palomar/PALOMAR-2026-10-30-000014","url":"https://github.com/flengyel/Dosen-Petric-Maximality/tree/2e771844077fd8cebfbe365230f13d4dd13a75b1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000014-v1.json","repo":"https://github.com/flengyel/Dosen-Petric-Maximality","tags":["math.CT","math.LO","msc:03G30","msc:03F07","msc:18A32"],"score":0,"title":"Maximality of the Došen–Petrić Boolean Category","trust":"high","domain":"math.CT","source":"palomar","authors":["Florian Lengyel"],"reviews":0,"subject":"math.CT","summary":"The freely generated zero-identity Boolean category of Došen and Petrić is maximal: every congruence preserved by the proof operations and uniform substitution is either equality or identifies every pair of parallel arrows. The Lean development constructs the equation-generated category and proves cut elimination and Boolean coherence, then proves maximality through both a symmetric-fold argument and the manuscript's short argument using two particular isomorphisms. It also formalizes the model corollary and the occurrence-substitution, finite-ordinal and structural-diagram constructions in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"Maximality of the Došen–Petrić Boolean Category, version 8","identifier":"https://github.com/flengyel/Dosen-Petric-Maximality/blob/6a66b14b382aac214b52c055b8bf281b35302239/manuscript/Maximality_of_the_Dosen_Petric_Boolean_Category_v8.tex","relationship":"formalizes"},{"title":"Proof-Theoretical Coherence","identifier":"https://www.mi.sanu.ac.rs/novi_sajt/biography/kosta/coh.pdf","relationship":"formalizes"}]}