PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Degree of the antipodal map on the sphere

Statement

Give $S^{n} = \partial D^{n + 1}$ its outward-normal-first boundary orientation. For $n \geq 1$ , the antipodal diffeomorphism $A : S^{n} \to S^{n}$ , $A (x) = - x$ , has $\deg (A) = (- 1)^{n + 1} .$

Facts & Assumptions

Given: The oriented sphere and antipodal map in the statement.

[F1]

Induced boundary orientation says that $(v_{1}, \dots, v_{n})$ is positive in $T_{x} S^{n}$ exactly when $(x, v_{1}, \dots, v_{n})$ is positive in the ambient $R^{n + 1}$ .

[F2]

Pointwise orientation sign of a local diffeomorphism identifies the orientation behavior of a local diffeomorphism from the determinant sign of its differential.

[F3]

Degree of an orientation-preserving or reversing diffeomorphism gives degree $1$ for an orientation-preserving diffeomorphism and $- 1$ for an orientation-reversing one.

Proof

technique · direct orientation comparison

1.1F1F2given

The map $A$ is smooth and satisfies $A^{- 1} = A$ , hence is a diffeomorphism. Fix $x \in S^{n}$ and a positive tangent basis $(v_{1}, \dots, v_{n})$ at $x$ . Its image basis at $- x$ is $(- v_{1}, \dots, - v_{n})$ . By [F1], its boundary-orientation sign is the ambient sign of $(- x, - v_{1}, \dots, - v_{n}) = (- 1)^{n + 1} (x, v_{1}, \dots, v_{n}) .$ Thus [F2] makes $A$ orientation preserving when $n + 1$ is even and orientation reversing when $n + 1$ is odd.

2.1F3step 1.1∎

Applying [F3] in the two parity cases gives $\deg (A) = (- 1)^{n + 1}$ . For $n = 1$ this is $+ 1$ , agreeing with the half-turn of the oriented circle; for even $n$ it is $- 1$ . The excluded $n = 0$ case has a disconnected sphere and lies outside the degree definition used here. There are no endpoint, fibre, or choice issues: the calculation is pointwise and the same sign holds at every $x$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

Robbin–Salamon, Introduction to Differential Topology, degree examples following Theorem 5.4.1 (standard reference, not scraped)