ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck pass

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.

Reordering independent one-handles

Example

Assume ${A C}_{ω}$ . On a surface, attach two disjoint $1$ -handles to a disk along disjoint pairs of disks in two different orders. The resulting handlebodies are diffeomorphic: the attaching regions are disjoint, both handles have index one, and the equal-index lemma permits simultaneous attachment or attachment in either order. The example tests the equal-index boundary case of rearrangement, where the dimension count $0 + 0 < 1$ makes the two attaching spheres disjoint and no trajectory obstruction can occur.

Facts & Assumptions

Given: The disk $D^{2}$ as a $0$ -handle and two embedded $1$ -handles $h_{1}, h_{2}$ attached to it along disjoint pairs of disjoint disks $D_{1}, D_{2} \subseteq \partial D^{2}$ ; write $M_{12}$ for the result of attaching $h_{1}$ then $h_{2}$ and $M_{21}$ for the result of attaching $h_{2}$ then $h_{1}$ .

[F1]

Handles of equal index can be attached on one level: Assume ${A C}_{ω}$ . Handles of equal index attached at one level may be regarded as attached simultaneously or successively in any order, with the same result up to diffeomorphism relative to the lower stage; their attaching embeddings may be changed by isotopy of the attaching region.

[F2]

Handle decomposition relative to the incoming boundary: a handle decomposition relative to the incoming boundary is an ordered list of handles attached successively to the collar of the incoming face.

[F3]

Index zero handles create components: a $0$ -handle attaches along the empty set and adds a disjoint $n$ -disk; in the surface case it is the disk $D^{2}$ .

[F4]

Handle attachments are relative cell attachments up to homotopy: each handle attachment is, up to homotopy of pairs relative to the lower stage, the attachment of a cell along the core sphere.

[F5]

Smooth handle attachment is independent of corner rounding up to diffeomorphism: two compatible roundings of the same attachment are diffeomorphic by an isotopy supported in the collar.

[A1]

Dimension count. For a surface, $n = 2$ . The attaching sphere of a $1$ -handle is $S^{0}$ , a pair of points, and the belt sphere of a $1$ -handle is also $S^{0}$ ; in the level set, which is a $1$ -manifold, the attaching sphere of the second handle and the belt sphere of the first have dimensions $0$ and $0$ , with $0 + 0 < n - 1 = 1$ , so they can be isotoped apart and the pair cannot obstruct the reordering.

Verification

technique · direct

1.1F2F3given

The disk $D^{2}$ is the $0$ -handle of [F3], with boundary the circle $\partial D^{2}$ . The two $1$ -handles are attached along the pairs of disks $D_{1}$ and $D_{2}$ , which are disjoint, so the attaching regions of the two handles are disjoint subsets of the level $\partial D^{2}$ ; the index of both is $1$ .

1.2F2givenconstruct

In either order the same two attachments are performed along the same disjoint attaching regions, and each attachment adds a handle body homeomorphic to $D^{1} \times D^{1}$ ; the surface produced is the disk with two bands attached, a compact surface with two bands, in both cases.

2.1F1A1step 1.1step 1.2algebra

By [F1] the two equal-index handles may be attached simultaneously or in either order with the same result up to diffeomorphism relative to the lower stage $D^{2}$ ; hence $M_{12}$ and $M_{21}$ are diffeomorphic by a diffeomorphism fixing the disk and identifying each labelled handle with the same labelled handle. The dimension count of [A1] records the reason: the two attaching spheres of the $1$ -handles are $0$ -dimensional in a $1$ -dimensional level and can be made disjoint, so no trajectory or intersection obstruction to the reordering exists.

3.1F4F5step 2.1algebra∎

The comparison also holds at the level of homotopy types: by [F4] each of the two attachments is, up to homotopy of pairs, the attachment of a $1$ -cell along a pair of points, so both orders produce the homotopy type of a wedge of two circles, in accordance with the disk with two bands. Corner rounding does not affect the conclusion, by [F5].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

C. T. C. Wall, Differential Topology (Cambridge Studies in Advanced Mathematics 156), Sections 5.1-5.4, printed pp. 129-148 (standard reference, not scraped)
John Milnor, Lectures on the h-Cobordism Theorem (notes by L. Siebenmann and J. Sondow), Sections 2-4, printed pp. 10-48 (standard reference, not scraped)