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

Zero-surgery on the circle

Example

Assume ${A C}_{ω}$ , as in the surgery definition. Take $M = S^{1}$ , $p = 0$ , $q = 1$ , and the standard framed embedding $φ : S^{0} \times D^{1} ↪ S^{1}$ that is the inclusion of the vertical sides in the standard decomposition (with corner charts rounded compatibly) $\partial (D^{1} \times D^{1}) = (S^{0} \times D^{1}) \cup (D^{1} \times S^{0})$ of the square's boundary, whose image is the union of two disjoint closed intervals. The framing is part of this data, and it is the one used in the verification below. The range $0 \leq p \leq m - 1$ holds with $m = 1$ . The $0$ -surgery removes the interiors of the two intervals and glues $D^{1} \times S^{0}$ , that is, two intervals, along $S^{0} \times S^{0}$ , that is, four points. The result is $S^{1} ⊔ S^{1}$ .

Verification

Given: $M = S^{1}$ with the standard framed embedding $φ : S^{0} \times D^{1} ↪ S^{1}$ of the two closed intervals.

[F1] p-surgery on a smooth m-manifold: the $p$ -surgery is $M_{φ} = (M ∖ φ (S^{p} \times int D^{q})) \cup_{φ ∣_{S^{p} \times S^{q - 1}}} (D^{p + 1} \times S^{q - 1}),$ with $p = 0$ , $q = 1$ this removes the interiors of the two intervals and glues two intervals along four points; the construction takes place in the interior of $M$ .

[F2] The outgoing boundary of a handle attachment trades the disk factors: for $k = 1$ , $n = 2$ the boundary of the square is $\partial (D^{1} \times D^{1}) = (S^{0} \times D^{1}) \cup (D^{1} \times S^{0})$ , two pairs of opposite sides meeting in the four corners $S^{0} \times S^{0}$ , and the trade lemma identifies the complement of the open attaching region with the complementary pair of sides.

[F3] The surgery gluing has a canonical smooth structure up to diffeomorphism: the gluing along the common boundary gives a smooth $1$ -manifold, and its diffeomorphism type is the one fixed by the identification on the overlap.

1.1F1given

The normal bundle of a point in a $1$ -manifold is trivial, so a framing of the $0$ -sphere $S^{0} \times {0}$ is exactly the product structure exhibited by $φ$ ; the image of $φ$ is the union of two disjoint closed intervals of $S^{1}$ , whose complement after removal of their interiors is a union of two disjoint closed arcs.

2.1F1F2step 1.1

Reading the standard decomposition of the square's boundary in [F2], the two intervals $S^{0} \times D^{1}$ are the two vertical sides and the two intervals $D^{1} \times S^{0}$ are the two horizontal sides; the four corners are $S^{0} \times S^{0}$ . The $0$ -surgery removes the open vertical sides and glues in the two horizontal sides, identifying their endpoints with the four corners by the framing, so the result is exactly the boundary of the square with the vertical sides replaced by the horizontal sides.

3.1F2step 2.1algebra

The complement of the open vertical sides in the square's boundary is the union of the two horizontal sides, each a closed arc; the glued interval $D^{1} \times {- 1}$ joins the two endpoints of one horizontal side and the glued interval $D^{1} \times {+ 1}$ joins the two endpoints of the other, so each horizontal side is closed up by one glued interval into a circle. There are no other points, and the two circles are disjoint because the four corners are distributed two to each. Hence the surgered manifold is $S^{1} ⊔ S^{1}$ .

4.1F1F2F3step 3.1∎

Equivalently, the same computation reads $D^{1} \times S^{0} \cup D^{1} \times S^{0} = S^{0} \times (D^{1} \cup_{S^{0}} D^{1}) = S^{0} \times S^{1} = S^{1} ⊔ S^{1},$ the two copies of $D^{1} \times S^{0}$ being the glued-in piece and the complementary arcs of the standard decomposition of $\partial (D^{1} \times D^{1})$ ; the gluing is the one induced by the framing, and by [F3] the smooth structure is the canonical one.

The example exercises the endpoint $p = 0$ of the definition and the case $p = m - 1$ ( $q = 1$ ) of the trace construction: the trace is the cylinder $S^{1} \times [0, 1]$ with a single $1$ -handle attached, in accordance with the index shift of the trace definition, and its outgoing face is the two-circle manifold just computed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

Andrew Ranicki, Algebraic and Geometric Surgery (Oxford Mathematical Monographs, 2002; electronic copy) (standard reference, not scraped)
C. T. C. Wall, Differential Topology (Cambridge Studies in Advanced Mathematics 156, Cambridge University Press 2016) (standard reference, not scraped)
Wolfgang Lück, A Basic Introduction to Surgery Theory (lecture notes, Münster, 27 October 2004) (standard reference, not scraped)