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

Two unoriented points bound an interval

Example

The closed interval $[- 1, 1]$ is a compact smooth one-manifold with boundary ${- 1, 1}$ ; hence the disjoint union of two points, as a closed zero-manifold, is null-cobordant and $[p t] + [p t] = 0$ in $Ω_{0}^{O}$ (Unoriented and oriented bordism groups). Since a single point is not null-cobordant (its parity is odd), the class of the one-point manifold is the unique nonzero element of $Ω_{0}^{O} ≅ Z / 2 Z$ (Zero-dimensional bordism groups). Thus every closed zero-manifold with an even number of points is null-cobordant.

Facts & Assumptions

Given: The closed interval $[- 1, 1]$ , the two-point manifold ${a, b}$ with distinct points, and the bordism classes of closed zero-manifolds.

[F1]

The closed ball $B^{1} = [- 1, 1] = {x : 1 - x^{2} \geq 0}$ is a compact smooth one-manifold with boundary $S^{0} = {- 1, 1}$ : the open interval is an open subset of $R$ , and at each endpoint the derivative of $1 - x^{2}$ is nonzero, so the inverse function theorem gives a half-space chart (Euclidean spaces and Euclidean open subsets as smooth manifolds, The Euclidean inverse function theorem, Euclidean upper half-space and its boundary, Smooth charts, atlases, and structures with boundary, Boundary-defining functions); Euclidean closed balls are compact and closed subsets of compact spaces are compact (For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[F2]

A closed zero-manifold is null-cobordant exactly when it is the whole boundary of a compact smooth one-manifold with a collar of that boundary; the class of a null-cobordant manifold is zero in the bordism group (Unoriented smooth cobordism of closed manifolds, Null-cobordant closed manifolds, Smooth collars of a manifold boundary, Immersions and embeddings for manifolds with boundary).

[F3]

$Ω_{0}^{O} ≅ Z / 2 Z$ with generator the class of a one-point manifold, the invariant being the parity of the cardinality; a compact zero-manifold bounds a compact one-manifold exactly when its cardinality is even (Zero-dimensional bordism groups).

[F4]

The bordism classes form an abelian group with $[M] + [N] = [M ⊔ N]$ and zero the class of the empty manifold; diffeomorphic closed manifolds have equal class (Disjoint union makes bordism classes abelian groups, Unoriented and oriented bordism groups, Diffeomorphisms and local diffeomorphisms of manifolds).

Verification

1.1F1F2F4

(Two points bound an interval.) By [F1], $W = [- 1, 1]$ is a compact smooth one-manifold with boundary $\partial W = {- 1, 1}$ . Define $θ : [0, 1) \times {- 1, 1} \to W$ by $θ (s, - 1) = - 1 + \frac{s}{2}$ and $θ (s, 1) = 1 - \frac{s}{2}$ ; the two images are the disjoint intervals $[- 1, - \frac{1}{2})$ and $(\frac{1}{2}, 1]$ , whose union is an open neighbourhood of $\partial W$ , and $θ (0, - 1) = - 1$ , $θ (0, 1) = 1$ , so $θ$ is a collar exhibiting all of $\partial W$ as the image of the source. Transporting this collar along the bijection ${a, b} \to {- 1, 1}$ gives a compact one-manifold whose whole boundary is ${a, b}$ with a collar. Hence the two-point manifold ${a, b}$ is null-cobordant, its class is zero, and $[p t] + [p t] = [p t ⊔ p t] = 0$ in $Ω_{0}^{O}$ .

1.2F3

(A single point is not null-cobordant.) By [F3] the parity of the cardinality is a complete invariant of $Ω_{0}^{O}$ and equals $1$ on a one-point manifold; hence the class of a point is nonzero, and a one-point manifold does not bound a compact one-manifold.

2.1F3step 1.1step 1.2∎

(The generator and the even case.) By [F3] the group $Ω_{0}^{O}$ has exactly two elements; step 1.1 shows that the nonzero class of a point is its own inverse, and step 1.2 shows that it is nonzero, so it is the unique nonzero element and generates $Ω_{0}^{O} ≅ Z / 2 Z$ . Finally, a closed zero-manifold with an even number of points has parity zero, so by [F3] it bounds a compact one-manifold and is null-cobordant.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

68 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)
Andrew Ranicki, Algebraic and Geometric Surgery (Oxford Mathematical Monographs, 2002) (standard reference, not scraped)