LemmaStatement: Literature-sourcedProof: 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.

A reducing move lowers the height by one

Statement

Assume the Axiom of Choice. If a diagram $D^{'}$ is obtained from an oriented diagram $D$ by a Yamada-Vogel reducing move, then $h (D^{'}) = h (D) - 1$ . Consequently every sequence of reducing moves starting at $D$ has length at most $h (D)$ .

Facts & Assumptions

Given: AC, an oriented diagram $D$ with Seifert circles $C_{1}, \dots, C_{m}$ , a reducing arc $α$ joining an incoherent pair $C_{i}, C_{j}$ , and the diagram $D^{'}$ obtained by the reducing move along $α$ (Defect regions, reducing arcs and the Yamada-Vogel reducing move).

[F1]

The pair $C_{i}, C_{j}$ is incoherent; in the new Seifert picture the two circles are replaced by two coherent circles $C_{a}, C_{z}$ joined by two signed arcs of opposite signs, all other circles are unchanged, $C_{a}$ bounds a disk $D_{a}$ containing no other Seifert circle of the new picture, and $C_{z}$ bounds a disk $D_{z}$ containing all Seifert circles that were contained in the annulus cobounded by $C_{i}$ and $C_{j}$ (Defect regions, reducing arcs and the Yamada-Vogel reducing move).

[F2]

Coherence of every pair of Seifert circles is defined through the annulus they cobound; the height is the number of incoherent unordered pairs (Coherence of Seifert circles and the height of a diagram).

[F3]

Two disjoint circles cobound an annulus, whose two complementary regions are the two disks bounded by the circles; the three regions determine which third circles lie in the annulus and which in the two disks (Two disjoint circles in the two-sphere cobound an annulus). AC is inherited from this lemma.

Proof

technique · direct

1.1F1F3givenconstruct

Partition the unchanged circles. Let $A$ be the common annulus and let $D_{i}, D_{j}$ be its complementary open disks. Each unchanged circle lies entirely in exactly one of these three regions. The reducing strip lies in $A$ and misses every other circle and signed arc. One new boundary surrounds the small empty strip disk $D_{a}$ ; the other surrounds the old middle region $A$ after the strip surgery, giving $D_{z}$ . In particular no unchanged circle is in $D_{a}$ .

2.1F1F2F3step 1.1algebra

Comparing coherences for a third circle. For $p \notin {i, j}$ with $C_{p} \subset A$ , $C_{p}$ cannot be essential in $A$ , since it would separate the endpoints of the reducing arc. Reading the boundary orientations before and after the strip surgery therefore gives $(C_{p}, C_{z}) = (C_{p}, C_{a}) = (C_{p}, C_{i}) = (C_{p}, C_{j})$ : the two new circles are coherent with $C_{p}$ exactly when the old pair was coherent with $C_{p}$ . For $C_{p} \subset D_{i}$ one has $(C_{p}, C_{z}) = (C_{p}, C_{i})$ and $(C_{p}, C_{a}) = (C_{p}, C_{j})$ , and for $C_{p} \subset D_{j}$ the two roles are interchanged. These identities follow from the descriptions of $D_{a}$ and $D_{z}$ in [F1] and the annulus decomposition of [F3], coherence being the same relation read in the regions of the new picture.

3.1F1F2step 2.1algebra

Counting the incoherent pairs. By step 2.1 pairs of two unchanged circles keep their coherence. For each unchanged $C_{p}$ , step 2.1 preserves the number of incoherent pairs involving $C_{p}$ and one of the two replaced circles; the moved pair itself is incoherent in $D$ by [F1] and the new pair $C_{a}, C_{z}$ is coherent in $D^{'}$ by [F1]. Hence the number of incoherent unordered pairs drops by exactly one: $h (D^{'}) = h (D) - 1$ .

4.1F2step 3.1∎

Conclusion. Since each reducing move lowers the height by one and the height is a nonnegative integer, a sequence of $k$ reducing moves from $D$ satisfies $0 \leq h (D) - k$ , so $k \leq h (D)$ and the sequence terminates after at most $h (D)$ moves. AC is inherited exactly from [F3].

Depends on

Used by

Dependency tree · two levels

15 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

Birman and Brendle, Braids: A Survey, Handbook of Knot Theory chapter, author manuscript; Lemma 2.1, printed pp. 15-16 (standard reference, not scraped)
Traczyk, A new proof of Markov's braid theorem, Banach Center Publications 42 (1998), 409-419; section 1 and Figure 2 (standard reference, not scraped)