CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Four closed sets can cover $S^{2}$ without any one containing an antipodal pair

Statement refuted

The conclusion for a closed cover by three sets remains true for a closed cover by four sets: whenever four closed subsets cover $S^{2}$ , one member contains a pair of antipodal points.

Facts & Assumptions

Given: The unit sphere $S^{2} \subseteq R^{3}$ .

[F1]

If three closed subsets cover $S^{2}$ , one of them contains a pair of antipodal points (One member of every three-set closed cover of $S^{2}$ contains an antipodal pair).

[F2]

The Euclidean inner product is bilinear (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F3]

The sphere $S^{2}$ is the set of unit vectors in $R^{3}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[L1]

A map into $R^{m}$ is continuous exactly when its component functions are continuous; sums and scalar multiples of continuous Euclidean-valued maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

Counterexample

technique · constructive

1.1

Let $v_{1} = \frac{(1, 1, 1)}{\sqrt{3}}, v_{2} = \frac{(1, - 1, - 1)}{\sqrt{3}}, v_{3} = \frac{(- 1, 1, - 1)}{\sqrt{3}}, v_{4} = \frac{(- 1, - 1, 1)}{\sqrt{3}},$ and for $1 \leq i \leq 4$ define $A_{i} = {x \in S^{2} : ⟨ x, v_{i} ⟩ \geq ⟨ x, v_{j} ⟩ for every 1 \leq j \leq 4} .$ The vectors $v_{i}$ are the vertices of a regular tetrahedron centred at $0$ .

givenF2F3constructalgebra

2.1

By [F2] and [L1], each $A_{i}$ is a finite intersection of sets defined by a continuous closed inequality $⟨ x, v_{i} - v_{j} ⟩ \geq 0$ , hence is closed in $S^{2}$ . For every $x \in S^{2}$ , the finite set of four real numbers $⟨ x, v_{j} ⟩$ has a maximum, so $x$ belongs to at least one $A_{i}$ . Thus $A_{1}, A_{2}, A_{3}, A_{4}$ cover $S^{2}$ .

step 1.1F2L1algebra

2.2

Suppose $x, - x \in A_{i}$ . Then $⟨ x, v_{i} - v_{j} ⟩ \geq 0$ and $⟨ - x, v_{i} - v_{j} ⟩ \geq 0$ for every $j$ , so all these inner products vanish. For $i = 1$ , the vectors $v_{1} - v_{2}$ , $v_{1} - v_{3}$ , and $v_{1} - v_{4}$ are scalar multiples of $(0, 1, 1)$ , $(1, 0, 1)$ , and $(1, 1, 0)$ , whose determinant is $2 \neq 0$ ; the other values of $i$ differ only by coordinate sign changes and permutations. Hence the three differences span $R^{3}$ , forcing $x = 0$ , contrary to $x \in S^{2}$ . No $A_{i}$ contains an antipodal pair.

step 1.1F2F3algebra

3.1

Steps 2.1 and 2.2 give a closed four-set cover with no antipodal pair in any member, refuting the proposed extension and showing that the three-set conclusion [F1] cannot be enlarged in this way.

step 2.1step 2.2F1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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

Allen Hatcher, Algebraic Topology, tetrahedral example after Corollary 1.11 (standard reference, not scraped)

Four closed sets can cover S2S2 without any one containing an antipodal pair