The lexicographic cone is invariant under decomposition-preserving automorphisms (Proposition 9)

Disproved

PCB.automorphism_invariant

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

almost-direct-productsautomorphismspositive-cones

The lexicographic cone is invariant under the automorphisms that preserve the almost-direct product decomposition. An automorphism mapping each free factor onto itself, whose restriction and inverse restriction preserve the Magnus-type cones, carries the lexicographic cone onto itself: it moves no components across factors and preserves the sign of the highest nontrivial one. This is Proposition 9 of the paper, which exhibits the rigidity of the lexicographic ordering.

Preamble

import Mathlib
import Definitions.Def_PCB_alg
import Definitions.Def_PCB_tor

Formal statement

namespace PCB

/-!  Milestone 7 (Proposition 9): the lexicographic cone is invariant
under the automorphisms preserving the almost-direct product decomposition.
An automorphism mapping each free factor onto itself with cone-preserving
restriction - and whose inverse does the same - carries the lexicographic
cone onto itself, so it preserves the lexicographic bi-ordering. -/
theorem automorphism_invariant {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
    (W : AlmostDirectProductWorld k G F) (φ : G ≃* G)
    (h : ∀ (j : Fin k) (f : F j), f ∈ W.cone j → ∃ f' ∈ W.cone j,
      ∀ i : Fin k, W.nf (φ (embedFactor W j f)) i = if h2 : i = j then h2 ▸ f' else 1)
    (hInv : ∀ (j : Fin k) (f : F j), f ∈ W.cone j → ∃ f' ∈ W.cone j,
      ∀ i : Fin k, W.nf (φ.symm (embedFactor W j f)) i = if h2 : i = j then h2 ▸ f' else 1) :
    (∀ g, g ∈ lexCone W → φ g ∈ lexCone W) ∧
    (∀ g, g ∈ lexCone W → φ.symm 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 (Proposition 9).

Read-back

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

Restate: in an almost-direct product world, for a multiplicative equivalence of the group that maps each free factor onto itself preserving the Magnus-type cones, and whose inverse does the same, both the equivalence and its inverse carry the lexicographic cone into itself. Hypotheses: the world is given; the equivalence and its inverse preserve the cones of the factors; no further hypotheses appear.

View graph