Prove2Me

The automorphisms descend to the multi-virtual braid group (Corollary 2.3)

Disproved
FRV.mkvb_descend

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

automorphismsmulti-virtual-braidsouter-automorphisms

The automorphisms theta and zeta_k descend to commuting involutive automorphisms of the multi-virtual braid group: the multi-virtual relations are invariant under the automorphisms, so each is compatible with the quotient projection. Neither the descended theta, nor the descended zeta_k, nor their composition is an inner automorphism, so their classes generate a subgroup of the outer automorphism group isomorphic to Z_2 x Z_2. This is Corollary 2.3 of the paper.

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

/-!  Milestone 3 (Corollary 2.3): the automorphisms theta and zeta_k
descend to commuting involutive automorphisms of the multi-virtual braid
group M_kVB_n, and their classes generate a subgroup of the outer
automorphism group isomorphic to Z_2 x Z_2: the descended automorphisms
are involutions, compatible with the quotient projection, and no
nontrivial one is inner. -/
theorem mkvb_descend {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) :
    ∃ (phiTheta : Mk ≃* Mk) (phiZetaK : Mk ≃* Mk),
      IsInvolutive phiTheta ∧ IsInvolutive phiZetaK ∧
      (∀ x : V, phiTheta (W.pm x) = W.pm (W.theta x)) ∧
      (∀ x : V, phiZetaK (W.pm x) = W.pm (W.zeta ⟨k - 1, by have := W.hk; omega⟩ x)) ∧
      (¬ ∃ g : Mk, ∀ y : Mk, phiTheta y = g * y * g⁻¹) ∧
      (¬ ∃ g : Mk, ∀ y : Mk, phiZetaK y = g * y * g⁻¹) ∧
      (¬ ∃ g : Mk, ∀ y : Mk, phiTheta (phiZetaK y) = g * y * g⁻¹) := by sorry

end FRV
Source
O. Ocampo, C. Stylianakis, Forbidden relations in universal virtual braid groups, arXiv:2606.06095 (2026), Section 2 (Corollary 2.3).
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, there exist two automorphisms of the multi-virtual quotient such that each is an involution, the first maps the image of an element to the image of its theta-image, the second maps the image of an element to the image of its zeta-image, and none of the two, nor their composition, acts as conjugation by an element of the quotient. Hypotheses: the world is given; the number of strands is at least three; no further hypotheses appear.

View graph