ExampleConstruction: Literature-sourcedVerification: 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.

A left garside normal form computation in b three

Example

Take $n = 3$ , so that $B_{3}$ has the two generators $σ_{1}, σ_{2}$ , the positive monoid $B_{3}^{+}$ has the two atoms $σ_{1}, σ_{2}$ , and the half twist is

$Δ = T_{1} T_{2} = σ_{1} (σ_{2} σ_{1}) = σ_{1} σ_{2} σ_{1},$

of length $N = 1 + 2 = 3$ . Let $x : = σ_{1}^{- 1} σ_{2} \in B_{3}$ . The example computes the left Garside normal form of $x$ of Left garside normal form is unique and checks:

$σ_{1}^{- 1} = Δ^{- 1} σ_{1} σ_{2}$ , hence $x = Δ^{- 1} σ_{1} σ_{2}^{2}$ with $σ_{1} σ_{2}^{2} \in B_{3}^{+}$ ;
$Δ \land_{L} σ_{1} σ_{2}^{2} = σ_{1} σ_{2}$ , so in particular $Δ ̸ ≼_{L} σ_{1} σ_{2}^{2}$ ;
the left normal form of $x$ is $x = Δ^{- 1} \cdot (σ_{1} σ_{2}) \cdot σ_{2},$ that is $p (x) = - 1$ , $A (x) = σ_{1} σ_{2}^{2}$ and the two factors $a_{1} = σ_{1} σ_{2}$ , $a_{2} = σ_{2}$ are proper simple braids with $π (a_{1}) = s_{1} s_{2}$ , $π (a_{2}) = s_{2}$ ;
the factor pair is left weighted: $(a_{1} a_{2}) \land_{L} Δ = a_{1}$ ;
consequently $x \notin B_{3}^{+}$ , in agreement with $p (x) = - 1 < 0$ .

Facts & Assumptions

Given: The natural number $3$ ; the braid group $B_{3} = ⟨ σ_{1}, σ_{2} ∣ σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2} ⟩$ of The braid group by Artin presentation; its positive monoid $B_{3}^{+}$ with atoms $σ_{1}, σ_{2}$ and length $ℓ$ ; the half twist $Δ = σ_{1} σ_{2} σ_{1} \in B_{3}^{+}$ of length $3$ ; and the element $x : = σ_{1}^{- 1} σ_{2} \in B_{3}$ .

[F1]

$B_{3}^{+}$ is generated by the atoms, $ℓ ([w]) = ∣ w ∣$ is additive, $ℓ (z) = 0$ forces $z = 1$ , and the braid relation gives $σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2}$ , so both triangular words for $Δ$ agree: $Δ = σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2}$ (Positive braid monoid, Positive artin relations preserve homogeneous length, The Garside half twist and simple positive braids).

[F2]

$a ≼_{L} b$ means $b = a c$ for some $c \in B_{3}^{+}$ , and then $ℓ (a) \leq ℓ (b)$ ; a left divisor of an atom has length $0$ or $1$ , so the left divisors of $σ_{1}$ are among $1, σ_{1}$ and those of $σ_{2}$ among $1, σ_{2}$ (Left and right divisibility for positive braids, Positive artin relations preserve homogeneous length).

[F3]

$π ⁣ : B_{3}^{+} \to S_{3}$ is a monoid homomorphism with $π (σ_{i}) = s_{i}$ ; in the composition convention of The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition the adjacent transpositions $s_{1} = (1 2)$ and $s_{2} = (2 3)$ are distinct, so $σ_{1} \neq σ_{2}$ (Reduced adjacent-transposition words have well-defined positive lifts, The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition).

[F4]

$B_{3}^{+}$ is a submonoid of $B_{3}$ , and for $x \in B_{3}$ one has $1 ≼_{L} x$ if and only if $x \in B_{3}^{+}$ (The group of fractions of the positive braid monoid is the Artin braid group, Left and right divisibility extend to lattice orders on the braid group).

[F5]

Scaling identity. For $D, A, B \in B_{3}^{+}$ one has $D (A \land_{L} B) = (D A) \land_{L} (D B)$ , where the meet is the positive left-gcd (Left and right divisibility extend to lattice orders on the braid group).

[F6]

Every nonempty finite family in $B_{3}^{+}$ has a unique left-gcd and a unique left-lcm; in particular $Δ \land_{L} A$ exists for every $A \in B_{3}^{+}$ , and every common left divisor of $Δ$ and $A$ left-divides $Δ \land_{L} A$ (Positive braids have left and right gcds and lcms).

[F7]

Normal form. Every $x \in B_{3}$ has a unique expression $x = Δ^{p} a_{1} \dots a_{r}$ with $p \in Z$ , $r \in N$ , every $a_{i}$ a proper simple braid and $a_{i} = Δ \land_{L} (a_{i} \dots a_{r})$ ; in such an expression $p = p (x)$ is the largest $p$ with $Δ^{p} ≼_{L} x$ , the product $a_{1} \dots a_{r}$ equals $A (x) = Δ^{- p (x)} x$ , and $(p (x), A (x))$ is the unique pair with $x = Δ^{p} A$ , $A \in B_{3}^{+}$ and $Δ ̸ ≼_{L} A$ . Moreover $p (x) \geq 0$ if and only if $x \in B_{3}^{+}$ , and if $r \geq 2$ then $(a_{i} a_{i + 1}) \land_{L} Δ = a_{i}$ for $1 \leq i < r$ (Left garside normal form is unique).

