Finitely generated positive cones in F_n × Z
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-12-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-12-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-12-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'