ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Primary obstruction to a nowhere-zero section of a sphere fibration

Claim

Assume AC. Let $(X, A)$ be a CW pair and let $p : E \to X$ be a numerable fibration with fiber $S^{r}$ , where $r \geq 1$ , together with a section over $A$ . The first possible obstruction to extending that section over $X$ is

$o_{r + 1} (p) \in H^{r + 1} (X, A; P),$

where $P$ has stalk $π_{r} (S^{r}) ≅ Z$ and fiber transport acts by its orientation sign. If $E$ is the unit-sphere bundle of a real vector bundle, a section of $E$ is equivalently a nowhere-zero vector-bundle section after radial normalization. No identification of $o_{r + 1}$ with an Euler class is asserted here.

Facts & Assumptions

[F1]

$S^{r}$ is path connected and $π_{q} (S^{r}) = 0$ for $0 < q < r$ (Lower-dimensional sphere maps are based nullhomotopic).

[F2]

Degree identifies $π_{r} (S^{r})$ with $Z$ and classifies based self-maps (Based sphere maps are classified by degree); a self-homotopy equivalence therefore acts by multiplication by the unit $1$ or $- 1$ .

[F3]

The lifting obstruction in dimension $q + 1$ has coefficients in the local system of $π_{q}$ of the fiber (Obstruction theory for lifting through a fibration).

[A1]

AC is used only to make simultaneous extension choices over arbitrary cell families (The Axiom of Choice).

Verification

Given: The fibration, relative section, and [A1] above.

1.1

A section is a lift of ${id}_{X}$ through $p$ . By [F1, F3], every positive-dimensional obstruction below degree $r + 1$ has zero stalk. The lifting theorem therefore extends the given section over $X^{r} \cup A$ ; for an arbitrary family of cells, this invokes exactly [A1].

F1F3A1

2.1

The next obstruction has stalk $π_{r} (S^{r})$ , which [F2] identifies with $Z$ . Transport around a loop in $X$ is represented by a self-homotopy equivalence of the fiber. Its action on this integer stalk is multiplication by its degree, hence by its orientation sign. This is precisely the local system $P$ , so [F3] places the obstruction in the displayed group.

F2F3step 1.1

3.1

Vanishing of this class is equivalent to extension through $X^{r + 1} \cup A$ after the permitted change on $X^{r} \cup A$ ; higher-dimensional cells may have further obstructions. The restriction $r \geq 1$ is essential: $π_{0} (S^{0})$ is a pointed set, not the asserted integer coefficient system. For a finite CW pair only finite choices occur. $□$

F3A1step 2.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

James Davis and Paul Kirk, Lecture Notes in Algebraic Topology (standard reference, not scraped)
Haynes Miller, MIT 18.906 Algebraic Topology II lecture notes (standard reference, not scraped)