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.

Source, sink and saddle indices on a surface

Example

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the canonical smooth tangent-bundle structure.

On a chart of a surface identified with $R^{2}$ consider the smooth vector fields (A smooth vector field is a smooth section of the tangent bundle) $X_{1} (x, y) = (x, y), X_{2} (x, y) = (- x, - y), X_{3} (x, y) = (x, - y) .$ Each has its only zero at the origin, with linearizations $I$ , $- I$ and $diag (1, - 1)$ ; by The index of a nondegenerate vector-field zero the indices are ${ind}_{0} X_{1} = sign \det I = + 1, {ind}_{0} X_{2} = sign \det (- I) = + 1, {ind}_{0} X_{3} = sign \det diag (1, - 1) = - 1.$ Thus the source and the sink of a surface field both have index $+ 1$ , while the saddle has index $- 1$ , matching the circulation, source, sink and saddle pictures of the classical treatment.

Facts & Assumptions

Given: The plane $R^{2}$ as a chart of a surface and the three displayed linear fields $X_{1}, X_{2}, X_{3}$ on it.

[F1]

A zero of a smooth field is nondegenerate when its linearization $D X_{p}$ is invertible, and then it is isolated (Nondegenerate zero of a vector field, Isolated zero and local index of a vector field).

[F2]

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

Verification

1.1F1algebra

The fields $X_{1}, X_{2}, X_{3}$ are linear, so their derivatives at every point are the matrices $I$ , $- I$ and $diag (1, - 1)$ ; each matrix is invertible, and $X_{i} (u) = A_{i} u = 0$ has the unique solution $u = 0$ since $A_{i}$ is invertible, so the origin is the only zero of each field and it is nondegenerate.

2.1F2step 1.1algebra∎

The determinants are $\det I = 1$ , $\det (- I) = (- 1)^{2} = 1$ and $\det diag (1, - 1) = - 1$ , so [F2] gives the displayed indices $+ 1, + 1, - 1$ ; in particular a source and a sink on a surface both contribute $+ 1$ , and a saddle contributes $- 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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 (Prentice-Hall 1974; complete PDF) (standard reference, not scraped)
John W. Milnor, Topology from the Differentiable Viewpoint (complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)