LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Framed points in one component of the frame bundle are framed cobordant

Statement

Assume ${A C}_{ω}$ . Let $M$ be a closed smooth $m$ -manifold, $m \geq 1$ , and let $c : [0, 1] \to B (M)$ be a smooth path in the frame bundle from $(x_{0}, b_{0})$ to $(x_{1}, b_{1})$ . Then the framed points $(x_{0}, b_{0})$ and $(x_{1}, b_{1})$ , regarded as closed framed $0$ -dimensional submanifolds of $M$ of codimension $m$ with framings $b_{i} : R^{m} \to T_{x_{i}} M$ , are framed cobordant in $M$ .

Facts & Assumptions

Given: A closed smooth $m$ -manifold $M$ , $m \geq 1$ , points $x_{0}, x_{1} \in M$ , linear isomorphisms $b_{i} : R^{m} \to T_{x_{i}} M$ , and a smooth path $c : [0, 1] \to B (M)$ with $c (0) = (x_{0}, b_{0})$ , $c (1) = (x_{1}, b_{1})$ (The frame bundle of a smooth manifold).

[F1]

The frame bundle $B (M)$ is a smooth manifold with smooth projection $π$ and smooth right action; writing $c (s) = (x (s), b (s))$ , both $s \mapsto x (s)$ and $s \mapsto b (s)$ are smooth, and composing $c$ with a smooth nondecreasing reparametrization $λ : [0, 1] \to [0, 1]$ with $λ = 0$ near $0$ and $λ = 1$ near $1$ gives a smooth path with the same endpoints that is constant near the ends (The frame bundle of a smooth manifold, Smooth embeddings, The chain rule for differentials of smooth maps). The interval is compact and its graph image is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[F2]

A framed cobordism from a closed framed codimension- $k$ submanifold $(N_{0}, φ_{0})$ to $(N_{1}, φ_{1})$ in a closed $X$ is data $(W, ε, Ψ)$ : a compact neat embedded $W \subseteq X \times I$ with $\partial W = N_{0} \times {0} ⊔ N_{1} \times {1}$ , product ends $W \cap (X \times [0, ε)) = N_{0} \times [0, ε)$ and $W \cap (X \times (1 - ε, 1]) = N_{1} \times (1 - ε, 1]$ , and a framing $Ψ$ of $ν (W \subseteq X \times I)$ the pullback of $φ_{i}$ over each end collar, along which the $I$ -direction is tangent to $W$ (Framed cobordism of framed submanifolds, Framings of a normal bundle, Normal and conormal bundles of an embedded submanifold, Neat submanifolds of a manifold with boundary, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · constructive

1.1F1givenconstruct

Choose a smooth nondecreasing $λ : [0, 1] \to [0, 1]$ given explicitly by $λ (t) = σ (3 t - 1)$ , with $σ$ the standard smooth step function (The standard smooth step function) and $ε = 1 / 8$ , and replace $c$ by the reparametrized smooth path $c \circ λ$ with the same endpoints, so that $x (λ (t)) = x_{0}$ and $b (λ (t)) = b_{0}$ for $t \leq ε$ and $x (λ (t)) = x_{1}$ , $b (λ (t)) = b_{1}$ for $t \geq 1 - ε$ .

2.1F1step 1.1given

Define $W : = {(x (λ (t)), t) : t \in [0, 1]} \subseteq M \times I$ . The map $t \mapsto (x (λ (t)), t)$ is smooth and injective (the second coordinate separates points) with derivative having second component $1 \neq 0$ , so $W$ is a compact embedded $1$ -submanifold with boundary the two endpoints $(x_{0}, 0)$ and $(x_{1}, 1)$ ; it is neat in $M \times [0, 1]$ , and by step 1.1 its ends are exactly $W \cap (M \times [0, ε)) = {x_{0}} \times [0, ε)$ and $W \cap (M \times (1 - ε, 1]) = {x_{1}} \times (1 - ε, 1]$ .

3.1F2step 1.1step 2.1

Write $γ (t) = x (λ (t))$ . At $(γ (t), t)$ define $Q_{t} : T_{γ (t)} M \oplus R \to T_{γ (t)} M$ by $Q_{t} (v, a) = v - a \dot{γ} (t)$ . Its kernel is precisely $R (\dot{γ} (t), 1) = T_{(γ (t), t)} W$ , and it is surjective since $Q_{t} (v, 0) = v$ ; hence it induces a smooth isomorphism of the normal quotient with $T_{γ (t)} M$ . The framing is $Ψ_{t} = b (λ (t))^{- 1} \circ Q_{t}$ on that quotient. On each end collar $\dot{γ} = 0$ and $b (λ (t)) = b_{i}$ , so $Ψ$ is exactly the product pullback of $φ_{i} = b_{i}^{- 1}$ . This supplies the required quotient map and the framing in the trivialization direction of [F2].

4.1F2step 3.1discharge-construct∎

Therefore $(W, ε, Ψ)$ satisfies all the data of a framed cobordism from the framed point $(x_{0}, φ_{0})$ to $(x_{1}, φ_{1})$ in the sense of [F2], and reading the framings through the frame-bundle dictionary the two framed points $(x_{0}, b_{0})$ and $(x_{1}, b_{1})$ are framed cobordant. No choice beyond the inherited countable choice and the finite choice of $λ$ and $ε$ is used.

Depends on

Used by

Dependency tree · two levels

86 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

Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (standard reference, not scraped)