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.

A circle is the boundary of a disk

Example

Let $D^{2} = {\overline{B}}_{2} (0, 1) \subset R^{2}$ be the closed unit disk. It is a compact smooth surface with boundary $S^{1} = S_{2} (0, 1)$ , and with the orientation of $D^{2}$ induced from the standard orientation of $R^{2}$ , its induced boundary orientation is the standard counterclockwise orientation of $S^{1}$ . Consequently $S^{1}$ with that orientation is null-cobordant, so its class is zero in $Ω_{1}^{S O}$ and in $Ω_{1}^{O}$ ; and the circle with the opposite orientation has the same zero class and is the inverse of $[S^{1}]$ in $Ω_{1}^{S O}$ .

Facts & Assumptions

Given: The closed unit disk $D^{2} = {\overline{B}}_{2} (0, 1) \subset R^{2}$ , the sphere $S^{1} = S_{2} (0, 1)$ , the standard orientation of $R^{2}$ (the one for which the identity chart is positive), and the orientations induced on $D^{2}$ and on its boundary.

[F1]

For $n \geq 1$ , write $B^{n} = {x : ρ (x) \geq 0}$ with $ρ (x) = 1 - ∣ x ∣^{2}$ . At each boundary point choose an index $j$ with $\partial_{j} ρ \neq 0$ , move that coordinate last, and apply the inverse function theorem to the remaining $n - 1$ coordinates together with $ρ$ . Its inverse is smooth: the derivative formula for the $C^{1}$ inverse bootstraps inductively to every order when the original map is smooth. Restricting to $ρ \geq 0$ gives a half-space chart, and these charts have smooth transitions because they are restrictions of ambient diffeomorphisms (The Euclidean inverse function theorem, Euclidean upper half-space and its boundary, Smooth charts, atlases, and structures with boundary). The interior uses ordinary Euclidean charts (Euclidean spaces and Euclidean open subsets as smooth manifolds). Thus $B^{n}$ is a smooth manifold with boundary $S^{n - 1}$ . Inward vectors have $d ρ > 0$ (Boundary-defining functions exist locally and detect inward vectors, Boundary-defining functions), and Euclidean balls and spheres are compact (For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact, Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[F2]

The induced boundary orientation is outward-normal-first: an outward vector followed by a positive basis of the boundary is a positive basis of the ambient tangent space (Induced boundary orientation, Oriented smooth manifolds and oriented charts).

[F3]

A closed oriented manifold is null-cobordant when it is oriented cobordant to the empty manifold; reversing the orientation of an oriented bordism flips both induced boundary orientations (Null-cobordant closed manifolds, Oriented smooth cobordism), and the classes of closed oriented $1$ -manifolds form $Ω_{1}^{S O}$ with operation $[M] + [N] = [M ⊔ N]$ and zero the class of $\emptyset$ (Unoriented and oriented bordism groups).

[F4]

Orientation-preserving diffeomorphic closed oriented manifolds have the same class (Disjoint union makes bordism classes abelian groups). A nonempty connected orientable manifold has exactly two orientations: relative to one supplied determinant ray the sign of another is locally constant, hence constant on the connected manifold (Oriented smooth manifolds and oriented charts).

Verification

1.1F1

( $D^{2}$ is a compact smooth surface with boundary $S^{1}$ .) By [F1] with $n = 2$ , $D^{2} = B^{2}$ is a smooth manifold with boundary $S^{1}$ , and $ρ (x) = 1 - ∣ x ∣^{2}$ is a boundary-defining function; by compactness of Euclidean balls $D^{2}$ is compact, hence a compact surface with boundary.

1.2F1F2

(The induced boundary orientation is counterclockwise.) Let $p \in S^{1}$ . Since $ρ (x) = 1 - ∣ x ∣^{2}$ has gradient $\nabla ρ (p) = - 2 p$ , the function $ρ$ decreases in the radial direction, so the outward normal of $D^{2}$ at $p$ is the radial vector $p$ (unit length). Let $J p = (- p_{2}, p_{1})$ be the counterclockwise rotation of $p$ by $90^{\circ}$ . In the standard orientation of $R^{2}$ the basis $(p, J p)$ is positive, because $\det (p, J p) = ∣ p ∣^{2} = 1 > 0$ . The outward-normal-first rule of [F2] therefore says that $(p, J p)$ is a positive basis of $T_{p} D^{2}$ exactly when $J p$ is a positive basis of $T_{p} S^{1}$ ; the unit tangent $J p$ is the counterclockwise direction of $S^{1}$ , so the induced boundary orientation of $S^{1} = \partial D^{2}$ is counterclockwise.

2.1F3step 1.2construct

(Null-cobordisms of the two circles.) Let $o$ be the counterclockwise orientation of $S^{1}$ . The map $θ : [0, 1) \times S^{1} \to D^{2}$ , $θ (s, p) = (1 - s / 2) p$ , is a smooth embedding onto the open annulus ${x : 1 / 2 < ∣ x ∣ \leq 1}$ and satisfies $θ (0, p) = p$ , so it is a supplied collar (Smooth collars of a manifold boundary). With the whole boundary incoming, the standard orientation on $D^{2}$ gives induced orientation $o$ by step 1.2, so it null-bords $(S^{1}, - o)$ . Reversing the disk orientation gives induced boundary orientation $- o$ and null-bords $(S^{1}, o)$ . Thus both oriented classes and their underlying unoriented classes are zero by [F3].

2.2F3F4step 1.2

(The two classes are mutually inverse.) Let $W : = (- D^{2}) ⊔ D^{2}$ with the disjoint-union orientation, a compact oriented surface whose boundary is the disjoint union of the two circles, and whose induced boundary orientation on $\partial W$ is (clockwise) $⊔$ (counterclockwise). As a bordism from the closed oriented manifold $S^{1} ⊔ (- S^{1})$ to $\emptyset$ it realises $[S^{1}] + [- S^{1}] = [\emptyset] = 0$ in $Ω_{1}^{S O}$ by [F3]: the incoming face carries the negative of $o ⊔ (- o)$ , namely $(- o) ⊔ o$ , which is exactly the induced orientation of $\partial W$ .

3.1step 1.1step 1.2step 2.1step 2.2∎

(Assembly.) Steps 1.1–1.2 identify $D^{2}$ as a compact smooth surface with boundary $S^{1}$ and compute its induced boundary orientation as counterclockwise; step 2.1 gives the null-cobordisms of both oriented circles, so $[S^{1}] = 0$ in $Ω_{1}^{S O}$ and in $Ω_{1}^{O}$ ; step 2.2 shows that the class of the opposite orientation is also $0$ and is the inverse of $[S^{1}]$ . This is the asserted example.

Depends on

Used by

The pair of pants is a cobordism realizing addition of circles Example

Dependency tree · two levels

64 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

Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor and James Stasheff, Characteristic Classes (original pagination) (standard reference, not scraped)