LemmaStatement: Literature-sourcedProof: 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 based configuration-loop homotopy traces a braid isotopy

Statement

Let $H : I_{s} \times I_{t} \to C_{n} (int D^{2})$ be a continuous homotopy of based loops at $[Q]$ , written with the homotopy parameter $s$ first and height $t$ second. Thus $H (s, 0) = H (s, 1) = [Q] (s \in I),$ and the boundary loops are $α (t) : = H (0, t)$ and $β (t) : = H (1, t)$ . The unique ordered lifts of $α$ and $β$ starting at $Q$ trace geometric braids that are braid-isotopic relative to their top and bottom endpoints.

Facts & Assumptions

Given: $n \in N$ ; a continuous map $H : I_{s} \times I_{t} \to C_{n} (int D^{2})$ satisfying the displayed based-loop endpoint conditions; and its boundary loops $α = H (0, -)$ and $β = H (1, -)$ .

[L1]

The quotient map $p^{\circ} : F_{n} (int D^{2}) \to C_{n} (int D^{2})$ is a covering, and every based interior configuration loop at $[Q]$ has a unique lift from $Q$ whose coordinate graphs form its geometric braid (An interior configuration loop traces a geometric braid).

[L2]

A path homotopy relative to its endpoints is a jointly continuous map on the product square fixing the two endpoints throughout; switching the two coordinates writes the homotopy parameter first and the path parameter second (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

[L3]

If $p : E \to B$ is a covering, a homotopy $G : Y \times I \to B$ and a lift of $G (-, 0)$ are given, then there is a unique continuous lift of $G$ extending that initial lift (Existence and uniqueness of homotopy lifts through a covering map).

[L4]

$F_{n} (X)$ is a subspace of the product $X^{n}$ with its product topology (Ordered configuration spaces $F_{n} (X)$ ).

[L5]

The product topology is the initial topology of the coordinate projections, so coordinate maps of a map into a product are continuous (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).

[L6]

A braid isotopy has jointly continuous coordinate maps and requires the bottom tuple pointwise fixed and the top endpoint set of every slice equal to $Q$ (Braid isotopy relative to the top and bottom endpoints).

[L7]

Since each labelled top endpoint lies in the finite discrete set $Q$ , joint continuity makes that endpoint constant throughout the isotopy (Braid isotopy relative to the top and bottom endpoints).

No arbitrary lift is chosen: the initial lift along $t = 0$ is the specified constant map $s \mapsto Q$ , and the homotopy lift is unique.

Proof

technique · direct

1.1L1L2

Specify the initial lift. By [L1], $p^{\circ}$ is a covering. The constant map ${\tilde{H}}_{0} : I_{s} \to F_{n} (int D^{2})$ , ${\tilde{H}}_{0} (s) = Q$ , is continuous and lifts the edge $H (s, 0) = [Q]$ because $p^{\circ} (Q) = [Q]$ .

2.1step 1.1L3

Lift the full square. Apply [L3] to $G = H$ with $Y = I_{s}$ , height coordinate $t$ , and initial lift from step 1.1. There is a unique jointly continuous lift $\tilde{H} : I_{s} \times I_{t} \to F_{n} (int D^{2})$ with $p^{\circ} \circ \tilde{H} = H$ and $\tilde{H} (s, 0) = Q$ .

3.1step 2.1L1L2

Each lifted height path is the braid trace. Fix $s \in I$ . By step 2.1, $t \mapsto \tilde{H} (s, t)$ lifts the based loop $H (s, -)$ from $Q$ . Uniqueness in [L1] identifies it with the lift whose coordinate graphs form the geometric braid traced by that loop. Its terminal tuple projects to $H (s, 1) = [Q]$ , so its endpoint set is $Q$ . This includes $n = 1$ , where there are no pairwise-collision conditions.

3.2step 2.1L1L2

Identify the two boundary braids. By step 2.1, $\tilde{H} (0, -)$ lifts $α$ from $Q$ and $\tilde{H} (1, -)$ lifts $β$ from $Q$ . Uniqueness in [L1] identifies these restrictions with the traces of the two boundary loops, so they are the exact braids at the ends of the claimed isotopy.

4.1step 2.1step 3.1L4L5L6L7

The lifted coordinates give a braid isotopy. Define $Z_{j} (s, t)$ to be the $j$ th coordinate of $\tilde{H} (s, t)$ under the fixed real-complex identification. The lift in step 2.1 is jointly continuous into $F_{n} (int D^{2}) \subseteq (int D^{2})^{n}$ ; the coordinate projections are continuous by [L4, L5]. Thus each $Z_{j}$ is jointly continuous. By step 3.1, every slice is a geometric braid with bottom $Q$ and top endpoint set $Q$ . It therefore meets the braid-isotopy conditions [L6]. By [L7], joint continuity also keeps each labelled top endpoint fixed during the isotopy. For $n = 0$ , both configuration spaces are points and this is the unique empty braid isotopy.

5.1step 3.2step 4.1∎

The jointly continuous lifted family has the prescribed boundary braids from step 3.2 and satisfies every braid-isotopy condition by step 4.1.

Depends on

Used by

Dependency tree · two levels

32 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.3, printed p. 5 (standard reference, not scraped)