Lemma 3.8

Proved

QAlgorithms.Papers.Independent.Intake100.P55.lemma_3_8

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $R$ be a commutative unital ring with units $\lambda,\delta$ and $z\in R$ satisfying $\lambda^{-1}-\lambda=z(\delta-1)$ . For the affine algebra specify arbitrary scalars $q_s$ for every positive integer $s$ , with no admissibility or cyclotomic condition. Write $W_n$ and $\widehat W_n$ for the ordinary and affine BMW presentations of Definitions 3.1 and 3.6. Lower levels denote their canonical generator images; products of subspaces denote their $R$ -linear spans.

In either presentation, for $1\le i<n$ ,

g_i^2=1+\lambda^{-1}ze_i-zg_i,\qquad g_i^{-2}=1-\lambda ze_i+zg_i^{-1}.

These are the quadratic consequences of the skein relation. The inverse-square formula corrects the printed final $zg_i$ using the source's prescribed multiplication by $g_i^{-1}$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P55

Formal statement

noncomputable section

open scoped Classical

namespace QAlgorithms.Papers.Independent.Intake100.P55

section Statements

variable {R : Type*} [CommRing R] (P : Ground R) (q : ℕ → R)

/-- Lemma 3.8, PDF p.18, in both ordinary and affine BMW algebras.
Source correction: the printed final z*g_i is z*g_i inverse, as follows
by multiplying the skein relation by g_i inverse. Independent moderation
of this correction remains required. -/
theorem lemma_3_8 (aff : Bool) (n i : ℕ) (hi : BMWIndex n i) :
    ghCrossing P q aff n i false ^ 2 = 1 +
      algebraMap R _ ((↑P.lam⁻¹ : R) * P.z) * ghContraction P q aff n i -
      algebraMap R _ P.z * ghCrossing P q aff n i false ∧
    ghCrossing P q aff n i true ^ 2 = 1 -
      algebraMap R _ ((P.lam : R) * P.z) * ghContraction P q aff n i +
      algebraMap R _ P.z * ghCrossing P q aff n i true := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intake100.P55

end

Source

Affine Birman-Wenzl-Murakami Algebras and Tangles in the Solid Torus, arXiv:math/0411155v2, PDF p. 18, Lemma 3.8

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $R$ be a commutative ring, let $\lambda,\delta\in R^\times$ and $z\in R$ satisfy $\lambda^{-1}-\lambda=z(\delta-1)$ , and let $q:\mathbb N\to R$ be arbitrary. For either Boolean choice $\mathrm{aff}$ and any $n\in\mathbb N$ , work in the quotient $B_{\mathrm{aff},n}$ of the free associative unital $R$ -algebra on $g_i,h_i,e_i$ for $1\le i<n$ , with additional symbols $X,T$ precisely when $\mathrm{aff}=\mathrm{true}$ and $n\ge1$ , subject to

\begin{gathered} g_ih_i=h_ig_i=1,\qquad e_i^2=\delta e_i,\qquad g_i-h_i=z(e_i-1),\qquad g_ie_i=e_ig_i=\lambda^{-1}e_i,\\ g_ig_{i+1}g_i=g_{i+1}g_ig_{i+1} \quad(1\le i,\ i+1<n),\\ g_ig_j=g_jg_i,\qquad g_ie_j=e_jg_i,\qquad e_ie_j=e_je_i \quad(1\le i,j<n,\ i+1<j\text{ or }j+1<i),\\ e_ie_je_i=e_i,\qquad g_ig_je_i=e_je_i,\qquad e_ig_jg_i=e_ie_j,\qquad e_ig_je_i=\lambda e_i \quad(1\le i,j<n,\ i+1=j\text{ or }j+1=i). \end{gathered}

In the affine case there are also the relations

\begin{gathered} XT=TX=1\quad(n\ge1),\\ Xg_1Xg_1=g_1Xg_1X,\qquad e_1X^s e_1=q(s)e_1\quad(s\ge1),\qquad e_1Xg_1X=Xg_1Xe_1=\lambda^{-1}e_1 \quad(n\ge2),\\ Xg_j=g_jX,\qquad Xe_j=e_jX\quad(2\le j<n). \end{gathered}

Here $g_i$ is the image of the crossing symbol with Boolean argument false, $h_i$ is the image of the crossing symbol with Boolean argument true, and $e_i$ is the image of the contraction symbol; unavailable generator expressions are $0$ , and scalar coefficients mean their images under the canonical map from $R$ . For every $i\in\mathbb N$ satisfying $1\le i<n$ , both identities hold:

g_i^2=1+(\lambda^{-1}z)e_i-zg_i, \qquad h_i^2=1-(\lambda z)e_i+zh_i.

The index hypothesis forces $n\ge2$ , so there is no admissible $i$ when $n=0$ or $n=1$ .

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph