ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passaudited 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.

The relation Sq^1Sq^1=0

Example

For every space $X$ , every integer $n \geq 0$ , and every $x \in H^{n} (X; F_{2})$ ,

$S q^{1} S q^{1} (x) = 0.$

This is the first positive Adem relation, but the calculation below does not use the general Adem theorem and assumes no form of choice.

Facts & Assumptions

Given: A space $X$ , an integer $n \geq 0$ , and $x \in H^{n} (X; F_{2})$ .

[F1]

Bockstein connecting operation defines the integral Bockstein $\tilde{β}$ from $0 \to Z \overset{2}{\to} Z \to F_{2} \to 0$ and the mod-two Bockstein $β$ from $0 \to F_{2} \overset{2}{\to} Z / 4 \to F_{2} \to 0$ ; zero/one residue lifts make both constructions choice-free.

[F2]

Sq^1 is the mod-two Bockstein gives $S q^{1} = β$ on every mod-two cohomology group without AC.

Verification

technique · compare the two cyclic Bocksteins on cochains and compose

1.1

Reduction modulo two satisfies $β = ρ \tilde{β}$ . [given, F1] Let $c$ be a mod-two cocycle representing a class $u$ , and let $\hat{c}$ be its integer zero/one lift. Since $δ c = 0$ , every value of $δ \hat{c}$ is even, so there is a unique integer cochain $h$ with

$δ \hat{c} = 2 h .$

Also $δ h = 0$ , because $2 δ h = δ^{2} \hat{c} = 0$ and integer cochains are torsion-free. Thus $\tilde{β} (u) = [h]$ . Reducing $\hat{c}$ modulo four gives a lift of $c$ for the mod-two coefficient sequence, and its coboundary is $2 (h m o d 2)$ in $Z / 4$ . Hence $β (u) = [h m o d 2] = ρ \tilde{β} (u)$ .

1.2

The integral Bockstein kills reduced integral classes: $\tilde{β} ρ = 0$ . [F1] If $z$ is an integral cocycle, then $z$ itself is an integer lift of its mod-two reduction. Its coboundary is zero, so the lift/divide definition gives $\tilde{β} (ρ [z]) = 0$ .

2.1

The mod-two Bockstein squares to zero. [step 1.1, step 1.2] For every mod-two class $u$ ,

$β^{2} (u) = ρ \tilde{β} ρ \tilde{β} (u) = 0.$

3.1

Substitution of $S q^{1} = β$ proves the claim. [F2, step 2.1] Apply [F2] first to $x$ and then to the class $β (x)$ :

$S q^{1} S q^{1} (x) = β (β (x)) = β^{2} (x) = 0.$

4.1

The boundary and choice cases introduce no exceptions. [F1, F2, step 1.1, step 1.2, step 2.1, step 3.1] For the empty space, a zero class, or a point in degree zero, every displayed positive-degree output is zero. The first allowed degree $n = 0$ is included, and there is no upper endpoint. Integer multiplication by two is injective even when a cochain group is zero, so the division argument is unique; ordinary singular cochains include degenerate simplices. Every lift used above is the specified residue lift or the already given cocycle $z$ , so no choice principle is spent. The proof establishes an equality, not either direction of a biconditional. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Hatcher, Algebraic Topology (standard reference, not scraped)