Verification

technique · direct

1.1

The half twist and the rewriting of $σ_{1}^{- 1}$ . By [F1], $Δ = σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2}$ has length $3$ . In the group $B_{3}$ , in which $B_{3}^{+}$ sits as a submonoid by [F4], multiplying out gives $Δ^{- 1} σ_{1} σ_{2} = (σ_{1} σ_{2} σ_{1})^{- 1} σ_{1} σ_{2} = σ_{1}^{- 1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{1} σ_{2} = σ_{1}^{- 1} σ_{2}^{- 1} σ_{2} = σ_{1}^{- 1}$ , so $σ_{1}^{- 1} = Δ^{- 1} σ_{1} σ_{2}$ ; substituting this identity into the given element $x = σ_{1}^{- 1} σ_{2}$ gives $x = Δ^{- 1} σ_{1} σ_{2}^{2}$ , and $σ_{1} σ_{2}^{2} \in B_{3}^{+}$ because it is a product of atoms.

F1F4givenalgebra

1.2

The atoms are coprime. Let $d \in B_{3}^{+}$ be a common left divisor of $σ_{1}$ and $σ_{2}$ . By [F2] write $σ_{1} = d c$ with $c \in B_{3}^{+}$ ; additivity of $ℓ$ [F1] gives $ℓ (d) + ℓ (c) = 1$ . If $ℓ (d) = 0$ then $d = 1$ [F1]; if $ℓ (d) = 1$ then $ℓ (c) = 0$ , so $c = 1$ and $d = σ_{1}$ . Since $d$ also left-divides $σ_{2}$ , write $σ_{2} = d c^{'}$ with a possibly different suffix $c^{'}$ . Length gives $ℓ (c^{'}) = 0$ , hence $c^{'} = 1$ and $σ_{2} = d = σ_{1}$ , contradicting $π (σ_{2}) = s_{2} \neq s_{1} = π (σ_{1})$ [F3]. So the only common left divisor of the two atoms is $1$ , and by [F6] their left-gcd is $σ_{1} \land_{L} σ_{2} = 1$ .

F1F2F3F6

2.1

The meet with $σ_{1} σ_{2}^{2}$ . Apply the scaling identity [F5] to $D : = σ_{1} σ_{2}$ , $A : = σ_{1}$ and $B : = σ_{2}$ ; by [F1] the two products are $D A = σ_{1} σ_{2} σ_{1} = Δ$ and $D B = σ_{1} σ_{2} σ_{2} = σ_{1} σ_{2}^{2}$ , so $Δ \land_{L} σ_{1} σ_{2}^{2} = (σ_{1} σ_{2} σ_{1}) \land_{L} (σ_{1} σ_{2} σ_{2}) = (σ_{1} σ_{2}) (σ_{1} \land_{L} σ_{2}) = (σ_{1} σ_{2}) \cdot 1 = σ_{1} σ_{2}$ , the third equality by step 1.2. Hence $Δ ̸ ≼_{L} σ_{1} σ_{2}^{2}$ : if $Δ$ were a common left divisor of $Δ$ and $σ_{1} σ_{2}^{2}$ , then by [F6] it would satisfy $Δ ≼_{L} Δ \land_{L} σ_{1} σ_{2}^{2} = σ_{1} σ_{2}$ , and monotonicity of $ℓ$ [F2] would force $3 = ℓ (Δ) \leq ℓ (σ_{1} σ_{2}) = 2$ , a contradiction.

F1F2F5F6step 1.2

3.1

The maximal $Δ$ -exponent is $- 1$ . The pair $(p, A) : = (- 1, σ_{1} σ_{2}^{2})$ satisfies $x = Δ^{p} A$ by step 1.1, $A \in B_{3}^{+}$ by step 1.1 and $Δ ̸ ≼_{L} A$ by step 2.1; by the uniqueness in [F7] of the pair $(p, A)$ it coincides with $(p (x), A (x))$ , hence $p (x) = - 1$ and $A (x) = σ_{1} σ_{2}^{2}$ .

F7step 1.1step 2.1

3.2

The permutation images and left weighting. Since $π$ is a homomorphism with $π (σ_{i}) = s_{i}$ [F3], the two factors have images $π (a_{1}) = s_{1} s_{2}$ and $π (a_{2}) = s_{2}$ , which are distinct; in particular $a_{1} \neq a_{2}$ , so the two-factor form is not a repetition of one simple braid. Left weighting is the instance $i = 1 < r = 2$ of the last assertion of [F7]: $(a_{1} a_{2}) \land_{L} Δ = a_{1}$ , which is literally the computation of step 2.1.

F3F7step 2.1

4.1

The two greedy factors. Put $a_{1} : = σ_{1} σ_{2}$ and $a_{2} : = σ_{2}$ , so that $A (x) = a_{1} a_{2}$ by step 3.1. Then $Δ \land_{L} A (x) = Δ \land_{L} σ_{1} σ_{2}^{2} = a_{1}$ by step 2.1, and the unique $A_{1}$ with $A (x) = a_{1} A_{1}$ is $A_{1} = σ_{2} = a_{2}$ , since $(σ_{1} σ_{2}) σ_{2} = σ_{1} σ_{2}^{2}$ [F1]; further $a_{2} ≼_{L} Δ$ because $Δ = σ_{2} σ_{1} σ_{2} = σ_{2} (σ_{1} σ_{2})$ [F1], hence $Δ \land_{L} A_{1} = Δ \land_{L} a_{2} = a_{2}$ [F6], and the unique $A_{2}$ with $A_{1} = a_{2} A_{2}$ is $A_{2} = 1$ . So the recursion of [F7] produces $r = 2$ with factors $a_{1}, a_{2}$ . Both are proper simple braids: $Δ = (σ_{1} σ_{2}) σ_{1}$ exhibits $a_{1} ≼_{L} Δ$ and $Δ = σ_{2} (σ_{1} σ_{2})$ exhibits $a_{2} ≼_{L} Δ$ [F1], while $a_{1} \neq 1, Δ$ and $a_{2} \neq 1, Δ$ because $ℓ (a_{1}) = 2$ and $ℓ (a_{2}) = 1$ lie in ${1, 2}$ and not in ${0, 3}$ [F1].

F1F6F7step 2.1step 3.1

5.1

The normal form conditions hold. For $i = 2$ , step 4.1 gives $Δ \land_{L} a_{2} = a_{2} = Δ \land_{L} (a_{2})$ ; for $i = 1$ , step 2.1 gives $Δ \land_{L} (a_{1} a_{2}) = Δ \land_{L} σ_{1} σ_{2}^{2} = a_{1}$ . So $x = Δ^{- 1} a_{1} a_{2}$ with both $a_{i}$ proper simple and $a_{i} = Δ \land_{L} (a_{i} \dots a_{r})$ for $i = 1, 2$ ; by the uniqueness in [F7] this is the left normal form of $x$ , and [F7] identifies its data as $p (x) = - 1$ and $A (x) = a_{1} a_{2} = σ_{1} σ_{2}^{2}$ , in agreement with step 3.1.

F7step 2.1step 4.1

6.1

Conclusion. The element $x = σ_{1}^{- 1} σ_{2}$ of $B_{3}$ has left Garside normal form $x = Δ^{- 1} (σ_{1} σ_{2}) σ_{2}$ with $p (x) = - 1$ and $A (x) = σ_{1} σ_{2}^{2}$ , with proper simple factors $a_{1} = σ_{1} σ_{2}$ and $a_{2} = σ_{2}$ whose images in $S_{3}$ are $s_{1} s_{2}$ and $s_{2}$ , and with the factor pair left weighted by step 3.2. Moreover $x \notin B_{3}^{+}$ , because $p (x) = - 1 < 0$ while $p \geq 0$ characterises positivity by [F7]; this is the qualitative content of the computation, since $x$ is visibly written with an inverse letter. No choice principle is used, the only selections being the explicit words displayed above. ∎

F7step 1.1step 2.1step 3.1step 5.1step 3.2

Remarks

Reading off the algorithm. In the notation of Left garside normal form is unique the recursion runs $A_{0} = σ_{1} σ_{2}^{2}$ , $a_{1} = Δ \land_{L} A_{0} = σ_{1} σ_{2}$ , $A_{1} = σ_{2}$ , $a_{2} = Δ \land_{L} A_{1} = σ_{2}$ , $A_{2} = 1$ ; the factor $σ_{1} σ_{2}$ is the maximal simple prefix of $σ_{1} σ_{2}^{2}$ because $Δ$ does not divide $σ_{1} σ_{2}^{2}$ on the left, and the remainder $σ_{2}$ is already simple.
Why the $Δ$ -exponent is negative. The computation above gives $p (x) = - 1$ ; by Left garside normal form is unique (d)(ii), this proves $σ_{1}^{- 1} σ_{2}$ is not positive. The calculation exhibits the witness pair $(- 1, σ_{1} σ_{2}^{2})$ of that theorem's uniqueness clause rather than merely asserting it. Note that $σ_{1} σ_{2}^{2}$ has the same length $3$ as $Δ$ ; length alone therefore decides neither left divisibility nor the meet, and it is the scaling computation of step 2.1 that shows $Δ ̸ ≼_{L} σ_{1} σ_{2}^{2}$ .
Conventions. All products are read left to right as words in the generators, and the permutation images are those of the positive monoid map $π$ ; the cycle notation is that of The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition, so $s_{1} s_{2} = (1 2 3)$ . No choice principle is used: every object in the computation is an explicitly displayed finite word.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

J. Gonzalez-Meneses, Basic results on braid groups, Section 4.1, printed pp. 29-30 (standard reference, not scraped)
J. Birman and T. Brendle, Braids: A Survey, Section 5.1 (standard reference, not scraped)