The algebraic witness criterion for the orientation-preserving involution of the torus (Lemma 26)

Disproved

BUP.tau1_witness

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

borsuk-ulambraid-groupstorus

In the torus world, the homotopy class with induced homomorphism h does not have the Borsuk-Ulam property if and only if there are pure braids a and b such that the half-twist conjugation relation holds - a times the conjugate of b equals b times a - and the image of the first coordinate loop under h is the Fadell-Neuwirth projection of a times the conjugate of a, while the image of the second coordinate loop under h is the projection of b. The criterion unwinds the diagram of Proposition 6 along the decomposition of the full two-string braid group of the torus into the pure braid group and the half-twist.

Preamble

import Mathlib
import Definitions.Def_BUP_alg
import Definitions.Def_BUP_tor

Formal statement

namespace BUP

/-!  Milestone 4 (Lemma 26): the algebraic witness criterion for the
orientation-preserving involution of the torus. The homotopy class with
induced homomorphism h does not have the Borsuk-Ulam property if and only if
there are pure braids a and b such that a conjugated by the half-twist
commutation relation holds (a times the conjugate of b equals b times a), the
image of the first coordinate loop under h is the Fadell-Neuwirth projection
of a times the conjugate of a, and the image of the second coordinate loop
under h is the projection of b. The proof unwinds the diagram of Proposition 6
along the decomposition of the full braid group into the pure braid group and
the half-twist. -/
theorem tau1_witness {A B P Bg : Type*} [Group A] [Group B] [Group P] [Group Bg]
    (W : TorusWorld A B P Bg) (h : A →* A) :
    NoBUP W.C W.D h ↔
      ∃ a b : P,
        a * W.D.lsigma b = b * a ∧
        h (W.e1) = W.D.p1 (a * W.D.lsigma a) ∧
        h (W.e2) = W.D.p1 b := by sorry

end BUP

Source

D. L. Goncalves, J. Guaschi, V. C. Laass, The Borsuk-Ulam property for homotopy classes of selfmaps of surfaces of Euler characteristic zero, arXiv:1608.00397 (2016), Section 5 (Lemma 26).

Read-back

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

Restate: in a torus world, the homotopy class with induced homomorphism h does not have the Borsuk-Ulam property if and only if there are pure braids a and b such that a times the conjugate of b under the half-twist equals b times a, the image of the first coordinate loop under h is the Fadell-Neuwirth projection of a times the conjugate of a, and the image of the second coordinate loop under h is the projection of b. Hypotheses: the torus world is given; no further hypotheses appear.

View graph