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.

Signed points give the oriented zero-bordism invariant

Example

For a closed oriented zero-manifold $M = ∐_{x} {x}$ with signs $ϵ_{x} \in {\pm 1}$ determined by the orientation, the integer $\sum_{x} ϵ_{x}$ is unchanged by oriented cobordism, and the map $[M] \mapsto \sum_{x} ϵ_{x}$ is an isomorphism $Ω_{0}^{S O} \to Z$ . A positively oriented point is a generator, and the standard interval $[- 1, 1]$ with suitable collars realizes $[{p t}_{+}] + [{p t}_{-}] = 0$ with the sign convention of the page, so $[{p t}_{-}] = - [{p t}_{+}]$ . Consequently two finite oriented point sets are oriented cobordant exactly when their signed counts agree (Zero-dimensional bordism groups, Unoriented and oriented bordism groups).

Facts & Assumptions

Given: A closed oriented zero-manifold $M = ∐_{x} {x}$ with signs $ϵ_{x}$ , the interval $[- 1, 1]$ with its standard orientation, and the oriented bordism classes of closed oriented zero-manifolds.

[F1]

With the standard orientation on $[a, b]$ , the induced boundary orientation is ${b} - {a}$ : the endpoint $b$ is positive and $a$ is negative (Boundary orientation is independent of the outward vector field, Induced boundary orientation); the closed ball $B^{1} = [- 1, 1] = {x : 1 - x^{2} \geq 0}$ is a compact smooth one-manifold with boundary ${- 1, 1}$ by the nonzero derivative of $1 - x^{2}$ at $\pm 1$ and the inverse function theorem (The Euclidean inverse function theorem, Euclidean upper half-space and its boundary, Smooth charts, atlases, and structures with boundary, Boundary-defining functions, Euclidean spheres and closed balls as subspaces of $R^{n}$ , For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact).

[F2]

An oriented bordism from $(M_{0}, o_{0})$ to $(M_{1}, o_{1})$ has induced boundary orientations $- o_{0}$ on the incoming and $o_{1}$ on the outgoing face, and a closed oriented manifold is null-cobordant exactly when it occurs as the negative of the induced boundary of a compact oriented one-manifold; collars are part of the bordism data (Oriented smooth cobordism, Null-cobordant closed manifolds, Smooth collars of a manifold boundary).

[F3]

The signed count $[M] \mapsto \sum_{x} ϵ_{x}$ is an isomorphism of abelian groups $Ω_{0}^{S O} \to Z$ with ${p t}_{+} \mapsto 1$ ; a compact oriented zero-manifold bounds a compact oriented one-manifold exactly when its signed count is zero; classes of orientation-preserving diffeomorphic closed oriented manifolds agree (Zero-dimensional bordism groups, Disjoint union makes bordism classes abelian groups, Unoriented and oriented bordism groups).

[F4]

The opposite orientation of a zero-manifold reverses every sign $ϵ_{x}$ , and the product orientation and boundary conventions of the page apply to the explicit interval model (Oriented smooth manifolds and oriented charts, Product orientations, Boundary orientation of a product with at most one boundary factor, Products of smooth manifolds have a canonical product smooth structure).

Verification

1.1F1F2F4

(The interval realizes $[{p t}_{+}] + [{p t}_{-}] = 0$ .) Let $x \neq y$ be two points and orient the zero-manifold ${x, y}$ so that $x$ is positive and $y$ is negative. On the compact interval $[- 1, 1]$ with its standard orientation the induced boundary orientation is ${1} - {- 1}$ by [F1], that is, the point $1$ is positive and the point $- 1$ is negative. Define the collar $θ : [0, 1) \times {x, y} \to [- 1, 1]$ by $θ (s, x) = - 1 + \frac{s}{2}$ and $θ (s, y) = 1 - \frac{s}{2}$ ; its images are disjoint open intervals around the two endpoints; taking the whole boundary as the incoming part, the induced orientation on the incoming face is ${y} - {x}$ , the negative of the source orientation. Hence $[- 1, 1]$ with this collar and orientation is an oriented null-cobordism of ${x, y}$ , and $[{p t}_{+}] + [{p t}_{-}] = 0$ in $Ω_{0}^{S O}$ .

2.1F3step 1.1∎

(The invariant, the generator and the consequences.) By [F3] the signed count is unchanged by oriented cobordism and defines an isomorphism $Ω_{0}^{S O} \to Z$ that sends a positively oriented point to $1$ . Step 1.1 shows $[{p t}_{-}] = - [{p t}_{+}]$ in the group, and this is consistent with the isomorphism because the two signed counts are $+ 1$ and $- 1$ . Finally, two finite oriented point sets have equal images under the isomorphism if and only if their signed counts agree, and since the isomorphism is injective this is exactly the condition that they are oriented cobordant; equivalently, their difference has signed count zero and is null-cobordant, again by [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 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

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