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.

Real projective infinity as BZ/2

Claim

Assume AC. The antipodal universal double cover identifies

${R P}^{\infty} ≃ B (Z / 2) = K (Z / 2, 1) .$

Facts & Assumptions

[F1]

The join of $N + 1$ copies of the two-point space $Z / 2$ is $S^{N}$ , compatibly with the standard inclusions, and the diagonal action is antipodal (Finite join models for the circle and the two-point group).

[F2]

The same finite-join identification induces the antipodal quotient $S^{N} / (Z / 2) = {R P}^{N}$ (Finite join models for the circle and the two-point group).

[F3]

For a well-pointed topological group of CW type, Milnor's $E G$ is contractible and its orbit map is a principal bundle (Milnor's join model is a contractible free G-space).

[F4]

Assuming AC, the classifying space of a discrete group $G$ has CW type $K (G, 1)$ (The classifying space of a discrete group is a K(G,1)).

[A1]

AC is used exactly through [F4] (The Axiom of Choice).

Verification

Given: $G = Z / 2$ with the discrete topology.

1.1

The identifications in [F1, F2] commute with the finite-join inclusions, so Milnor's orbit bundle is

F1F2

$S^{\infty} ⟶ {R P}^{\infty} .$

It is the antipodal double cover and its quotient is Milnor's $B (Z / 2)$ . By [F3] its total space is contractible and the map is locally trivial; because $Z / 2$ is discrete, each trivialization is an evenly covered neighborhood. Thus it is the universal double cover. [F1, F2, F3]

2.1

Under [A1], apply [F4]: the base is connected, its fundamental group is $Z / 2$ , and every higher homotopy group vanishes. The assumption is used exactly through that cited corollary. Hence ${R P}^{\infty}$ is the displayed Eilenberg--Mac Lane model. $□$

F4A1step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

Dale Husemoller, Fibre Bundles, Third Edition (standard reference, not scraped)