TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-09-07

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.

Boundary-tangent fields have boundary-preserving local two-sided flows

Statement

Let $M$ be a smooth manifold with boundary and let $X$ be a smooth vector field on $M$ tangent to $\partial M$ . Then $X$ has a local two-sided ambient flow, and every defined time slice preserves $\partial M$ .

Facts & Assumptions

Given: A smooth manifold $M$ with boundary and a smooth vector field $X$ on $M$ satisfying $X_{p} \in T_{p} \partial M$ for every $p \in \partial M$ .

[L1]

A smooth vector field on a boundaryless manifold has a unique maximal local flow with open time-state domain (The fundamental theorem on flows).

[L2]

The flow of a vector field tangent to a closed embedded submanifold preserves that submanifold (The flow of a vector field tangent to a closed embedded submanifold preserves it).

[L3]

The boundary tangent space is the last-coordinate-zero hyperplane in a boundary chart (The boundary tangent space is the boundary-tangent hyperplane).

Proof

technique · direct

1.1

Fix a boundary point and extend the coordinate components of $X$ smoothly across the face of a boundary chart. By [L1], the extended Euclidean field has a unique two-sided local flow near that point.

givenL1

2.1

By [L3], the extended field is tangent to the face along the face. Applying [L2] in the Euclidean chart shows that its flow preserves the face. Each sufficiently small time slice is a local diffeomorphism with inverse the negative-time slice, so an interior point cannot cross the invariant face without violating injectivity. After shrinking the flow domain, it therefore preserves the half-space and restricts to a two-sided local flow on $M$ preserving $\partial M$ .

L2L3step 1.1∎

Depends on

Used by

Every boundary vector field has a local two-sided flow inside the manifold False statement

Dependency tree · two levels

15 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

Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1 (standard reference, not scraped)
Will Merry, Differential Geometry (2021), Lecture 24 (standard reference, not scraped)