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.
Nearest-point projection is the tubular retraction after shrinking
Statement
Assume countable choice. Let be a closed embedded smooth submanifold. After shrinking the tubular neighbourhood from the Euclidean tubular neighbourhood theorem, the tubular retraction agrees with the unique nearest-point projection onto .
Facts & Assumptions
Given: Countable choice and a closed embedded smooth submanifold .
Under countable choice (The Axiom of Countable Choice ()), the Euclidean tubular theorem constructs with a positive radius satisfying , where is a diffeomorphism on each local set for (The Euclidean tubular neighbourhood theorem, proof steps 2.1–4.1).
The tubular retraction is , where is the normal-bundle projection (directly from [L1]).
Proof
If is empty the assertion is vacuous. Otherwise fix in the tube from [L1]. Since is closed, the continuous distance function to attains a minimum on the compact set ; let be a minimizer. Because , . The first derivative of along every tangent vector at vanishes, so and .
The triangle inequality gives . Also . Choose with . Both and then lie in , on which [L1] makes injective. Since they have the same image , they coincide, and in particular . The same argument applies to any minimizing , so the nearest point is unique.
By [L2], . Step 2.1 shows that is exactly the unique nearest point. The theorem’s constructed tube already has this property, hence so does any smaller tube.