LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Artin positive word reversing is complete

Statement

Let $n \geq 2$ and let $Θ$ be the total right complement of Artin right complements and word reversing, with $\equiv^{+}$ the congruence of Positive braid monoid and $ℓ$ the length of Positive artin relations preserve homogeneous length. Then, for all positive words $u, v$ :

(a) Coherence of the recursion. Wherever the values exist, $Θ (u, v_{1} v_{2}) = Θ (u, v_{1}) Θ (Θ (v_{1}, u), v_{2})$ for all positive words $u, v_{1}, v_{2}$ . Consequently $Θ$ is the unique minimal extension $θ^{*}$ of $θ$ of the source, it satisfies all the recursion rules of the source, and its values depend only on the pair of words, so that "the right complement of $v$ over $u$ " is a well-defined word whenever it exists. ( $Θ$ is by construction a partial map: $Θ (u, v)$ is defined exactly when the reversing of $u^{- 1} v$ terminates. For the Artin presentation it is in fact total, because every pair of positive words admits a common right multiple; that is noted below and proved in Every positive braid divides a power of the half twist on both sides.)

(b) Complement common multiples. If $Θ (u, v)$ is defined then $u Θ (u, v) \equiv^{+} v Θ (v, u)$ ; in particular, if $Θ (u, v) = Θ (v, u) = ε$ , then $u \equiv^{+} v$ in $B_{n}^{+}$ .

(c) Completeness and the equality criterion. $u \equiv^{+} v$ if and only if the reversing of $u^{- 1} v$ terminates in the empty path, equivalently if and only if $Θ (u, v)$ and $Θ (v, u)$ are defined and both empty. Equivalently, right-reversing is complete for the Artin presentation.

(d) Left cancellativity. If $x u = x v$ in $B_{n}^{+}$ then $u = v$ ; that is, $B_{n}^{+}$ is left-cancellative.

(e) Conditional right-lcms. If $[u]$ and $[v]$ admit a common right multiple in $B_{n}^{+}$ (equivalently, if $Θ (u, v)$ is defined), then $[u Θ (u, v)]$ is their least common right multiple; consequently any two elements of $B_{n}^{+}$ that admit a common right multiple admit a unique right-lcm. Moreover $Θ (u, v) = ε$ if and only if $[u] = [v] c$ for some $c \in B_{n}^{+}$ .

For a pair with a common right multiple, the criterion and complement are effective: the conditional-lcm assertion below guarantees that right-reversing terminates, and a fixed rule such as reversing the leftmost negative--positive pair computes its terminal form in finitely many steps. The later explicit $Δ$ -power construction makes every pair satisfy this hypothesis and thus turns (c) into an unconditional decision test. No choice principle is used.

Facts & Assumptions

Given: A natural number $n \geq 2$ , the alphabet $Σ_{n}$ , the right complement $Θ$ , the congruence $\equiv^{+}$ and the length $ℓ$ .

[F1]

$Θ (ε, v) = v$ , $Θ (u, ε) = ε$ , $Θ (s u^{'}, v) = Θ (u^{'}, Θ (s, v))$ , and $Θ (s, t v) = θ (s, t) Θ (θ (t, s), v)$ , where $θ (σ_{i}, σ_{j})$ is $ε$ for $i = j$ , $σ_{j} σ_{i}$ for $∣ i - j ∣ = 1$ , and $σ_{j}$ for $∣ i - j ∣ \geq 2$ ; for letters $s \neq t$ , $s θ (s, t)$ and $t θ (t, s)$ are the two sides of a defining pair of the presentation, so $[s θ (s, t)] = [t θ (t, s)]$ (Artin right complements and word reversing).

[F2]

$\equiv^{+}$ is the smallest congruence on $Σ_{n}^{*}$ containing the braid pairs and the commutation pairs; $B_{n}^{+} = Σ_{n}^{*} / ⁣ \equiv^{+}$ , and $u \equiv^{+} v$ implies $∣ u ∣ = ∣ v ∣$ (Positive braid monoid, Positive artin relations preserve homogeneous length).

[L3]

$ℓ ⁣ : B_{n}^{+} \to N$ is a monoid homomorphism, $ℓ (x) = 0$ only for $x = 1$ , and $ℓ$ takes only the values $0, \dots, k$ on the classes of words of length $k$ ; a surjection from a finite set onto a set makes the target finite with no more elements (Positive artin relations preserve homogeneous length).

