{"id":"palomar/PALOMAR-2026-11-01-000004","url":"https://github.com/RBarish-UTokyo/OrthogonalArtGalleryProblem-ExistsR-Lean4/tree/88aa383397d3c8a896ba127307a6073cf9765f2b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000004-v1.json","repo":"https://github.com/RBarish-UTokyo/OrthogonalArtGalleryProblem-ExistsR-Lean4","tags":["cs.CG","cs.CC","msc:68U05","msc:68Q17","msc:14P10","msc:68V20"],"score":0,"title":"The orthogonal art gallery problem is ∃ℝ-complete (point-point and point-boundary), in Lean 4","trust":"high","domain":"cs.CG","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"cs.CG","summary":"A Lean 4 formalization of material in a forthcoming manuscript entitled \"The Orthogonal Art Gallery Problem is ∃ℝ-complete\". A Lean 4 and Mathlib proof, for an explicit single-tape Turing machine model, that deciding whether an orthogonal simple polygon (every edge horizontal or vertical) with rational corners can be guarded by g guards is ∃ℝ-complete under polynomial-time many-one reductions, both when the guards must see the whole polygon (point-point) and when they must see only its boundary (point-boundary). Both problems also reduce to ETR by formulas whose only variables are the 2g…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"The Orthogonal Art Gallery Problem is ∃ℝ-complete","identifier":"","relationship":"formalizes"},{"title":"The Point-Boundary Art Gallery Problem is ∃ℝ-hard","identifier":"arXiv:2210.12817v3","relationship":"adapts"},{"title":"The Art Gallery Problem is ∃ℝ-complete","identifier":"","relationship":"formalizes"}]}