Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

The Artin action of the B_3 generators

Example

In B3 the two Artin automorphisms of Artin automorphisms of the free group act by ρ(σ1):x1↦x1x2x1−1,x2↦x1,x3↦x3, ρ(σ2):x1↦x1,x2↦x2x3x2−1,x3↦x2. Tabulating both on a basis of F3 and verifying the relation ρ(σ1)ρ(σ2)ρ(σ1)=ρ(σ2)ρ(σ1)ρ(σ2) by direct substitution and free reduction:

generatorρ(σ1)ρ(σ2)
x1x1x2x1−1x1
x2x1x2x3x2−1
x3x3x2

Facts & Assumptions

Given: the free group F3=⟨x1,x2,x3⟩ and the automorphisms ρ(σ1),ρ(σ2) of Artin automorphisms of the free group.

[F1]

The displayed substitutions are the frozen formulas with n=3, and ρ(σj)(xk)=xk whenever k∉{j,j+1}; two endomorphisms agreeing on a free basis are equal, and equality of elements is decided by reduced words (Artin automorphisms of the free group).

Proof

technique · direct
1.1F1

The table. Substituting the frozen formulas for n=3 gives the table displayed above: ρ(σ1) moves only x1,x2, and ρ(σ2) moves only x2,x3.

2.1F1step 1.1

The composite ρ(σ1)ρ(σ2)ρ(σ1). Composing the table (rightmost letter first) gives x1↦x1x2x3x2−1x1−1,x2↦x1x2x1−1,x3↦x1. Indeed: applying ρ(σ1) first gives (x1,x2,x3)↦(x1x2x1−1,x1,x3); applying ρ(σ2) gives (x1x2x3x2−1x1−1, x1, x2); and applying ρ(σ1) again gives (x1x2x3x2−1x1−1, x1x2x1−1, x1).

2.2F1step 1.1

The composite ρ(σ2)ρ(σ1)ρ(σ2). Composing in the opposite order gives x1↦x1x2x3x2−1x1−1,x2↦x1x2x1−1,x3↦x1. Indeed: applying ρ(σ2) first gives (x1,x2x3x2−1,x2); applying ρ(σ1) gives (x1x2x1−1, x1x3x1−1, x1); and applying ρ(σ2) again gives (x1x2x3x2−1x1−1, x1x2x1−1, x1).

3.1F1step 2.1step 2.2∎

Comparison. The two composites of steps 2.1 and 2.2 agree on each of x1,x2,x3, hence on the whole free basis; by [F1] they are equal as automorphisms, which verifies the braid relation in B3.

Remarks

  • The exponent and the conjugation direction in the table follow the frozen convention of Artin automorphisms of the free group; with Artin's original letter convention the table is read with σj and σj−1 interchanged.
  • The same verification is the n=3 case of lem-artin-automorphisms-satisfy-the-braid-relations.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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