ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

Collapsing $k$ oriented disks realizes degree $k$

Example

Let $M$ be a nonempty closed connected oriented smooth $m$ -manifold, $m \geq 1$ , and let $k \in Z$ . Pick $∣ k ∣$ pairwise disjoint closed coordinate balls in $M$ . On each ball read the explicit smooth pinch model $F$ of Every integer is realized by a map to the sphere through a chart centred at that ball. Choose the chart sign so that $sgn (d F_{0}) sgn (d φ_{i}) = sgn (k)$ ; for this outward-normal-first sphere orientation, $sgn (d F_{0}) = (- 1)^{m + 1}$ . Extend by the same base point $N$ outside the balls. The resulting smooth map $f_{k} : M \to S^{m}$ has the point $y_{-} = F (0)$ of the model as a regular value whose preimage is exactly the set of centres of the chosen balls, one point per ball, so that $\deg (f_{k}) = \sum_{i = 1}^{∣ k ∣} sgn (d f_{k, p_{i}})$ . Choosing all local signs to be $sgn (k)$ gives $\deg (f_{k}) = k$ . For $k = \pm 1$ this is the pinch of a single oriented ball, and for $k = 0$ the empty family gives the constant map, of degree $0$ .

Facts & Assumptions

Given: A nonempty closed connected oriented smooth $m$ -manifold $M$ with $m \geq 1$ , an integer $k$ , the unit sphere $S^{m} \subseteq R^{m + 1}$ with its standard orientation for which the outward normal of the ball is first, and the explicit model pinch $F : R^{m} \to S^{m}$ of the realization lemma with its regular value $y_{-}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ , Induced boundary orientation).

[F1]

For every integer $k$ there is a smooth map $M \to S^{m}$ of degree $k$ , constructed by reading the smooth model pinch $F$ in $∣ k ∣$ pairwise disjoint closed coordinate balls (with a chart orientation chosen for the desired local sign) and extending by the base point; the model satisfies $F^{- 1} (y_{-}) = {0}$ , $d F_{0}$ invertible, and $F = N$ outside the unit ball (Every integer is realized by a map to the sphere).

[F2]

For a proper smooth map $f : M \to S^{m}$ with $M$ a nonempty connected oriented closed manifold, a regular value $y$ with finite fibre gives $\deg (f) = \sum_{x \in f^{- 1} (y)} sgn (d f_{x})$ , where $\deg$ is the compact-support degree and the signs use the orientations of source and target (Regular-value formula for degree, Degree of a proper smooth map by compact-support cohomology).

[F3]

A chart of the oriented manifold $M$ is orientation-preserving or orientation-reversing, and the sign of the chart multiplies the local orientation sign of a composition with the chart; $S^{m}$ carries the stated orientation (Orientation-preserving parametrizations, Oriented smooth manifolds and oriented charts, Induced boundary orientation).

Verification

technique · direct

1.1F1given

The realization lemma supplies exactly the objects described: the model $F$ with $F^{- 1} (y_{-}) = {0}$ , $d F_{0}$ invertible and $F = N$ off the unit ball, and the glued map $f_{k}$ which equals $F$ read through the $i$ -th chart near the centre $p_{i}$ and $N$ elsewhere; its construction and its smoothness are those verified there.

1.2F1given

The preimage of $y_{-}$ under $f_{k}$ is exactly ${p_{1}, \dots, p_{∣ k ∣}}$ : each centre gives a preimage by $F (0) = y_{-}$ , the model has no other preimage of $y_{-}$ inside the unit ball, and points outside the balls as well as points of a ball mapping outside the unit ball have value $N \neq y_{-}$ ; the differential $d f_{k, p_{i}} = d F_{0} \circ d φ_{i}$ is invertible, so $y_{-}$ is a regular value and $f_{k}$ is proper because $M$ is compact.

2.1F2F3step 1.2algebra∎

By step 1.2 and [F2], $\deg (f_{k}) = sgn (d F_{0}) \sum_{i = 1}^{∣ k ∣} ε_{i}$ with $ε_{i} = \pm 1$ the orientation sign of the $i$ -th chart, by [F3]; choosing every chart so that $sgn (d F_{0}) ε_{i} = sgn (k)$ makes the sum equal to $k$ . For $k = 0$ there is no ball and $f_{0} = N$ is constant, with an empty regular fibre over any point different from $N$ , so $\deg (f_{0}) = 0$ . This realizes every prescribed degree by collapsing oriented disks with the prescribed local signs.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

Victor Guillemin and Alan Pollack, Differential Topology (standard reference, not scraped)
Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (standard reference, not scraped)

Collapsing kk oriented disks realizes degree kk