ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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 pure two-strand full twist as an ordered loop

Example

For $n = 2$ with $Q = (- h, h)$ , the ordered path $η (t) = (- h, - h + 2 h \exp (2 π i t))$ stays collision-free in the open disk and closes at $Q$ . Its traced geometric braid is the positive full twist $[σ_{1}]^{2}$ and has identity endpoint permutation.

Facts & Assumptions

Given: $n = 2$ , the published base tuple $Q$ , spacing $h$ , positive elementary half twist $σ_{1}$ , and its diamond relative path $ρ$ .

[L1]

For $n = 2$ , $h = 1 / (4 (2 + 1)) = 1 / 12$ , $Q = (- h, h)$ , the midpoint is $0$ , and $(σ_{1})_{1} = ρ$ , $(σ_{1})_{2} = - ρ$ . The path $ρ$ is continuous, has endpoints $- h, + h$ , never vanishes, and satisfies $∣ ρ (t) ∣ \leq h$ . The positive convention is the published anticlockwise half twist (The elementary geometric half twist, its support disc, and its opposite, Geometric braids in the disc with setwise endpoints).

[L2]

The complex exponential is continuous, $\exp (i θ) = \cos θ + i \sin θ$ and $∣ \exp (i θ) ∣ = 1$ for real $θ$ , and $\exp (i π) = - 1$ ; also $\exp (z + w) = \exp z \exp w$ (The complex exponential is entire and its complex derivative is itself, Complex differentiability at a point implies continuity there, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L3]

Complex modulus is definite and satisfies $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ ; complex addition and scalar multiplication are continuous (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Vector addition and scalar multiplication are continuous in a normed space).

[L4]

On $[0, π]$ cosine decreases through $0$ at $π / 2$ and sine is nonnegative; on $[π, 2 π]$ cosine increases through $0$ at $3 π / 2$ and sine is nonpositive by its $π$ -shift. Thus $\exp (2 π i t)$ lies in the corresponding closed quadrant for $t \in [0, 1 / 4]$ , $[1 / 4, 1 / 2]$ , $[1 / 2, 3 / 4]$ , and $[3 / 4, 1]$ (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi, Pi is the first positive zero of sine).

[L5]

