{"id":"palomar/PALOMAR-2026-10-12-000004","url":"https://github.com/homeowmorphism/finitely-generated-positive-cones-in-fnz/tree/20bfd7cb2abb773f2426af11cd0217b415f7497b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000004-v1.json","repo":"https://github.com/homeowmorphism/finitely-generated-positive-cones-in-fnz","tags":["math.GR","msc:20F60","msc:06F15","msc:20E05","group-theory","positive-cones","lean-formalization"],"score":0,"title":"Finitely generated positive cones in F_n × Z","trust":"high","domain":"math.GR","source":"palomar","authors":["Hang Lu Su"],"reviews":0,"subject":"math.GR","summary":"This Lean 4 formalization proves that, for every integer n at least two, the direct product of the free group of rank n with the infinite cyclic group has a positive cone generated by finitely many elements as a semigroup if and only if n is even. It formalizes Theorem 1.1 and Corollary 1.2 of Hang Lu Su's arXiv:2608.31103v1. The even-rank construction passes a positive cone through two finite-index subgroups. The converse derives the parity obstruction from finite circle domains and their endpoint actions. The required base-cone theorem and the supporting algebraic and dynamical arguments…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true,"formalizes":[{"title":"Finitely generated positive cones in F_n × Z","identifier":"https://arxiv.org/abs/2608.31103v1","relationship":"formalizes"},{"title":"Formal language convexity in left-orderable groups","identifier":"https://arxiv.org/abs/1905.13001","relationship":"formalizes"},{"title":"On braid groups","identifier":"https://doi.org/10.1070/SM2001v192n05ABEH000564","relationship":"formalizes"},{"title":"A remarkable family of left-ordered groups: central extensions of Hecke groups","identifier":"https://arxiv.org/abs/0909.4994v3","relationship":"formalizes"},{"title":"Ping-pong configurations and circular orders on free groups","identifier":"https://arxiv.org/abs/1709.02348v2","relationship":"formalizes"}]}