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.

Pontryagin calibration of the basic quaternionic clutchings

Statement

Assume the Axiom of Choice as inherited from the Chern and Pontryagin suppliers. Let $V_{L}$ be the oriented rank-four bundle over $S^{4}$ clutched by $a \mapsto (v \mapsto a v)$ and $V_{R}$ the one clutched by $a \mapsto (v \mapsto v a)$ , with the base, fibre and Euler-degree conventions of Quaternionic clutching bundles $ξ_{h, j}$ over $S^{4}$ . Then $e (V_{L}) = e (V_{R}) = u \in H^{4} (S^{4}; Z), p_{1} (V_{L}) = 2 u, p_{1} (V_{R}) = - 2 u .$

Facts & Assumptions

Given: The basic bundles $V_{L}, V_{R}$ of Quaternionic clutching bundles $ξ_{h, j}$ over $S^{4}$ with the generator $u \in H^{4} (S^{4}; Z)$ .

[A1]

The Axiom of Choice is assumed as inherited from the Chern/Pontryagin suppliers (The Axiom of Choice).

[L1]

For the basic left and right quaternionic clutchings the Euler number is $+ 1$ , so $e (V_{L}) = e (V_{R}) = u$ (Euler number of a clutched bundle as the clutching degree, Quaternionic clutching bundles $ξ_{h, j}$ over $S^{4}$ ).

[L2]

The top Chern class of a complex rank- $n$ bundle equals the Euler class of its underlying real bundle in the complex orientation (Top Chern class equals Euler class of the underlying real bundle).

[L3]

A complex bundle $V$ has a canonical complex orientation of $V_{R}$ , natural under complex-linear isomorphisms; orientation reversal negates the Euler class (The complex orientation of the underlying real bundle).

[L4]

For a complex bundle $V$ , the conjugate satisfies $c_{i} (\overline{V}) = (- 1)^{i} c_{i} (V)$ , and the complexification of a real bundle is canonically isomorphic to its conjugate (Complexification is conjugation invariant, Pontryagin classes by complexification).

[L5]

Total Chern classes multiply under Whitney sums and vanish in degrees above the rank (Naturality, normalization, and Whitney sum for Chern classes).

Proof

technique · direct

1.1L1given

Write $V = V_{L}$ or $V = V_{R}$ with its complex structure: for $V_{L}$ right multiplication by $i$ commutes with left multiplication by every quaternion and makes $V_{L}$ a complex rank-two bundle; for $V_{R}$ left multiplication by $i$ plays the same role for right multiplication.

2.1step 1.1L4

The complexification $V_{C} = V \otimes_{R} C$ carries the complexified complex structure $J_{C}$ ; its $\pm i$ eigenspace projections are complex subbundles $E_{+} ≅ V$ and $E_{-} ≅ \overline{V}$ (locally over a trivializing chart they are the $\pm i$ eigenspaces of the constant matrix $J$ ), so $V_{C} ≅ V \oplus \overline{V}$ as complex bundles.

3.1step 2.1L4L5

By [L5] and step 2.1, $c_{2} (V_{C}) = c_{2} (V) + c_{2} (\overline{V}) = c_{2} (V) + c_{2} (V) = 2 c_{2} (V)$ because $c_{2}$ is even in the conjugate sign of [L4], and $c_{1}$ terms do not contribute in degree four on $S^{4}$ as $H^{2} (S^{4}) = 0$ .

4.1step 3.1L4A1

By the Pontryagin convention $p_{1} (V_{R}) = - c_{2} (V_{C}) = - 2 c_{2} (V)$ (the sign is the one fixed in [L4]).

5.1step 4.1L1L2L3

The complex orientation of $V_{L}$ is opposite to the fibre orientation: the commuting complex structure is right multiplication by $i$ , whose complex basis $(1, j)$ gives the real ordered basis $(1, i, j, - k)$ , the negative of the fixed fibre basis $(1, i, j, k)$ ; hence by [L2] and [L3] $c_{2} (V_{L}) = e (V_{L, R})$ in the complex orientation $= - e (V_{L, R})$ in the fibre orientation $= - u$ .

6.1step 5.1L2L3

The complex orientation of $V_{R}$ agrees with the fibre orientation: the commuting complex structure is left multiplication by $i$ , whose complex basis $(1, j)$ gives the real ordered basis $(1, i, j, k)$ ; hence $c_{2} (V_{R}) = + u$ .

7.1step 5.1step 6.1∎

Substituting steps 5.1 and 6.1 into step 4.1 gives $p_{1} (V_{L}) = - 2 (- u) = 2 u$ and $p_{1} (V_{R}) = - 2 u$ , while step 1.1's Euler computation gives $e (V_{L}) = e (V_{R}) = u$ , as asserted.

Depends on

Used by

Euler and first Pontryagin classes of ξ_h,j Lemma

Dependency tree · two levels

39 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 3.2 (complexification and Pontryagin classes) (standard reference, not scraped)