ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

Orthogonal projection $S^{2} \to R^{2}$ has exactly one antipodal pair with equal image

Example

For the coordinate projection

$q : S^{2} ⟶ R^{2}, q (x, y, z) = (x, y),$

the only antipodal pair with equal image is the unordered north-south pair ${(0, 0, 1), (0, 0, - 1)}$ .

Facts & Assumptions

Given: The unit sphere $S^{2} \subseteq R^{3}$ and the coordinate projection $q (x, y, z) = (x, y)$ .

[L1]

Every continuous map $S^{2} \to R^{2}$ has an antipodal pair with equal image (Borsuk–Ulam theorem in dimension two).

[F1]

The sphere $S^{2}$ consists of triples $(x, y, z)$ satisfying $x^{2} + y^{2} + z^{2} = 1$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[L2]

Continuity of a map into $R^{2}$ is equivalent to continuity of its coordinate functions (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).

Verification

technique · direct

1.1givenL2

Both coordinate functions of $q$ are continuous, so $q$ is continuous by [L2].

2.1step 1.1F1L1algebra∎

If $v = (x, y, z) \in S^{2}$ satisfies $q (v) = q (- v)$ , then $(x, y) = (- x, - y)$ and hence $x = y = 0$ . The unit-sphere equation gives $z^{2} = 1$ , so $v = (0, 0, 1)$ or $v = (0, 0, - 1)$ . These are two points forming exactly one antipodal pair, and they do have equal image $(0, 0)$ , in agreement with [L1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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, example after Theorem 1.10 (standard reference, not scraped)

Orthogonal projection S2→R2S2→R2 has exactly one antipodal pair with equal image