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

The outward radial field on a disk

Example

Assume the Axiom of Choice (The Axiom of Choice) for the applications of Poincare-Hopf below.

On the closed unit ball $D^{n} = {\overline{B}}_{2} (0, 1) \subseteq R^{n}$ , $n \geq 1$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ), the radial field $X (u) = u$ points strictly outward along $\partial D^{n}$ (Inward, outward, and boundary-tangent vectors) and has its only zero at the centre, nondegenerate with linearization $I_{n}$ and index $sign \det I_{n} = + 1$ (The index of a nondegenerate vector-field zero). Since $D^{n}$ is contractible, $H_{0} (D^{n}; Q) ≅ Q$ and all higher rational homology vanishes (Contractible nonempty spaces have the homology of a point), so $χ (D^{n}) = 1$ (Euler characteristic of a compact manifold); the index sum $+ 1$ equals $χ (D^{n})$ , verifying the boundary form Poincare-Hopf with outward-pointing boundary in the simplest case.

Facts & Assumptions

Given: The closed unit ball $D^{n} \subseteq R^{n}$ , $n \geq 1$ , and the radial field $X (u) = u$ (A smooth vector field is a smooth section of the tangent bundle).

[F1]

At a boundary point $u \in \partial D^{n}$ the outward direction is the radial direction $u$ , and $X (u) = u$ has positive inner product with it (Inward, outward, and boundary-tangent vectors).

[F2]

A nondegenerate zero has index $sign \det (D X_{p})$ (The index of a nondegenerate vector-field zero).

[F3]

For a contractible space the rational homology is that of a point, so $χ (D^{n}) = 1$ , and the boundary form of Poincare-Hopf gives $\sum_{p} {ind}_{p} X = χ (D^{n})$ for a strictly outward field (Contractible nonempty spaces have the homology of a point, Euler characteristic of a compact manifold, Poincare-Hopf with outward-pointing boundary).

Verification

1.1F2algebra

The field $X$ is linear with $D X_{u} = I_{n}$ , invertible at every point, so its only zero is the centre $0$ and that zero is nondegenerate; by [F2] its index is $sign \det I_{n} = + 1$ , so the index sum is $+ 1$ .

2.1F1F3step 1.1algebra∎

On the boundary sphere the outward normal is the radial vector $u$ , so $⟨ X (u), u ⟩ = ∣ u ∣^{2} = 1 > 0$ and the field is strictly outward by [F1]; by [F3] the index sum equals $χ (D^{n})$ , and the value $+ 1$ computed in step 1.1 matches $χ (D^{n}) = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

46 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 W. Milnor, Topology from the Differentiable Viewpoint (complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)
Joel W. Robbin and Dietmar A. Salamon, Introduction to Differential Topology (web draft 2018, complete PDF) (standard reference, not scraped)