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.

Framed zero-manifolds and signed points

Example

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). For $n \geq 1$ , a closed framed $0$ -dimensional submanifold of $S^{n}$ is a finite set of points (zero-dimensional charts make the singletons open, and compactness gives a finite singleton subcover), each framed by a basis of $T_{x} S^{n}$ (the normal bundle of a point is the whole tangent space, Framings of a normal bundle). Call the framing positive when that basis is positively oriented for the standard orientation of $S^{n}$ , and let $sgn (x) = \pm 1$ accordingly. Framed cobordism classes of such points are classified by the signed count $\sum_{x} sgn (x) \in Z :$ under the fixed-codimension correspondence with $k = n$ the signed count is the degree of the Pontryagin-Thom map $S^{n} \to S^{n}$ , and $π_{n} (S^{n}) ≅ Z$ by degree. A single positively framed point realizes $+ 1$ , its orientation reversal $- 1$ , and the empty $0$ -manifold $0$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , an integer $n \geq 1$ , the standard oriented sphere $S^{n}$ , and a closed framed $0$ -submanifold $P = {(x_{i}, φ_{i})}$ of $S^{n}$ with finitely many points.

[F1]

The normal bundle of a point $x \in S^{n}$ is $T_{x} S^{n}$ ; a framing is a basis, and reversing one vector changes the orientation class (Framings of a normal bundle, Orientation of a finite-dimensional real vector space).

[F2]

The Pontryagin-Thom map of a framed point $(x, φ)$ is smooth and equals the composite of the framing with the radial collapse of a small tube; the centre $y_{0}$ is a regular value with preimage ${x}$ , and the sign of the differential there is $+ 1$ for a positive framing and $- 1$ for a negative one (The Pontryagin-Thom map of a framed submanifold, Framed regular preimages of a map to a sphere).

[F3]

For a proper smooth map between nonempty connected closed oriented $n$ -manifolds, the degree is computed at any regular value as the sum of the signs of the differential over the finite preimage (Regular-value formula for degree, Based sphere maps are classified by degree).

[F4]

The Pontryagin-Thom correspondence with $n = k \geq 1$ is a bijection from framed cobordism classes of closed framed $0$ -submanifolds of $S^{n}$ to $π_{n} (S^{n})$ , and degree is an isomorphism $π_{n} (S^{n}) \to Z$ (The Pontryagin-Thom correspondence in fixed codimension, Based sphere maps are classified by degree).

Verification

1.1F1F2F3

(A single framed point has degree $\pm 1$ .) Let $(x, φ)$ be a framed point and let $f = f_{(x, φ)}$ be its Pontryagin-Thom map. By [F2], $f$ is smooth, the centre $y_{0}$ is a regular value and $f^{- 1} (y_{0}) = {x}$ ; the differential of $f$ at $x$ is the framing composed with the orientation-preserving identification of $R^{n}$ with $T_{y_{0}} S^{n}$ , so its sign is $+ 1$ when the basis $φ$ is positive and $- 1$ when it is negative. By the regular-value formula [F3], $\deg (f) = + 1$ in the first case and $\deg (f) = - 1$ in the second: a positively framed point realizes $+ 1$ and its orientation reversal $- 1$ .

2.1F2F3givenstep 1.1

(Finite unions and the signed count.) For a finite framed $0$ -manifold $P = {(x_{1}, φ_{1}), \dots, (x_{m}, φ_{m})}$ choose pairwise disjoint tubes around the points and use the normalized smooth single-point collapses of [F2] on them, sending their complement to the basepoint. Each collapse is constant near its tube boundary, so the resulting map $f_{P} : S^{n} \to S^{n}$ is smooth everywhere. Its centre preimage is $P$ , and at $x_{i}$ its differential induces $φ_{i}$ , with local sign $sgn (x_{i})$ by step 1.1. Thus $y_{0}$ is regular, including when $P$ is empty. Since $n \geq 1$ , both spheres are nonempty connected closed oriented manifolds, and $f_{P}$ is proper by compactness. The regular-value formula [F3] therefore gives $\deg f_{P} = \sum_{i} sgn (x_{i})$ , including the empty sum zero.

3.1F1F4step 1.1step 2.1∎

(Classification.) By the correspondence of [F4] two closed framed $0$ -manifolds of $S^{n}$ are framed cobordant if and only if their Pontryagin-Thom maps are homotopic, and by [F4] homotopy classes of based self-maps of $S^{n}$ are classified by degree. By step 2.1 the degree of the Pontryagin-Thom map of $P$ is exactly the signed count, so the framed cobordism class of $P$ is determined by $\sum_{x} sgn (x)$ and every integer occurs: for $m \in Z$ take $∣ m ∣$ distinct points framed positively if $m > 0$ and negatively if $m < 0$ , and the empty set for $m = 0$ . Hence framed cobordism classes of framed $0$ -manifolds are classified by the signed count.

Depends on

Used by

Nothing in the library uses this result yet.

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

John Milnor, Topology from the Differentiable Viewpoint (standard reference, not scraped)
Andrew Ranicki, Algebraic and Geometric Surgery (Oxford Mathematical Monographs, 2002) (standard reference, not scraped)
Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)