Atiyah calls it that in §2.2 of his lectures: “The fundamental theorem for K-theory is the periodicity theorem.” In Theorem 2.4.9 the group K⁻²(point) = K̃(S²) is the free “abelian group Z generated by [H] - [1]”, where H is the Hopf line bundle. Dugger describes the history: Bott “found an 8-fold periodicity (with respect to k) in the case of real vector bundles, and a 2-fold periodicity in the case of complex bundles”, and adds that “Bott’s periodicity theorems are of paramount importance in modern algebraic topology.” CITED
Zois' Lecture 4 proves the complex case from the index pairing of Lecture 3. The generator is concrete: “Let b ∈ K⁻¹R be the generator corresponding to the function z ↦ 1/z”. Under the isomorphism, 1 goes to “the tautological line bundle”, and gluing the two hemispheres of S² = ℂP¹ “we obtain the Hopf line bundle”. CITED
To build a line bundle on S², take a trivial line over each hemisphere and glue the two along the equator with a function f from the circle to the nonzero complex numbers. The sources above state that the bundle depends only on the homotopy class of f, and that this class is its winding number. The script checks the pieces that can be computed. The clutching function zk has winding number k for k = −3 … 3. Zois' generator 1/z has −1. Tensoring two line bundles multiplies their clutching functions, and the winding numbers add, in all 25 cases tried. A function that looks nothing like z², namely (z−.3)(z+.2i)/(z−3), also has winding number 2, and the straight line from it to −z²/3 never passes through 0 on the circle, so it glues the same bundle. COMPUTED
These are the numbers of Chapter 3. There the winding number of a symbol gave the index of a Toeplitz operator. Here it gives the degree of a line bundle. The group K̃(S²) = ℤ is the winding numbers again. Its generator has winding number −1, the same integer as the index of Chapter 1's shift, whose symbol is z.
The last step of Zois' proof uses the fact that the matrix [[0, −I], [I, 0]], acting on ℝ² ⊕ ℝ², “is homotopic to the identity”. “The above is known as Atiyah’s trick.” CITED The homotopy is the rotation R(t) of the plane in each coordinate, from t = 0 to π/2. The script checks that it starts at the identity, ends at the quarter-turn, and has determinant 1 at all 401 points in between. CliffordSmall.J_sq and J_det prove in Lean that the 2×2 quarter-turn squares to −1 and has determinant 1. It is the rotation of Chapter 5's Whitehead lemma, used a second time. COMPUTED KERNEL-CHECKED
Where the 2 and the 8 come from is usually explained with Clifford algebras: algebras generated by n anticommuting elements whose squares are fixed. With two generators squaring to −1 one gets Hamilton's quaternions. qi_sq, qj_sq and qi_qj_anticomm check i² = j² = −1 and ij = −ji in Mathlib's ℍ. KERNEL-CHECKED
The script works in the basis of monomials eS, with exact sign arithmetic and no matrices. For each n up to 16 it finds the centre, the elements that commute with everything. Over ℂ the centre has dimension 1 when n is even and 2 when n is odd, so the pattern has period 2, the complex period. Over ℝ, for Cl0,n, the pattern has period 4: COMPUTED
| n mod 8 | dim of centre | centre (real) |
|---|---|---|
| 0 | 1 | R |
| 1 | 2 | C |
| 2 | 1 | R |
| 3 | 2 | R⊕R |
| 4 | 1 | R |
| 5 | 2 | C |
| 6 | 1 | R |
| 7 | 2 | R⊕R |
That is half of the 8. The other half is invisible to the centre. It is whether each simple piece is a matrix algebra over ℝ, ℂ or ℍ, and that takes the division algebras of dimensions 1, 2 and 4. Zois gives the fact behind it as a theorem of topological K-theory: there are “no finite dimensional division algebras over R in dimensions other than 1, 2, 4 and 8”. The script does not compute that half, and the page says so. CITED OPEN
Dugger computes the real K-theory of real projective space: KÕ(ℝPn) is cyclic of order 2f, where f counts the s with 0 < s ≤ n and “s ≡ 0, 1, 2, or 4 mod 8”. CITED The script evaluates the formula. The orders for n = 1 … 8 are 2, 4, 4, 8, 8, 8, 8, 16, and f(n + 8) = f(n) + 4 for every n checked. Every eight dimensions add exactly four factors of 2. The period 8 shows up here directly, in the size of a group. COMPUTED
The first draft of CliffordSmall.lean did not compile, because it was missing one import, the real numbers. Lean still printed “does not depend on any axioms” for the theorems whose statements had failed to elaborate. An axiom report is not evidence that a file compiled. That is why this series' gate builds the file first and only then reads the report (Book XIX).