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.

Euler and first Pontryagin classes of $ξ_{h, j}$

Statement

Assume the Axiom of Choice as inherited from the characteristic-class suppliers. Under the fixed quaternionic, base and upper-to-lower clutching orientations of Quaternionic clutching bundles $ξ_{h, j}$ over $S^{4}$ , the bundle $ξ_{h, j}$ has $e (ξ_{h, j}) = (h + j) u, p_{1} (ξ_{h, j}) = 2 (h - j) u \in H^{4} (S^{4}; Z),$ where $u$ is the positive base generator.

Facts & Assumptions

Given: Integers $h, j$ , the bundle $ξ_{h, j}$ and the generator $u \in H^{4} (S^{4}; Z)$ with $⟨ u, [S^{4}] ⟩ = 1$ .

[A1]

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

[L1]

The clutching map satisfies $g_{h, j} (a) v = a^{h} v a^{j}$ , so for $h, j \geq 0$ it is the pointwise product of $h$ copies of $g_{1, 0}$ and $j$ copies of $g_{0, 1}$ ; for negative exponents the same holds with the corresponding inverse maps, and $g_{- 1, 0} = g_{1, 0}^{- 1}$ , $g_{0, - 1} = g_{0, 1}^{- 1}$ (Quaternionic clutching bundles $ξ_{h, j}$ over $S^{4}$ ).

[L2]

The Euler and first Pontryagin evaluations of the bundle clutched by a pointwise product are the sums of the evaluations of the factors, and inversion negates them (Degree-four characteristic evaluations add under the clutching product).

[L3]

The basic left and right bundles satisfy $e = u$ and $p_{1} = + 2 u$ (left) and $e = u$ , $p_{1} = - 2 u$ (right) (Pontryagin calibration of the basic quaternionic clutchings).

[L4]

Evaluation against the fundamental class is additive and, since $H^{4} (S^{4}; Z) = Z \cdot u$ with $⟨ u, [S^{4}] ⟩ = 1$ , determines a degree-four class (Kronecker evaluation pairing).

Proof

technique · direct

1.1L1L2L3A1

For $h, j \geq 0$ , [L1] writes $g_{h, j}$ as the pointwise product of $h$ copies of $g_{1, 0}$ and $j$ copies of $g_{0, 1}$ ; applying [L2] inductively with the basic values [L3] gives $⟨ e (ξ_{h, j}), [S^{4}] ⟩ = h \cdot 1 + j \cdot 1 = h + j$ and $⟨ p_{1} (ξ_{h, j}), [S^{4}] ⟩ = h \cdot 2 + j \cdot (- 2) = 2 (h - j)$ .

2.1step 1.1L1L2

For arbitrary integers $h, j$ , write the clutching as the same product with the inverse maps for the negative exponents; the inverse clause of [L2] negates both evaluations, so the displayed evaluations remain $⟨ e (ξ_{h, j}), [S^{4}] ⟩ = h + j$ and $⟨ p_{1} (ξ_{h, j}), [S^{4}] ⟩ = 2 (h - j)$ .

3.1step 2.1L4∎

By [L4] a degree-four integral class on $S^{4}$ is determined by its evaluation on $[S^{4}]$ , and $⟨ (h + j) u, [S^{4}] ⟩ = h + j$ , $⟨ 2 (h - j) u, [S^{4}] ⟩ = 2 (h - j)$ ; comparing with step 2.1 gives $e (ξ_{h, j}) = (h + j) u$ and $p_{1} (ξ_{h, j}) = 2 (h - j) u$ , as asserted.

Depends on

Used by

Dependency tree · two levels

24 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, Vector Bundles & K-Theory, section 1.2 (standard reference, not scraped)

Euler and first Pontryagin classes of ξh,jξh,j​