Almost-direct products of free groups are torsion-free without generalized torsion (Corollary 5)

Disproved

PCB.torsion_free

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

bi-orderablegeneralized-torsiontorsion-free

An almost-direct product of free groups is torsion-free and has no generalized torsion. Once the goal equips the group with a bi-invariant ordering, the standard consequences follow: no positive power of a non-identity element is trivial, and no product of conjugates of a non-identity element is trivial, since such products are positive in any bi-invariant ordering. This is Corollary 5 of the paper.

Preamble

import Mathlib
import Definitions.Def_PCB_alg
import Definitions.Def_PCB_tor

Formal statement

namespace PCB

/-!  Milestone 4 (Corollary 5): an almost-direct product of free groups is
torsion-free and has no generalized torsion. By the goal, the group admits
a bi-invariant ordering, and bi-orderable groups are torsion-free and
admit no nontrivial product of conjugates of a single element. -/
theorem torsion_free {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
    (W : AlmostDirectProductWorld k G F) :
    TorsionFreeNoGeneralizedTorsion G := 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 (Corollary 5, the torsion statements).

Read-back

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

Restate: in an almost-direct product world, the ambient group is torsion-free and has no generalized torsion: no positive power of a non-identity element is trivial, and no product of conjugates of a non-identity element is trivial. Hypotheses: the world is given; no further hypotheses appear.

View graph