The lexicographic cone is a positive cone (Theorem 4)

Disproved

PCB.lex_positive_cone

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

almost-direct-productsbi-orderablepositive-cones

The lexicographic cone of Definition 2 is a positive cone in the sense of Definition 1: it is closed under products, it contains neither the identity nor the inverse of any of its elements, every non-identity element or its inverse lies in it, and it is invariant under conjugation. By the recipe of Definition 1, it defines a bi-invariant ordering on every almost-direct product of free groups. This is Theorem 4 of the paper, the main theorem of the mission.

Preamble

import Mathlib
import Definitions.Def_PCB_alg
import Definitions.Def_PCB_tor

Formal statement

namespace PCB

/-!  The goal (Theorem 4): the lexicographic cone of Definition 2 is a
positive cone: it is closed under products, it contains neither the
identity nor inverses of its elements, every non-identity element or its
inverse lies in it, and it is invariant under conjugation. It therefore
defines a bi-invariant ordering on every almost-direct product of free
groups. -/
theorem lex_positive_cone {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
    (W : AlmostDirectProductWorld k G F) :
    IsPositiveCone (lexCone W) := by sorry

end PCB

Source

O. Ocampo, J. R. T. Theodoro de Lima, Positive cones and bi-orderings on almost-direct products of free groups, arXiv:2209.04706 (2022), Section 2 (Theorem 4, the main theorem).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in an almost-direct product world, the lexicographic cone satisfies the positive-cone predicate: it is closed under products, contains neither the identity nor inverses of its elements, every non-identity element or its inverse lies in it, and it is invariant under conjugation. Hypotheses: the world is given; no further hypotheses appear.

View graph