ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 normal line of an oriented hypersurface is trivial

Example

Assume AC. Let $M^{m} \subseteq R^{m + 1}$ be a closed embedded hypersurface that is oriented (for example the unit sphere $S^{m}$ ). The standard orientation of $R^{m + 1}$ and the orientation of $M$ determine an orientation of the normal line bundle (An oriented transverse normal bundle orients an embedded submanifold, Orientable manifolds); an oriented real line bundle is trivial, because the smooth Euclidean normal metric (Assuming countable choice, an ambient metric identifies the two normal bundles) and its positive unit vector give a nowhere-zero global section (A vector bundle is trivial if and only if it has a global frame, Local and global frames of a vector bundle). Hence the normal bundle of the embedding is trivial, ${\overset{ˉ}{w}}_{1} (M) = 0$ , ${\overset{ˉ}{w}}_{i} (M) = 0$ for $i \geq 2$ by rank, and $\overset{ˉ}{p} (M) = 1$ (An embedding into Euclidean space gives a rank-(n-m) stable normal inverse, Normal Stiefel-Whitney and Pontryagin classes of a closed manifold): the rank-one characteristic-class tests give no obstruction to codimension-one immersions or embeddings of an oriented hypersurface, since a nowhere-zero normal section forces the Euler class to vanish (A nowhere-zero section forces the Euler class to vanish, Euler class by zero-section pullback of the Thom class). In particular for $S^{m}$ one also has $T S^{m} \oplus ε^{1} ≅ ε^{m + 1}$ , so $\overset{ˉ}{w} (S^{m}) = 1$ and $\overset{ˉ}{p} (S^{m}) = 1$ .

Facts & Assumptions

Given: A closed oriented embedded hypersurface $M^{m} \subseteq R^{m + 1}$ with its normal line bundle $ν$ , and AC (The Axiom of Choice).

[F1]

For an embedded submanifold, any two of the orientations of the ambient tangent bundle, the tangent bundle and the transverse normal bundle determine the third; here the standard orientation of $R^{m + 1}$ and the orientation of $M$ determine an orientation of $ν$ (An oriented transverse normal bundle orients an embedded submanifold, Orientable manifolds). The statement assumes the countable choice ${A C}_{ω}$ used by the normal-bundle identifications, which AC supplies (AC implies DC implies countable choice).

[F2]

The standard Euclidean metric induces a smooth metric on the orthogonal normal line, smoothly identified with the quotient (Assuming countable choice, an ambient metric identifies the two normal bundles). On an oriented local frame $v$ , the positive unit vector is $v / \sqrt{⟨ v, v ⟩}$ ; it is smooth and independent of the positive frame, so these vectors give a smooth global section (Smoothness of a section is equivalent to smooth local components). A rank-one global frame trivializes the bundle (A vector bundle is trivial if and only if it has a global frame, Local and global frames of a vector bundle).

[F3]

The normal bundle of an embedding into $R^{N}$ is a rank- $(N - m)$ stable normal inverse, so its Stiefel-Whitney and Pontryagin classes are the normal classes $\overset{ˉ}{w} (M)$ and $\overset{ˉ}{p} (M)$ ; in rank one this gives ${\overset{ˉ}{w}}_{i} (M) = 0$ for $i > 1$ and the top class in degree one otherwise (An embedding into Euclidean space gives a rank-(n-m) stable normal inverse, Normal Stiefel-Whitney and Pontryagin classes of a closed manifold).

[F4]

A nowhere-zero section of an oriented rank-one numerable bundle forces its Euler class to vanish: if $ν$ has a nowhere-zero section then $e (ν) = 0$ (A nowhere-zero section forces the Euler class to vanish, Euler class by zero-section pullback of the Thom class).

[F5]

The unit sphere $S^{m} = {x \in R^{m + 1} : ∣ x ∣ = 1}$ is a closed embedded hypersurface of $R^{m + 1}$ with $T_{x} S^{m} = x^{⊥}$ : it is the level set of the smooth function $x \mapsto ⟨ x, x ⟩$ at the regular value $1$ , whose differential $2 ⟨ x, \cdot ⟩$ is nonzero at every $x \in S^{m}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ , A regular level set is an embedded submanifold, The tangent space of a regular level set is the kernel). Under the Euclidean metric the normal line of this embedding is identified with the orthogonal complement of $T S^{m}$ (Assuming countable choice, an ambient metric identifies the two normal bundles, Normal and conormal bundles of an embedded submanifold), and the radial field $x \mapsto x$ is a nowhere-zero section of that line, smooth because in the standard global frame of the restricted trivial bundle its coefficients are the coordinate functions (Smoothness of a section is equivalent to smooth local components).

Verification

technique · direct

1.1F1

By [F1] the standard orientation of $R^{m + 1}$ together with the orientation of $M$ orients the normal line bundle $ν$ : the orientation of the ambient bundle and of the tangent bundle determine that of the rank-one transverse normal bundle. This is the coorientation of the hypersurface, and it is a datum determined by the two given orientations.

2.1F1F2step 1.1

Use the Euclidean metric on the orthogonal normal line of $M$ . By [F2] its positive unit vectors form a smooth nowhere-zero section: on overlaps two positive frames differ by a positive smooth function, which cancels on normalization. This is a global frame, so $ν ≅ ε^{1}$ smoothly.

3.1F2F3step 2.1

Consequently the normal bundle of the embedding is trivial, and by [F3] the normal line bundle realizes the normal classes of $M$ : ${\overset{ˉ}{w}}_{1} (M) = w_{1} (ν) = 0$ because the trivial bundle has trivial total class, and ${\overset{ˉ}{w}}_{i} (M) = w_{i} (ν) = 0$ for every $i \geq 2$ by the rank convention for a rank-one bundle; likewise $\overset{ˉ}{p} (M) = p (ν) = 1$ . Thus the degree-one and higher normal classes give no obstruction to a codimension-one immersion or embedding of $M$ .

3.2F2F4step 2.1

The Euler class of the normal line also vanishes: the section exhibited in step 2.1 is nowhere zero, so [F4] gives $e (ν) = 0$ . Hence a nonzero normal Euler class is likewise no obstruction here, and every rank-one characteristic-class test of the page returns zero for an oriented hypersurface.

4.1F2F3F5step 3.1∎

For the unit sphere $S^{m}$ the outward normal field $x \mapsto x$ of [F5] is a nowhere-zero global section of the normal line, hence a global frame, so the normal bundle of the inclusion is trivial by [F2] and [F5]; combined with the embedding normal identity [F3] this gives $T S^{m} \oplus ε^{1} ≅ ε^{m + 1}$ for the sphere's stable normal inverse, whence $\overset{ˉ}{w} (S^{m}) = 1$ and $\overset{ˉ}{p} (S^{m}) = 1$ as in step 3.1. The argument applies to every oriented hypersurface, uses AC through the Euler and characteristic-class suppliers and its countable-choice consequence through the normal-bundle identifications, and asserts nothing about embeddability in higher codimension or about uniqueness of embeddings.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

72 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 and James D. Stasheff, Characteristic Classes (Annals of Mathematics Studies 74, Princeton University Press; complete text) (standard reference, not scraped)
Ralph L. Cohen, Immersions of Manifolds and Homotopy Theory (lecture notes, 30 June 2022; complete 46-page text) (standard reference, not scraped)
Arkadiy Skopenkov, Embedding and Knotting of Manifolds in Euclidean Spaces (arXiv:math/0604045) (standard reference, not scraped)