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

Relative Pontryagin square of the Milnor disk bundle

Statement

Assume the Axiom of Choice as inherited from the Thom and characteristic-class suppliers. Let $h + j = ε \in {+ 1, - 1}$ and $k = h - j$ . Then the first Pontryagin class $p_{1} (T W_{h, j})$ has a unique relative lift ${\overset{ˉ}{p}}_{1} \in H^{4} (W_{h, j}, M_{h, j}; Z)$ , and $q (W_{h, j}) : = ⟨ {\overset{ˉ}{p}}_{1} ⌣ {\overset{ˉ}{p}}_{1}, [W_{h, j}, M_{h, j}] ⟩ = 4 ε k^{2} .$

Facts & Assumptions

Given: Integers $h, j$ with $ε = h + j = \pm 1$ , $k = h - j$ , the disk bundle $W = D (ξ_{h, j})$ , its boundary $M = S (ξ_{h, j})$ , the projection $π$ , the classes $x = π^{*} u$ and the Thom generator $U$ .

[A1]

The Axiom of Choice is assumed (The Axiom of Choice).

[L1]

$e (ξ_{h, j}) = ε u$ and $p_{1} (ξ_{h, j}) = 2 k u$ (Euler and first Pontryagin classes of $ξ_{h, j}$ ).

[L2]

$p_{1} (T W) = 2 k x$ with $x = π^{*} u$ (Stable splitting of the tangent bundle of the Milnor disk bundle).

[L3]

The Thom theorem gives $H^{4} (W, M; Z) = Z \cdot U$ and $H^{4} (W; Z) = Z \cdot x$ . Since the zero section and projection are homotopy inverses, the Euler-class identity $s^{*} j (U) = e (ξ_{h, j})$ gives $j (U) = π^{*} e (ξ_{h, j})$ in $H^{4} (W; Z)$ (Thom isomorphism for oriented vector bundles, Euler class by zero-section pullback of the Thom class, The Milnor sphere and disk bundles $M_{h, j}$ and $W_{h, j}$ ).

[L4]

The normalized evaluation satisfies $⟨ U ⌣ x, [W, M] ⟩ = 1$ (The Thom class of a disk bundle pairs with the base generator to one).

[L5]

For $a \in H^{4} (W, M; Z)$ , $⟨ a ⌣ a, [W, M] ⟩ = ⟨ a ⌣ j (a), [W, M] ⟩$ and the mixed evaluation uses the relative cup product (The relative square equals the mixed evaluation, Relative cup product for an excisive triad).

Proof

technique · direct

1.1L1L2L3A1

By [L3] and [L1] the map $j$ sends the generator $U$ to $ε x$ with $ε = \pm 1$ , so it is an isomorphism and $p_{1} (T W) = 2 k x$ of [L2] has the unique relative lift ${\overset{ˉ}{p}}_{1} = 2 k ε U$ .

2.1step 1.1L4L5∎

Using [L5] and [L4], $q (W) = ⟨ (2 k ε U) ⌣ (2 k x), [W, M] ⟩ = 4 ε k^{2} ⟨ U ⌣ x, [W, M] ⟩ = 4 ε k^{2}$ , since the mixed evaluation equals the relative square.

Depends on

Used by

Dependency tree · two levels

45 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 Milnor, On Manifolds Homeomorphic to the 7-Sphere, Annals of Mathematics 64 (1956), 399-405 (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, Cambridge University Press 2002 (complete book) (standard reference, not scraped)