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.

A cancelling one-two handle pair on a surface

Example

Assume ${A C}_{ω}$ . In dimension $n = 2$ start with a closed disc $D^{2}$ (a $0$ -handle) and attach a $1$ -handle (a band) along two disjoint intervals of $\partial D^{2}$ , with attaching orientations chosen so the disc orientation extends over the band; the result is an annulus whose two boundary circles each contain exactly one point of the belt sphere $S^{0}$ of the band. Attach a $2$ -handle (a disc) along one boundary circle. Then the attaching sphere of the $2$ -handle meets the belt sphere of the $1$ -handle in exactly one point, the pair is geometrically cancelling, and $D^{2} \cup h^{1} \cup h^{2} ≅ D^{2}$ . The transverse count of the unique intersection point is $1$ mod $2$ and has local sign $\pm 1$ ; the matrix definition of this page is stated for $1 \leq k \leq n - 2$ and does not cover the endpoint case $n = 2$ , which is handled here directly by the geometric criterion.

Facts & Assumptions

Given: Dimension $n = 2$ : a closed disc $D^{2}$ as a $0$ -handle, a $1$ -handle (band) attached along two disjoint intervals of $\partial D^{2}$ , with attaching orientations chosen so the disc orientation extends over the band, and then a $2$ -handle (disc) attached along one boundary circle of the resulting annulus.

[F1]

Attaching a smooth handle with corner rounding and K handle core cocore attaching region and belt sphere: the $1$ -handle $D^{1} \times D^{1}$ has attaching region $S^{0} \times D^{1}$ and outgoing region $D^{1} \times S^{0}$ , so its belt sphere in the outgoing boundary is a $0$ -sphere ${0} \times S^{0}$ ; the $2$ -handle $D^{2} \times D^{0}$ has attaching sphere $S^{1} \times {0}$ .

[F2]

Geometrically cancelling adjacent handle pair: in dimension $n = 2$ and $k = 1$ the attaching sphere of the $2$ -handle is a circle and the belt sphere of the $1$ -handle is a $0$ -sphere in the middle boundary (the two boundary circles of the annulus); they meet transversely in isolated points, and the pair is geometrically cancelling when exactly one point of the belt sphere lies on the attaching circle.

[F3]

Handle cancellation, The local oriented intersection sign, The mod 2 intersection number and The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume ${A C}_{ω}$ ; a geometrically cancelling pair may be deleted, so the total is diffeomorphic to the initial disc; the unique transverse intersection has local sign $\pm 1$ and mod-2 count $1$ .

Verification

Given: The configuration of the statement.

1.1F1given

Attaching a band to $D^{2}$ along two disjoint boundary intervals gives the annulus $S^{1} \times [0, 1]$ , whose two boundary circles each contain exactly one of the two points of the belt sphere $S^{0} = {0} \times S^{0}$ of the band: the two points are the end points of the cocore arc ${0} \times D^{1}$ , one on each boundary circle.

2.1F2F3step 1.1

Attaching the $2$ -handle along one boundary circle makes the attaching circle meet the belt sphere in exactly one point, and the intersection is isolated and automatic in these dimensions; by [F2] the pair is geometrically cancelling, with the transverse count equal to $1$ modulo $2$ and local sign $\pm 1$ by [F3].

3.1F2F3step 2.1given∎

By [F3] the pair cancels: $D^{2} \cup h^{1} \cup h^{2} ≅ D^{2}$ relative to the incoming boundary. The attaching-belt matrix is not defined here: its definition requires $1 \leq k \leq n - 2$ , and with $n = 2$ and $k = 1$ we have $k = n - 1$ , so the endpoint case is handled directly by the geometric criterion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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; complete PDF) (standard reference, not scraped)
John Milnor, Lectures on the h-Cobordism Theorem (notes by L. Siebenmann and J. Sondow; scanned edition with text layer) (standard reference, not scraped)