Prove2Me

The subproducts of theta and the zeta are outer (Theorem 2.1)

Disproved
FRV.outer_independent

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

inner-automorphismsouter-automorphismsvirtual-braids

For n at least three, every nontrivial subproduct of the automorphisms of Theorem 2.1 is not an inner automorphism of the universal virtual braid group: the product of the zeta over a nonempty list of indices, optionally composed with theta, never acts as conjugation by a single element. The proof projects to the unrestricted quotient and uses the action on the abelianization together with the non-innerness technique of Makri. The classes therefore generate a subgroup of the outer automorphism group isomorphic to the elementary Abelian 2-group of rank k+1. This is the outer part of Theorem 2.1 of the paper.

Preamble
import Mathlib
import Definitions.Def_FRV_alg
import Definitions.Def_FRV_tor
Formal statement
namespace FRV

/-!  Milestone 2 (Theorem 2.1): the classes of theta, zeta_1, ..., zeta_k
generate a subgroup isomorphic to (Z_2)^(k+1) in the outer automorphism
group of the universal virtual braid group: every nontrivial subproduct -
zeta over a nonempty list of indices, optionally composed with theta - is
not inner. The proof projects to the unrestricted virtual braid group and
uses the action on the abelianization together with the Makri proposition
on non-innerness. -/
theorem outer_independent {n k : ℕ} {V Q1 Q2 QM1 QM2 Mk U : Type*}
    [Group V] [Group Q1] [Group Q2] [Group QM1] [Group QM2] [Group Mk] [Group U]
    (W : ForbiddenWorld n k V Q1 Q2 QM1 QM2 Mk U) (hn : 3 ≤ n) :
    ∀ (L : List (Fin k)) (eps : Bool), (L ≠ [] ∨ eps = true) →
      ¬ ∃ g : V, ∀ x : V, zetaApplied W L eps x = g * x * g⁻¹ := by sorry

end FRV
Source
O. Ocampo, C. Stylianakis, Forbidden relations in universal virtual braid groups, arXiv:2606.06095 (2026), Section 2 (Theorem 2.1).
Read-back

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

Restate: in a forbidden-relations world with at least three strands, for every list of family indices and every flag, if the list is nonempty or the flag is set, then there is no element of the group such that the corresponding subproduct automorphism sends every element to the conjugate of it by that element. Hypotheses: the world is given; the number of strands is at least three; no further hypotheses appear.

View graph