The lexicographic cone satisfies the trichotomy law (Theorem 4 (ii))
DisprovedPCB.lex_cone_trichotomynormal-formspositive-conestrichotomy
The lexicographic cone satisfies the trichotomy law of Definition 1. Every non-identity element has a highest nontrivial component in its normal form; since the Magnus-type cone of the corresponding free factor satisfies the trichotomy law, either the element or its inverse lies in the lexicographic cone, and never both. This is Theorem 4 (ii) of the paper.
Preamble
import Mathlib import Definitions.Def_PCB_alg import Definitions.Def_PCB_tor
Formal statement
namespace PCB
/-! Milestone 2 (Theorem 4 (ii)): the lexicographic cone satisfies the
trichotomy law. Every non-identity element has a highest nontrivial
component in its normal form; since the Magnus-type cone of the
corresponding free factor satisfies trichotomy, either the element or its
inverse lies in the lexicographic cone, and never both. -/
theorem lex_cone_trichotomy {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
(W : AlmostDirectProductWorld k G F) :
(∀ g : G, g ≠ 1 → (g ∈ lexCone W ∨ g⁻¹ ∈ lexCone W)) ∧
(∀ g ∈ lexCone W, g⁻¹ ∉ 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 (ii)).
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in an almost-direct product world, every non-identity element of the group or its inverse lies in the lexicographic cone, and the inverse of no element of the cone lies in the cone. Hypotheses: the world is given; no further hypotheses appear.