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

The standard complementary pair fills a ball

Statement

Assume ${A C}_{ω}$ . Let $0 \leq k \leq n - 1$ and let $1 \times φ_{0} : S^{k} \times D^{n - k - 1} \to S^{k} \times D^{n - k}$ be the standard hemisphere attaching embedding, where $φ_{0} : D^{n - k - 1} \to \partial D^{n - k}$ is the stereographic embedding of $D^{n - k - 1}$ onto the upper hemisphere of $\partial D^{n - k}$ . Then: (i) $(S^{k} \times D^{n - k}) \cup_{1 \times φ_{0}} (D^{k + 1} \times D^{n - k - 1}) ≅ D^{n}$ after rounding the corner along $S^{k} \times S^{n - k - 2}$ ; (ii) for the standard equatorial embedding $σ : S^{k - 1} \times D^{n - k} \to \partial D^{n}$ one has $D^{n} \cup_{σ} (D^{k} \times D^{n - k}) ≅ S^{k} \times D^{n - k}$ ; moreover the two diffeomorphisms may be chosen compatibly, so that the $n$ -disc with a standard $k$ -handle followed by the standard $(k + 1)$ -handle is again an $n$ -disc.

Facts & Assumptions

Given: Integers $0 \leq k \leq n - 1$ , the standard $k$ -handle $D^{k} \times D^{n - k}$ and $(k + 1)$ -handle $D^{k + 1} \times D^{n - k - 1}$ , the stereographic embedding $φ_{0} : D^{n - k - 1} \to \partial D^{n - k}$ onto the upper hemisphere of $S^{n - k - 1} = \partial D^{n - k}$ , and the standard equatorial embedding $σ : S^{k - 1} \times D^{n - k} \to \partial D^{n}$ .

[F1]

Attaching a smooth handle with corner rounding and K handle core cocore attaching region and belt sphere: attaching means gluing along the attaching region $S^{k^{'} - 1} \times D^{n - k^{'}}$ by the given embedding and rounding the corner; the outgoing region is $D^{k^{'}} \times S^{n - k^{'} - 1}$ and the belt sphere is ${0} \times S^{n - k^{'} - 1}$ ; there is no corner if $k^{'} = 0$ or $k^{'} = n$ .

[F2]

Smooth handle attachment is independent of corner rounding up to diffeomorphism: two compatible roundings of the same attachment data are diffeomorphic by an isotopy supported in the collar, so the diffeomorphism class of the rounded attachment does not depend on the rounding chosen.

[F4]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): ${A C}_{ω}$ is assumed; it is used by the corner-rounding and collar suppliers cited in [F1] and [F2].

Proof

technique · direct

1.1F1F2given

For (ii), use the rounded product $D^{k} \times D^{n - k}$ as the standard $n$ -disc and attach a second copy along $S^{k - 1} \times D^{n - k}$ . The first factors glue as two hemispheres of $S^{k}$ , with a smooth seam in their collar coordinates. Taking the product with $D^{n - k}$ and rounding the remaining corners gives $S^{k} \times D^{n - k}$ ; the lower handle's belt sphere becomes ${p} \times S^{n - k - 1}$ , for a point $p$ in its core hemisphere. For $k = 0$ the seam is empty and this says that adding a disjoint disc gives $S^{0} \times D^{n}$ .

1.2F1F2construct

Put $p = n - k - 1 \geq 0$ . Model the disk factor $D^{p + 1}$ by $D^{p} \times [0, 1]$ , rounding its bottom and side corners, and retain the top face $D^{p} \times {1}$ as the attaching hemisphere. This is the usual disk with a corner introduced along the equator: in meridian coordinates a smooth monotone rounding identifies it with $D^{p + 1}$ , carrying the top face onto the upper hemisphere. Its disk parametrization is chosen to be $φ_{0}$ . The same product charts on the attaching seam are used on the handle side. Thus the rounded attachment in (i) is represented by the rounded product $((S^{k} \times [0, 1]) \cup_{S^{k} \times {1}} D^{k + 1}) \times D^{p} .$ For $p = 0$ the disk factor is simply an interval and the attaching hemisphere is one endpoint.

2.1F1F2step 1.2construct

The first factor of step 1.2 is a disk with an extra boundary collar. Identify its cap with the unit disk in $R^{k + 1}$ and send $(u, t) \in S^{k} \times [0, 1]$ to $(2 - t) u$ . The cap boundary and $t = 1$ have the same radial collar coordinate, so this is a smooth identification, across the seam, with the disk of radius $2$ . Consequently the product in step 1.2 is a product of disks, whose compatible rounding is a standard $n$ -disc (round the convex product boundary and use its smooth radial parametrization). The rounding-independence supplier makes this conclusion independent of the compatible profiles. This proves (i), including $k = 0$ and $k = n - 1$ .

3.1F1F2F4step 1.1step 2.1∎

In the two-hemisphere identification of step 1.1 choose the disk-factor hemisphere and its framing exactly as in step 1.2. The standard $(k + 1)$ -handle is then attached by $1 \times φ_{0}$ , so step 2.1 returns an $n$ -disc. These are the required compatible identifications for the consecutive standard pair; Countable Choice is inherited only from the attachment and rounding conventions.

Depends on

Used by

A cancelling zero-one handle pair Example
A handle slide realizes an elementary row operation Example
Algebraic cancellation does not yet give geometric cancellation Lemma
One transverse intersection gives the standard local cancelling model Lemma
Creation of a cancelling handle pair Theorem
Handle cancellation Theorem

Dependency tree · two levels

26 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)
Wolfgang Lück, A Basic Introduction to Surgery Theory (ICTP lecture notes; complete author PDF) (standard reference, not scraped)