The lexicographic ordering extends the Magnus-type orderings of the factors (Proposition 6)

Proved

PCB.projection_compatible

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

magnus-orderingspositive-conesprojections

The lexicographic bi-ordering extends the Magnus-type orderings of the free factors. The embedding of a positive element of a factor into the product has that element as its single nontrivial normal-form component, so it lies in the lexicographic cone, and the restriction of the lexicographic ordering to each factor recovers the given Magnus-type ordering. This is Proposition 6 of the paper.

Preamble

import Mathlib
import Definitions.Def_PCB_alg
import Definitions.Def_PCB_tor

Formal statement

namespace PCB

/-!  Milestone 5 (Proposition 6): the lexicographic bi-ordering extends
the Magnus-type orderings of the free factors. The embedding of a positive
element of a factor into the product lies in the lexicographic cone, and
its j-th component is the element itself, so the restriction of the
ordering to each factor recovers the given Magnus-type ordering. -/
theorem projection_compatible {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
    (W : AlmostDirectProductWorld k G F) :
    ∀ (j : Fin k) (f : F j), f ∈ W.cone j →
      embedFactor W j f ∈ lexCone W ∧ W.nf (embedFactor W j f) j = f := 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 6).

Read-back

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

Restate: in an almost-direct product world, for every factor index and every element of the corresponding free factor lying in its Magnus-type cone, the embedded element lies in the lexicographic cone and its normal-form component at that index is the element itself. Hypotheses: the world is given; the factor element lies in the cone of its factor; no further hypotheses appear.

View graph