ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

An empty incoming boundary requires zero handles

Example

Assume ${A C}_{ω}$ . Let $n \geq 1$ . If a nonempty compact connected triad has $M_{0} = \emptyset$ , then every handle decomposition relative to $M_{0}$ begins with at least one $0$ -handle: a $k$ -handle with $k \geq 1$ attaches along the nonempty sphere $S^{k - 1} \times D^{n - k}$ , which cannot be embedded in the empty initial boundary. The sphere $S^{n}$ has the presentation with exactly one $0$ -handle and one $n$ -handle. This shows that the nonempty-incoming-boundary hypothesis in the elimination proposition cannot be dropped.

Facts & Assumptions

Given: A nonempty compact connected triad $(W; M_{0}, M_{1})$ with $n \geq 1$ and ${A C}_{ω}$ with $M_{0} = \emptyset$ and $\dim W = n$ , and a finite handle decomposition of $W$ relative to $M_{0}$ with indices $k_{1}, \dots, k_{r}$ and attaching embeddings $h_{1}, \dots, h_{r}$ .

[F1]

Handle decomposition relative to the incoming boundary: a decomposition relative to $M_{0}$ is a finite ordered list of handles attached successively, the first to the boundary of the initial stage; when $M_{0} = \emptyset$ the initial stage is the empty manifold and the first handle attaches to the empty set.

[F2]

Index zero handles create components: a $0$ -handle attaches along the empty set $S^{- 1} \times D^{n}$ and adds one disjoint $n$ -disk component.

[F3]

Index n handles cap boundary spheres: an $n$ -handle attaches along its whole boundary sphere $S^{n - 1}$ . For $n \geq 2$ it fills a boundary component diffeomorphic to $S^{n - 1}$ ; for $n = 1$ its attaching $S^{0}$ is a pair of boundary points, possibly in different components.

[F4]

Connected cobordisms admit presentations without superfluous zero handles: Assume ${A C}_{ω}$ . A connected triad with nonempty incoming boundary admits a presentation relative to that boundary with no $0$ -handles; when the incoming boundary is empty, exactly the $0$ -handles needed to create the components remain.

[F5]

Morse functions and handle decompositions correspond: Assume ${A C}_{ω}$ . Every finite handle decomposition of a compact triad relative to its incoming face is induced by an adapted excellent Morse function with one critical point per handle, of the same index (and conversely).

[A1]

For $k \geq 1$ the attaching region $S^{k - 1} \times D^{n - k}$ is nonempty: $S^{k - 1} \neq \emptyset$ for $k \geq 1$ , and $D^{n - k} \neq \emptyset$ for $0 \leq k \leq n$ . For $k = 0$ the attaching region is $S^{- 1} \times D^{n} = \emptyset$ .

Verification

technique · direct

1.1F1A1givenalgebra

The initial stage of any presentation relative to $M_{0} = \emptyset$ is empty, so its boundary is empty as well, and the first attaching embedding $h_{1}$ must map into it; hence the first handle must have empty attaching region. By [A1] this happens exactly for $k = 0$ : the attaching region of a $0$ -handle is $S^{- 1} \times D^{n} = \emptyset$ , while a $k$ -handle with $k \geq 1$ has nonempty attaching region and cannot be attached to the empty initial boundary. Therefore every presentation begins with at least one $0$ -handle.

2.1F2F4step 1.1algebra

A connected manifold with empty incoming boundary needs at least one $0$ -handle, since the first stage is empty and only a $0$ -handle creates a component by [F2]; and by [F4] exactly the $0$ -handles needed to create the components of $W$ remain, which for connected $W$ is one $0$ -handle. Hence the elimination of $0$ -handles is impossible when $M_{0} = \emptyset$ , and the hypothesis $M_{0} \neq \emptyset$ in [F4] is necessary.

3.1F3step 2.1construct

The sphere example: the closed $n$ -sphere is the union of two closed disks glued along their common boundary sphere, $S^{n} = D^{n} \cup_{S^{n - 1}} D^{n}$ . Read the first disk as a $0$ -handle and the second as an $n$ -handle attached along its whole boundary $S^{n - 1}$ , which by [F3] fills the whole boundary sphere and produces $S^{n}$ . This presentation has exactly one $0$ -handle and one $n$ -handle, and no other handles, in agreement with the fact that a connected manifold with $M_{0} = \emptyset$ keeps exactly one $0$ -handle by step 2.1 and that the $n$ -handle closes the remaining boundary sphere.

4.1F3F5step 1.1step 3.1algebra∎

By [F5] the presentation of step 3.1 is realized by a Morse function on the triadic description of $S^{n}$ with two critical points, of indices $0$ and $n$ ; this is the standard round-sphere height function with a minimum and a maximum. In particular the sphere carries a presentation with exactly one $0$ -handle as claimed, and the presentation of any connected triad with empty incoming boundary must begin with a $0$ -handle, so the elimination proposition cannot be applied without change in that case.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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)