$F_{2} (X)$ is the subspace of $X^{2}$ consisting of ordered pairs with distinct coordinates; continuity into $X^{2}$ is coordinatewise, and continuity into $F_{2} (X)$ follows from the subspace topology (Ordered configuration spaces $F_{n} (X)$ , The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[L6]

The orbit map $p_{2} : F_{2} (X) \to C_{2} (X)$ is continuous, and an interior based motion is a continuous path with both endpoints $[Q]$ (Unordered configuration spaces $C_{n} (X)$ , Based motions of an unordered point configuration).

[L7]

Every interior based configuration loop at $[Q]$ has a unique ordered lift from $Q$ , whose coordinate graphs are its geometric braid trace (An interior configuration loop traces a geometric braid).

[L8]

A geometric braid starts at the labelled tuple $Q$ , remains collision-free in the open disk, and is pure when every labelled endpoint returns to its starting point (Geometric braids in the disc with setwise endpoints).

[L9]

In $γ ⋆ β$ , the first half runs $β$ and the second half runs $γ$ with labels permuted by the lower braid, and the induced class product is $[γ] [β] = [γ ⋆ β]$ (Stacking of geometric braids is a well-defined associative operation on isotopy classes).

[L10]

The isotopy classes of geometric braids based at $Q$ form a group with the stacking product (The isotopy classes of geometric braids based at $Q$ form a group, and the endpoint permutation is a homomorphism).

[L11]

A braid isotopy is a jointly continuous family of braids with bottom tuple $Q$ and top endpoint set $Q$ at every isotopy parameter (Braid isotopy relative to the top and bottom endpoints); piecewise continuous maps on two closed sets covering the square paste continuously (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L12]

For a pure geometric braid with coordinate loop $z_{β}$ at $Q$ , the pure-braid isomorphism is $Ψ ([β]) = (ι_{*}^{F} [z_{β}])^{- 1}$ (Pure geometric braids and ordered configuration loops).

The formulae below specify every path and homotopy. No lift, representative, or point of a nonempty set is chosen, so the Axiom of Choice is not used.

Proof

technique · direct

1.1L1L2L3L5

Put $ω (t) : = \exp (2 π i t)$ . By [L2], $ω$ is continuous and $∣ ω (t) ∣ = 1$ . Since $\exp (i π) = - 1$ and the exponential addition law gives $\exp (2 π i) = \exp (i π)^{2} = 1$ , one has $ω (0) = ω (1) = 1$ . Hence $η (t) = (- h, - h + 2 h ω (t))$ starts and ends at $Q$ . Its coordinate difference is $2 h ω (t) \neq 0$ , and $∣ - h + 2 h ω (t) ∣ \leq h + 2 h = 3 h = \frac{1}{4} < 1,$ while $∣ - h ∣ = h < 1$ . Thus its values are ordered configurations in $F_{2} (int D^{2})$ ; coordinate continuity and [L5] show that $η$ is a continuous ordered loop at $Q$ .

1.2L6L7L8

Let $α (t) : = p_{2} (η (t))$ . By [L6], this is a continuous interior based loop at $[Q]$ . Its unique lift from $Q$ is $η$ itself, so [L7] identifies its trace with the coordinate braid $β_{η} (t) = (- h, - h + 2 h ω (t))$ . Because both coordinates of $η$ return to their starting values, [L8] shows $β_{η}$ is pure and its endpoint permutation is the identity.

1.3L1L2L4L9

Use the stacking formula [L9] on two copies of $σ_{1}$ . Since the endpoint permutation of the lower copy exchanges labels $1$ and $2$ , the stacked coordinate pair is $(ρ (2 t), - ρ (2 t)) (0 \leq t \leq \frac{1}{2}), (- ρ (2 t - 1), ρ (2 t - 1)) (\frac{1}{2} \leq t \leq 1) .$ Its centre is $0$ and its second-minus-first coordinate is $D_{0} (t) = {\begin{cases} - 2 ρ (2 t), & 0 \leq t \leq \frac{1}{2}, \\ 2 ρ (2 t - 1), & \frac{1}{2} \leq t \leq 1. \end{cases}$ Substitution of the two branches of $ρ$ from [L1] shows that $D_{0} (t)$ lies successively in the first, second, third, and fourth closed quadrants on the four quarter intervals. It never vanishes, and $∣ D_{0} (t) ∣ \leq 2 h$ by [L1]. By [L2] and [L4], $D_{1} (t) : = 2 h ω (t)$ lies in the same respective closed quadrant, never vanishes, and has modulus $2 h$ .

2.1L1L2L3L9L11step 1.3

For $s, t \in I$ set $D_{s} (t) : = (1 - s) D_{0} (t) + s D_{1} (t), H_{1} (s, t) : = (- D_{s} (t) / 2, D_{s} (t) / 2) .$ Each closed quadrant is convex and contains no pair of opposite nonzero vectors, so $D_{s} (t) \neq 0$ for every $(s, t)$ . By [L3], $∣ D_{s} (t) ∣ \leq (1 - s) ∣ D_{0} (t) ∣ + s ∣ D_{1} (t) ∣ \leq 2 h,$ so both coordinates of $H_{1}$ have modulus at most $h < 1$ . The formulas and [L2], [L3], [L9] give joint continuity. Both $D_{0}$ and $D_{1}$ equal $2 h$ at $t = 0, 1$ , so $H_{1} (s, 0) = H_{1} (s, 1) = Q$ for every $s$ . Thus [L11] makes $H_{1}$ a braid isotopy from the stacked diamond braid to the centred round pair $β_{r o u n d} (t) = (- h ω (t), h ω (t))$ .

2.2L1L2L3L11step 1.1

Put $C_{s} (t) : = s (- h + h ω (t))$ and define $H_{2} (s, t) : = (C_{s} (t) - h ω (t), C_{s} (t) + h ω (t)) .$ The coordinate difference is $2 h ω (t) \neq 0$ , and [L3] gives $∣ C_{s} (t) \pm h ω (t) ∣ \leq ∣ C_{s} (t) ∣ + h \leq 2 h + h = 3 h < 1.$ Both coordinates are therefore in the open disk and distinct at every height. The formula is jointly continuous by [L2], [L3]. Since $C_{s} (0) = C_{s} (1) = 0$ and $ω (0) = ω (1) = 1$ , the endpoints are $Q$ for every $s$ . Thus [L11] makes $H_{2}$ a braid isotopy from $β_{r o u n d}$ to $β_{η}$ .

3.1L9L10L11step 1.2step 2.1step 2.2

The families $H_{1}$ and $H_{2}$ agree at their common braid $β_{r o u n d}$ . Pasting $H_{1} (2 s, t)$ for $s \leq 1 / 2$ to $H_{2} (2 s - 1, t)$ for $s \geq 1 / 2$ gives a jointly continuous family by [L11]. Each slice is a braid and its endpoints remain $Q$ , so this is a braid isotopy from $σ_{1} ⋆ σ_{1}$ to $β_{η}$ . By [L9] and [L10], $[β_{η}] = [σ_{1} ⋆ σ_{1}] = [σ_{1}]^{2} .$ Together with step 1.2, this proves that the trace of the stated ordered loop is the positive full twist and has identity endpoint permutation.

4.1

Since $β_{η}$ is pure by step 1.2, the exact ordered representative of its class under the pure-braid isomorphism [L12] is $Ψ ([β_{η}]) = (ι_{*}^{F} [η])^{- 1} \in P B_{2} .$ Thus the displayed collision-free ordered loop records this positive full twist under the common basepoint convention, including the inverse in the published identification. [L12, step 1.2, step 3.1] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

98 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

Juan Gonzalez-Meneses, Basic results on braid groups, §1.2, printed pp. 4–5 (standard reference, not scraped)