[L4]

The $θ$ -cube condition holds for every triple of letters: $Θ_{3} (x, y, z) : = Θ (Θ (x, y), Θ (x, z))$ and $Θ_{3} (y, x, z)$ are $\equiv^{+}$ -equivalent for all letters $x, y, z$ ; in the three consecutive cases the values are $σ_{i + 2} σ_{i + 1} σ_{i}$ , $σ_{i} σ_{i + 1} σ_{i + 2}$ and the pair $σ_{i + 1} σ_{i} σ_{i + 2} σ_{i + 1} \equiv^{+} σ_{i + 1} σ_{i + 2} σ_{i} σ_{i + 1}$ (Artin right complements satisfy the cube condition).

[L5]

Induction on the natural numbers (The principle of mathematical induction); consequently a partial map defined by a recursion whose every recursive call has strictly smaller value of a natural-valued measure is well defined, by induction on that measure.

[L6]

A rewriting relation $\to$ is confluent below a set $T$ if every two maximal $\to$ -sequences starting from a common element either both terminate in the same element of $T$ or both fail to terminate; and a relation containing no infinite sequence has every maximal sequence finite.

[L7]

Right-complemented presentations have well-defined complements (source's Lemma 4.32, printed pp. 73--74). If a category presentation is right-complemented, associated with the syntactic right complement $θ$ , then: (i) for all paths $u, v$ there exists at most one pair of paths $(u^{'}, v^{'})$ with $u^{- 1} v ⇝ v^{'} (u^{'})^{- 1}$ ; (ii) defining $θ^{*} (u, v) : = v^{'}$ when that pair exists, $θ^{*}$ is a partial map extending $θ$ , it satisfies the four rules $θ^{*} (s, s) = ε$ , $θ^{*} (u_{1} u_{2}, v) = θ^{*} (u_{2}, θ^{*} (u_{1}, v))$ , $θ^{*} (u, v_{1} v_{2}) = θ^{*} (u, v_{1}) θ^{*} (θ^{*} (v_{1}, u), v_{2})$ , $θ^{*} (ε, u) = u$ , $θ^{*} (u, ε) = ε$ , and it is the least extension of $θ$ satisfying those rules. The presentation of $B_{n}^{+}$ by $Σ_{n}$ and $R_{n}$ is right-complemented, associated with the syntactic right complement $θ$ of Artin right complements and word reversing; this is checked letter by letter there (equal letters give the common word $s$ , and distinct letters give the unique defining pair of $R_{n}$ beginning with each). Hence (i) and (ii) apply to the Artin presentation, and the map $Θ$ of that definition is $θ^{*}$ ; in particular the terminal pair of any successful reversing of $u^{- 1} v$ is $Θ (u, v) (Θ (v, u))^{- 1}$ . [L7]

[L8]

Noetherianity witnesses (source's Definition II.2.31(ii), Proposition II.2.32, printed pp. 47--48). A right-Noetherianity witness for a presentation $(S, R)$ is a map $λ^{*}$ from $S$ -paths to ordinals that is invariant under $\equiv^{+}$ and satisfies $λ^{*} (w) \leq λ^{*} (s w)$ for all letters $s$ and words $w$ , the inequality being strict whenever the class of $s$ is not invertible in $⟨ S ∣ R ⟩^{+}$ . Every homogeneous presentation admits the $N$ -valued witness $λ^{*} (w) : = ∣ w ∣$ : length is $\equiv^{+}$ -invariant because relations preserve length [F2], and $∣ w ∣ < ∣ s w ∣$ for every letter $s$ ; strictness is automatic, and it is consistent with [L3], since no letter of $Σ_{n}$ is invertible in $B_{n}^{+}$ . [L3]

[L9]

The $θ$ -cube condition implies the cube condition (source's Lemma 4.55, printed p. 80). If a presentation is associated with a syntactic right complement $θ$ and the $θ$ -cube condition is true on a set of paths, then the cube condition (4.49) of the source is true on that set. Together with [L4] this gives the cube condition for every triple of letters. [L4]

[L10]

Reversing implies equivalence (source's Proposition 4.34 and formula (4.35), printed pp. 74, 90--91). If $u^{- 1} v ⇝ v^{'} (u^{'})^{- 1}$ for positive words $u, v, u^{'}, v^{'}$ , then $u v^{'} \equiv^{+} v u^{'}$ ; in particular $u^{- 1} v ⇝ ε$ implies $u \equiv^{+} v$ . [F2]

Proof

technique · direct

1.1

All four recursion rules hold, including the coherence claimed in (a). The presentation of $B_{n}^{+}$ is right-complemented with syntactic right complement $θ$ , as verified letter by letter in Artin right complements and word reversing, so L7 applies to it: the map $Θ$ of that definition is the least extension $θ^{*}$ of $θ$ satisfying the four rules, and by L7 there is at most one pair of blocks to which a pair of positive words can be reversed, so $Θ$ is well defined where it is defined and the terminal pair of any successful reversing of $u^{- 1} v$ is $Θ (u, v) (Θ (v, u))^{- 1}$ — an identification used at the end of the proof. Of the four rules, $Θ (ε, v) = v$ and $Θ (u, ε) = ε$ are the two empty-word clauses of L7, and $Θ (s u^{'}, v) = Θ (u^{'}, Θ (s, v))$ is the first-argument rule of [F1]; the remaining rule, $Θ (u, v_{1} v_{2}) = Θ (u, v_{1}) Θ (Θ (v_{1}, u), v_{2})$ , is the second-argument rule and is exactly claim (a). So (a) holds for all positive words $u, v_{1}, v_{2}$ and every rule of [F1] may be used below.

F1L7

1.2

Repeated-entry triples. For all letters $x, y, z$ : if $x = y$ the two words $Θ_{3} (x, y, z)$ and $Θ_{3} (y, x, z)$ are identical; if $x = z$ both are $ε$ ; if $y = z$ the first is $Θ (Θ (x, y), Θ (x, y)) = ε$ and the second is $Θ (Θ (y, x), Θ (y, y)) = ε$ . This is recorded for later use in the distance induction.

F1L4

1.3

Complement common multiples (b). Assume $Θ (u, v)$ is defined. Then by the definition of $Θ$ and L7, the reversing of $u^{- 1} v$ terminates in the pair of blocks $Θ (u, v) (Θ (v, u))^{- 1}$ , so $u^{- 1} v ⇝ Θ (u, v) (Θ (v, u))^{- 1}$ ; [L10] then gives $u Θ (u, v) \equiv^{+} v Θ (v, u)$ , which is (b). In particular if both complements are empty, $u \equiv^{+} v$ .

L7L10

1.4

The reversing formalism. A signed path is a finite word with signed letters; right-reversing replaces a negative-positive subpath $s^{- 1} t$ by $v u^{- 1}$ when $s v = t u$ is a defining relation, and deletes $s^{- 1} s$ ; a step with $s \neq t$ replaces two letters by the $∣ θ (s, t) ∣ + ∣ θ (t, s) ∣ \geq 2$ letters of the new blocks, while the step with $s = t$ removes two letters, so along a terminating sequence the length changes by a finite sum of such terms. Equivalence in $B_{n}^{+}$ is detected by reversing, in the sense of the source's completeness criterion for $ε$ -free presentations: because the presentation contains no $ε$ -relation, reversing is complete if and only if $u \equiv^{+} v$ implies that the path $u^{- 1} v$ reverses to the empty path. The combinatorial distance $d (u, v)$ between two $\equiv^{+}$ -related paths is the least number of single relation applications transforming one into the other; it is a natural number by the definition of $\equiv^{+}$ .

F1F2given

1.5

Elementary compatibility. (i) If $s \neq t$ are letters, then $s^{- 1} t ⇝ θ (s, t) θ (t, s)^{- 1}$ by the defining relation $s θ (s, t) = t θ (t, s)$ ; for $s = t$ , $s^{- 1} s ⇝ ε$ . (ii) A reversing step at a subpath remains valid when the same signed context is placed on both sides; thus $x ⇝ x^{'}$ implies $a x b ⇝ a x^{'} b$ , and a second step $y ⇝ y^{'}$ in a disjoint subpath gives $x^{'} y ⇝ x^{'} y^{'}$ . Finite reversing sequences concatenate. (iii) The positive-word length $λ^{*} (w) : = ∣ w ∣$ satisfies $λ^{*} (w) < λ^{*} (s w)$ for every positive letter $s$ , and it is $\equiv^{+}$ -invariant because relations preserve length [F2]. Moreover no letter $s$ is invertible in $B_{n}^{+}$ : if $[s] x = 1$ for some $x$ , then applying the monoid homomorphism $ℓ$ to both sides gives $1 + ℓ (x) = 0$ in $N$ , which is impossible. So the strictness clause of [L8] holds and the length is a right-Noetherianity witness.

F1F2L3L8

1.6

Inner induction on the total length. For natural $ℓ^{'}$ let $E_{α, ℓ^{'}}$ be $E_{α}$ restricted to quadruples with $∣ \hat{u} ∣ + ∣ \hat{v} ∣ \leq ℓ^{'}$ . $E_{α, 1}$ holds: if $\hat{u}$ is empty, the choices $a = ε$ , $b = \hat{v}$ , $c = \overset{ˇ}{u}$ witness factorability, and symmetrically for $\hat{v}$ empty.

1.7

The length-two case, third induction on the distance. Assume $∣ \hat{u} ∣ = ∣ \hat{v} ∣ = 1$ , so $\hat{u}, \hat{v}$ are letters $s, t$ . Let $E_{α, 2, d}$ be $E_{α, 2}$ restricted to quadruples with combinatorial distance $d (\hat{u} \overset{ˇ}{v}, \hat{v} \overset{ˇ}{u}) \leq d$ . $E_{α, 2, 0}$ holds: then $\hat{u} = \hat{v}$ and $\overset{ˇ}{u} \equiv^{+} \overset{ˇ}{v}$ , and $a = b = ε$ , $c = \overset{ˇ}{u}$ witness factorability. $E_{α, 2, 1}$ holds: if the single relation step does not involve the first letter, then $\hat{u} = \hat{v}$ and the previous witness applies; otherwise the first letters of the two paths satisfy $\hat{u} v^{'} = \hat{v} u^{'}$ for a relation of the presentation, and $a = u^{'}$ , $b = v^{'}$ , $c$ the common remainder witness factorability.

F1L4L5

2.1

Empty complements and the equality test (c), forward direction. If $Θ (u, v) = Θ (v, u) = ε$ and $Θ$ is defined on the pair, then $u \equiv^{+} v$ by step 1.3. Conversely, if $u \equiv^{+} v$ , then $∣ u ∣ = ∣ v ∣$ by [F2] and the completeness proved below supplies a reversing of $u^{- 1} v$ to the empty path, so that $Θ (u, v)$ and $Θ (v, u)$ are defined and empty; this is the equivalence asserted in (c), completed later in the proof.

F2L6step 1.3

2.2

The Appendix lemma, outer induction. Let $λ^{*}$ be the length function $λ^{*} (w) = ∣ w ∣$ , which by [L8] and step 1.5(iii) is an $N$ -valued right-Noetherianity witness for the Artin presentation; let $α \in N$ and let $E_{α}$ be: every quadruple $(\hat{u}, \hat{v}, \overset{ˇ}{u}, \overset{ˇ}{v})$ of paths with $\hat{u} \overset{ˇ}{v} \equiv^{+} \hat{v} \overset{ˇ}{u}$ and $λ^{*} (\hat{u} \overset{ˇ}{v}) \leq α$ is reversing-factorable, meaning that there are positive paths $a, b, c$ with $(\hat{u})^{- 1} \hat{v} ⇝ b a^{- 1}$ , $\overset{ˇ}{u} \equiv^{+} a c$ , $\overset{ˇ}{v} \equiv^{+} b c$ . Hats and checks are variable labels, not signs; $u^{- 1}$ is the signed inverse word (reverse order, negative letters). We prove $E_{α}$ for every natural $α$ by induction on $α$ using [L5], assuming $E_{β}$ for all $β < α$ .

F1L3L5L8

2.3

The distance induction, main step. Assume $d \geq 2$ and $E_{α, 2, d^{'}}$ for $d^{'} < d$ , and let $(\hat{u}, \hat{v}, \overset{ˇ}{u}, \overset{ˇ}{v})$ with $\hat{u} \overset{ˇ}{v} \equiv^{+} \hat{v} \overset{ˇ}{u}$ , $λ^{*} (\hat{u} \overset{ˇ}{v}) \leq α$ , $∣ \hat{u} ∣ = ∣ \hat{v} ∣ = 1$ and distance $d$ . Choose an intermediate path $w \hat{w}$ of a derivation from $\hat{u} \overset{ˇ}{v}$ to $\hat{v} \overset{ˇ}{u}$ , with $w$ its first letter; then $\hat{u} \overset{ˇ}{v} \equiv^{+} w \hat{w} \equiv^{+} \hat{v} \overset{ˇ}{u}$ , and both distances to $w \hat{w}$ are $< d$ . By $E_{α, 2, d - 1}$ applied to the quadruples $(\hat{u}, w, \hat{w}, \overset{ˇ}{v})$ and $(w, \hat{v}, \overset{ˇ}{u}, \hat{w})$ — legitimate because $∣ \hat{u} ∣ = ∣ w ∣ = 1$ , $∣ w ∣ + ∣ \hat{v} ∣ = 2$ , and the distances and $λ^{*}$ -values are within range — there are paths $u_{0}, v_{0}, u_{1}, v_{1}, {\overset{ˇ}{u}}_{0}, {\overset{ˇ}{v}}_{0}$ with $(\hat{u})^{- 1} w ⇝ v_{1} (u_{0})^{- 1}, \overset{ˇ}{v} \equiv^{+} v_{1} {\overset{ˇ}{v}}_{0}, \hat{w} \equiv^{+} u_{0} {\overset{ˇ}{v}}_{0}, w^{- 1} \hat{v} ⇝ v_{0} (u_{1})^{- 1}, \overset{ˇ}{u} \equiv^{+} u_{1} {\overset{ˇ}{u}}_{0}, \hat{w} \equiv^{+} v_{0} {\overset{ˇ}{u}}_{0} .$ Hence $u_{0} {\overset{ˇ}{v}}_{0} \equiv^{+} \hat{w} \equiv^{+} v_{0} {\overset{ˇ}{u}}_{0}$ , and $λ^{*} (u_{0} {\overset{ˇ}{v}}_{0}) = λ^{*} (\hat{w}) < λ^{*} (w \hat{w}) \leq α$ by the strict increase of step 1.5(iii) at the non-invertible letter $w$ ; so the outer induction hypothesis $E_{β}$ at $β : = λ^{*} (u_{0} {\overset{ˇ}{v}}_{0}) < α$ applies, giving paths $u_{0}^{'}, v_{0}^{'}, w_{0}^{'}$ with $(u_{0})^{- 1} v_{0} ⇝ v_{0}^{'} (u_{0}^{'})^{- 1}, {\overset{ˇ}{u}}_{0} \equiv^{+} u_{0}^{'} w_{0}^{'}, {\overset{ˇ}{v}}_{0} \equiv^{+} v_{0}^{'} w_{0}^{'} .$ Concatenating the first reversings at their signed boundaries gives $(\hat{u})^{- 1} w w^{- 1} \hat{v} ⇝ v_{1} (u_{0})^{- 1} v_{0} (u_{1})^{- 1} ⇝ v_{1} v_{0}^{'} (u_{1} u_{0}^{'})^{- 1}$ . The middle $w w^{- 1}$ is a signed inverse pair, not a positive word relation. Since the $θ$ -cube condition holds for the triple $(\hat{u}, \hat{v}, w)$ of letters — [L4] for distinct letters, the repeated-entry cases being the computation in step 1.2 — [L9] yields the cube condition of the source for that triple, so there are paths $u^{'}, v^{'}, w_{1}$ with $(\hat{u})^{- 1} \hat{v} ⇝ v^{'} (u^{'})^{- 1}, u_{1} u_{0}^{'} \equiv^{+} u^{'} w_{1}, v_{1} v_{0}^{'} \equiv^{+} v^{'} w_{1} .$ Setting $w^{'} = w_{1} w_{0}^{'}$ gives $\overset{ˇ}{u} \equiv^{+} u_{1} u_{0}^{'} w_{0}^{'} \equiv^{+} u^{'} w^{'}$ and $\overset{ˇ}{v} \equiv^{+} v_{1} v_{0}^{'} w_{0}^{'} \equiv^{+} v^{'} w^{'}$ , so $(\hat{u}, \hat{v}, \overset{ˇ}{u}, \overset{ˇ}{v})$ is factorable. Hence $E_{α, 2, d}$ holds for all $d$ , and therefore $E_{α, 2}$ .

F1L3L4L7L9step 1.2step 1.5step 1.7

3.1

Inner induction on the total length, main step. Let $ℓ^{'} \geq 3$ and assume $E_{α, ℓ^{''}}$ for $ℓ^{''} < ℓ^{'}$ . Let $(\hat{u}, \hat{v}, \overset{ˇ}{u}, \overset{ˇ}{v})$ satisfy the hypotheses with $∣ \hat{u} ∣ + ∣ \hat{v} ∣ = ℓ^{'}$ , so one of $\hat{u}, \hat{v}$ has length at least two; say $\hat{v} = v_{1} v_{2}$ with both factors nonempty. Then $\hat{u} \overset{ˇ}{v} \equiv^{+} v_{1} (v_{2} \overset{ˇ}{u})$ with $∣ \hat{u} ∣ + ∣ v_{1} ∣ < ℓ^{'}$ , so $E_{α, ℓ^{''}}$ with $ℓ^{''} = ∣ \hat{u} ∣ + ∣ v_{1} ∣$ gives paths $u_{1}^{'}, v_{1}^{'}, w_{1}^{'}$ with $(\hat{u})^{- 1} v_{1} ⇝ v_{1}^{'} (u_{1}^{'})^{- 1}, v_{2} \overset{ˇ}{u} \equiv^{+} u_{1}^{'} w_{1}^{'}, \overset{ˇ}{v} \equiv^{+} v_{1}^{'} w_{1}^{'} .$ Here $λ^{*} (v_{2} \overset{ˇ}{u}) < λ^{*} (v_{1} v_{2} \overset{ˇ}{u}) \leq α$ by step 1.5(iii) at the non-invertible letter(s) of $v_{1}$ , so the outer induction hypothesis $E_{β}$ at $β : = λ^{*} (v_{2} \overset{ˇ}{u}) < α$ applies to the quadruple $(u_{1}^{'}, v_{2}, \overset{ˇ}{u}, w_{1}^{'})$ — legitimate since $u_{1}^{'} w_{1}^{'} \equiv^{+} v_{2} \overset{ˇ}{u}$ — giving paths $u^{'}, v_{2}^{'}, w^{'}$ with $(u_{1}^{'})^{- 1} v_{2} ⇝ v_{2}^{'} (u^{'})^{- 1}, \overset{ˇ}{u} \equiv^{+} u^{'} w^{'}, w_{1}^{'} \equiv^{+} v_{2}^{'} w^{'} .$ Setting $v^{'} = v_{1}^{'} v_{2}^{'}$ and concatenating reversings gives $(\hat{u})^{- 1} \hat{v} = (\hat{u})^{- 1} v_{1} v_{2} ⇝ v_{1}^{'} (u_{1}^{'})^{- 1} v_{2} ⇝ v_{1}^{'} v_{2}^{'} (u^{'})^{- 1} = v^{'} (u^{'})^{- 1}$ and $\overset{ˇ}{v} \equiv^{+} v_{1}^{'} w_{1}^{'} \equiv^{+} v_{1}^{'} v_{2}^{'} w^{'} = v^{'} w^{'}$ , so the quadruple is factorable. The other case, in which $∣ \hat{u} ∣ \geq 2$ , is not a symmetry shortcut: write $\hat{u} = u_{1} u_{2}$ with both factors nonempty. Apply the inner hypothesis to $(u_{1}, \hat{v}, \overset{ˇ}{u}, u_{2} \overset{ˇ}{v})$ , since $u_{1} (u_{2} \overset{ˇ}{v}) \equiv^{+} \hat{v} \overset{ˇ}{u}$ and $∣ u_{1} ∣ + ∣ \hat{v} ∣ < ℓ^{'}$ . It gives $(u_{1})^{- 1} \hat{v} ⇝ v_{1}^{'} (u_{1}^{'})^{- 1}$ , $\overset{ˇ}{u} \equiv^{+} u_{1}^{'} w_{1}^{'}$ and $u_{2} \overset{ˇ}{v} \equiv^{+} v_{1}^{'} w_{1}^{'}$ . Since $∣ u_{2} \overset{ˇ}{v} ∣ = ∣ \hat{u} \overset{ˇ}{v} ∣ - ∣ u_{1} ∣ < α$ , the outer hypothesis applies to $(u_{2}, v_{1}^{'}, w_{1}^{'}, \overset{ˇ}{v})$ and gives $(u_{2})^{- 1} v_{1}^{'} ⇝ v_{2}^{'} (u_{2}^{'})^{- 1}$ , $w_{1}^{'} \equiv^{+} u_{2}^{'} w^{'}$ and $\overset{ˇ}{v} \equiv^{+} v_{2}^{'} w^{'}$ . Thus $(\hat{u})^{- 1} \hat{v} = (u_{2})^{- 1} (u_{1})^{- 1} \hat{v} ⇝ (u_{2})^{- 1} v_{1}^{'} (u_{1}^{'})^{- 1} ⇝ v_{2}^{'} (u_{2}^{'})^{- 1} (u_{1}^{'})^{- 1} = v_{2}^{'} (u_{1}^{'} u_{2}^{'})^{- 1}$ , while $\overset{ˇ}{u} \equiv^{+} u_{1}^{'} u_{2}^{'} w^{'}$ and $\overset{ˇ}{v} \equiv^{+} v_{2}^{'} w^{'}$ . So this quadruple is factorable too, and $E_{α, ℓ^{'}}$ holds.

L3L5L8step 1.5step 2.2

4.1

The Appendix lemma. Steps 2.2, 1.6, 1.7, 2.3 and 3.1 prove $E_{α, ℓ^{'}}$ for all $α, ℓ^{'}$ by the outer induction on $α$ , the inner induction on $ℓ^{'}$ , and the third induction on derivation distance. Hence every quadruple $(\hat{u}, \hat{v}, \overset{ˇ}{u}, \overset{ˇ}{v})$ with $\hat{u} \overset{ˇ}{v} \equiv^{+} \hat{v} \overset{ˇ}{u}$ is reversing-factorable: right-reversing is complete for the Artin presentation, which is the completeness proposition of the source in the homogeneous, $ε$ -free case.

step 2.2step 1.6step 1.7step 2.3step 3.1

5.1

The left-cancellativity consequence. Since the presentation contains no relation $s u = s v$ — both sides of every defining pair begin with different letters when the two sides are distinct, and the equal-letter case is trivial — the source's left-cancellativity corollary applies: $B_{n}^{+}$ is left-cancellative. Indeed, if $s u \equiv^{+} s v$ for a letter $s$ , completeness gives a factorization of $(s, s, u, v)$ , and by right-complementedness the signed pair $s^{- 1} s$ deletes, so $u \equiv^{+} v$ ; iterating, $x u = x v$ implies $u = v$ for every $x$ by the universal property of $\equiv^{+}$ and induction on the length of a representative of $x$ . This is (d).

F1F2step 4.1L5

5.2

The conditional-lcm corollary. For all paths $u, v$ : the elements $[u], [v]$ admit a common right multiple if and only if $u^{- 1} v$ reverses to some terminal pair $v^{'} (u^{'})^{- 1}$ , and then $[u v^{'}]$ is their right-lcm. Indeed, if $h$ is a common right multiple, completeness factorizes $(u, v, \overset{ˇ}{u}, \overset{ˇ}{v})$ with $u \overset{ˇ}{v} \equiv^{+} v \overset{ˇ}{u}$ , giving $u^{- 1} v \to v^{'} (u^{'})^{- 1}$ and $[h]$ a right multiple of $[u v^{'}]$ ; conversely a reversing $u^{- 1} v \to v^{'} (u^{'})^{- 1}$ gives $u v^{'} \equiv^{+} v u^{'}$ and hence a common right multiple. Leastness holds because in a right-complemented presentation the terminal pair is unique when it exists: the maximal right-reversing diagram from a given initial path is unique, as recorded in L7, so the pair $(v^{'}, u^{'})$ — and hence the element $[u v^{'}]$ — does not depend on the order in which the steps are enumerated.

F1L7step 4.1

6.1

The complements compute the reversing, and (a),(c),(e) follow. By step 1.1 the recursion of [F1] is the square-filling computation, so the terminal pair of the reversing of $u^{- 1} v$ is $Θ (u, v) (Θ (v, u))^{- 1}$ (the well-definedness lemma [L7]); this identification is the bridge used in the following three consequences. First, (c): if $u \equiv^{+} v$ then by [L6] and the completeness criterion recalled in step 1.4 the path $u^{- 1} v$ reverses to the empty path, so $Θ (u, v)$ and $Θ (v, u)$ are defined and both $ε$ ; conversely step 2.1 gives $u \equiv^{+} v$ from empty complements. Second, (e): if $[u], [v]$ admit a common right multiple then by step 5.2 the pair $u^{- 1} v$ reverses to a terminal pair $v^{'} (u^{'})^{- 1}$ with $[u v^{'}]$ the right-lcm, and by the identification $v^{'} = Θ (u, v)$ , giving $[u Θ (u, v)]$ as the right-lcm; and $Θ (u, v) = ε$ holds exactly when $[u] = [v] Θ (v, u)$ , which together with step 2.1 and the additivity of $ℓ$ shows the second assertion of (e). Third, (a) and (b) are steps 1.1 and 1.3.

F1L3L6L7step 1.1step 1.3step 2.1step 5.1step 5.2

7.1

End. Parts (a),(b),(c),(d),(e) are steps 1.1 and 1.3 (with step 6.1 for the forward direction of (c)), step 2.1 with step 6.1, step 5.1 and step 6.1. The effective operation here is conditional: if a common right multiple exists, step 5.2 proves that the deterministic leftmost reversing procedure terminates and computes $Θ$ . In this Artin presentation, the later explicit common- $Δ$ -power construction supplies that hypothesis for every pair, making the procedure total. No bound by the total input-word length is asserted; no step uses a choice principle. ∎

step 1.3step 2.1step 5.1step 6.1

Remarks

Source dependence. Three facts are taken from the source, with their hypotheses verified, and are recorded in Facts & Assumptions: the well-definedness of the complements and the coherence of the two evaluation orders ([L7], the source's Lemma 4.32, established there by the square-filling grid argument); the right-Noetherianity witness supplied by homogeneity ([L8], the source's Definition II.2.31(ii) and Proposition II.2.32, whose hypothesis "every relation preserves length" is [F2]); and the $θ$ -cube/cube link ([L9], the source's Lemma 4.55). Everything else is re-derived here: the $θ$ -cube condition itself (Artin right complements satisfy the cube condition), the whole nested induction of Appendix Lemma II.4.62 (steps 4.1--6.1), the left-cancellativity deduction (Corollary 4.45) and the conditional-lcm deduction (Corollary 4.47). The specific complements used on this page and on the companion examples page are recomputed from the recursion in Artin right complements and word reversing and in the items below.
The hypothesis "right-Noetherian" is met by the length function $λ^{*} (w) = ∣ w ∣$ because the presentation is homogeneous, and no $ε$ -relation occurs, so the source's case (4.53) of Proposition 4.51 is the one used. The sharp cube condition, which the source records as failing for $n \geq 4$ , is never used.
The completeness argument is the only place on this page where the reversing machinery is needed at full strength: everything else (atom complements, $Δ$ -divisibility, the normal form) is a finite computation with the recursion and with the criterion of (c).
Source numbering used above. The descriptive names in the proof correspond to the source as follows: "the Appendix lemma" is Lemma II.4.62 of the Appendix (with its inner sub-lemmas II.4.60--II.4.63); "the completeness proposition in the homogeneous, $ε$ -free case" is Proposition 4.51 in case (4.53); "the left-cancellativity corollary" is Corollary 4.45; "the conditional-lcm corollary" is Corollary 4.47; "the completeness criterion for $ε$ -free presentations" is Lemma 4.42; and "the well-definedness lemma" is Lemma 4.32. The numbers are kept out of the numbered steps on purpose, so that a source numbering such as 4.62 cannot be mistaken for a proof step of this item.

Depends on

Used by

Cited to discharge well-definedness by Artin right complements and word reversing.

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Patrick Dehornoy et al., Foundations of Garside Theory, Chapter II, Lemma 4.6, Proposition 4.16, Definition 4.48, Lemma 4.55, Proposition 4.51, printed pp. 63-68, 78-83 (standard reference, not scraped)
Patrick Dehornoy et al., Foundations of Garside Theory, Appendix, Lemmas II.4.60-II.4.63, printed pp. 657-662, and Chapter II, Corollaries 4.45 and 4.47, printed pp. 79-80 (standard reference, not scraped)