Stable homotopy theory and generalised cohomology

The homotopy groups of spheres $\pi_{n+k}(S^n)$ are among the most basic and most mysterious objects in topology. $\pi_3(S^2) \cong \Z$ is generated by the Hopf map; $\pi_6(S^3) \cong \Z/12$; $\pi_{10}(S^4) \cong \Z/24 \oplus \Z/3$. No formula is known, and none is expected.

But a pattern appears if you look along the diagonals. Suspending a map $f : S^{n+k} \to S^n$ — taking the double cone on both sides — gives a map $\Sigma f : S^{n+k+1} \to S^{n+1}$, and Hans Freudenthal proved in 1937 that once $n > k + 1$ this changes nothing: the groups $\pi_{n+k}(S^n)$ stabilise. The limits $\pi_k^s$, the stable stems, are still hard — they are known only in a finite range — but they are abelian, finite in positive degrees, and they carry a rich algebraic structure.

Stable phenomena turn out to be everywhere:

• Generalised cohomology theories — ordinary cohomology, topological K-theory, cobordism — are all represented by the objects of stable homotopy theory, spectra (Brown, 1962).
• Manifolds. Thom (1954) showed that classifying manifolds up to cobordism is a computation of stable homotopy groups of Thom spectra. Kervaire and Milnor (1963) counted exotic spheres using the stable stems: there are exactly 28 smooth structures on $S^7$, up to orientation-preserving diffeomorphism.
• Algebra and number theory. The stable stems are approached by spectral sequences built from the Steenrod algebra, and organised by formal groups — objects that came from number theory — through Quillen's theorem (1969) and chromatic homotopy theory. Bernoulli numbers appear in the answers.

This lesson is an orientation: suspension and spectra, cohomology theories, Thom's theorem with a complete proof of its easy half, the J-homomorphism, and a glimpse of the chromatic picture, with what is known and what is open.

Here is part of the table of $\pi_{n+k}(S^n)$ (Toda, 1962). Rows are spheres $S^n$, columns the excess $k$. Entries with $n > k + 1$ — in the stable range, by Freudenthal's theorem — are in bold; along each column they are constant.

So $\pi_0^s = \Z$ (degree), $\pi_1^s = \Z/2$ (generated by the suspended Hopf map $\eta$), $\pi_2^s = \Z/2$ ($\eta^2$), $\pi_3^s = \Z/24$ ($\nu$, from the quaternionic Hopf map), $\pi_4^s = \pi_5^s = 0$, $\pi_6^s = \Z/2$ ($\nu^2$). Unstable phenomena change on suspension: the infinite cyclic summand of $\pi_7(S^4)$, generated by the quaternionic Hopf map, becomes torsion — the Hopf map suspends to the generator $\nu$ of $\pi_3^s = \Z/24$.

The guiding analogy: stable homotopy theory is to homotopy theory what linear algebra is to geometry. Suspension is invertible in the stable world, maps can be added, every map has a cofibre and the cofibre sequences are long exact both ways — fibre sequences and cofibre sequences coincide. Spectra are the "abelian groups" of homotopy theory: just as every abelian group is a set with extra structure that makes addition possible, a spectrum is a space with infinitely many deloopings. (This is an analogy, made precise by the theory of stable ∞-categories: see stable ∞-categories.)

All spaces are pointed CW complexes; $[X, Y]$ denotes pointed homotopy classes of maps.

Proof sketch. Write $\Sigma X$ as the union of two cones $C_+X \cup C_-X$ meeting in $X$. The suspension map is the composite $\pi_q(X) \cong \pi_{q+1}(C_+X, X) \to \pi_{q+1}(\Sigma X, C_-X) \cong \pi_{q+1}(\Sigma X)$, and the middle map is an isomorphism in the stated range by the homotopy excision theorem (Blakers–Massey), since $(C_\pm X, X)$ are $n$-connected. See Hatcher, Algebraic Topology, Corollary 4.24; a different proof uses the James construction $J(X) \simeq \Omega\Sigma X$. For $n > k + 1$ we have $n + k < 2n - 1$, which gives the second statement.

The proof builds $E_n$ cell by cell so that $[-, E_n]$ agrees with $\tilde E^n$ on spheres and then on all complexes, using the Mayer–Vietoris property (from exactness) and additivity; the suspension isomorphism supplies the structure maps. Categorically, it is a Yoneda-type statement: a contravariant functor to sets that turns homotopy colimits into limits is representable.

Proof sketch of (1). Embed $M^n \subset S^{n+k}$ with normal bundle $\nu$ and tubular neighbourhood $N \cong \nu$. Collapse everything outside $N$ to the base point: $S^{n+k} \to N/\partial N \cong \mathrm{Th}(\nu)$. Compose with the Thom map of the classifying map $\nu \to \gamma_k$: this gives an element of $\pi_{n+k}(MO(k))$. Conversely, a map $S^{n+k} \to MO(k)$ can be made transverse to the zero section $BO(k) \subset MO(k)$, and the preimage is a closed $n$-manifold. Cobordisms correspond to homotopies (apply the same constructions to $S^{n+k} \times [0, 1]$). Statement (2) is a computation: Thom determined the homotopy type of $MO$ as a product of Eilenberg–MacLane spectra $H\mathbb{F}_2$ using the Steenrod algebra. See Milnor–Stasheff, Characteristic Classes, Chapters 17–18. The experiment below compares (2) with Stiefel–Whitney numbers of products of projective spaces.

Adams (1965–66) proved that the image has order $m(2k)$ or $2m(2k)$ and that it is exactly $m(2k)$ if the Adams conjecture holds; the conjecture was proved by Quillen (1971), Sullivan (1974) and Becker–Gottlieb (1975). Equivalently, $m(2k)$ is the denominator of $\zeta(1 - 2k)/2$, since $\zeta(1-2k) = -B_{2k}/2k$. The lower bound comes from the e-invariant, defined using K-theory and Adams operations.

Chromatic homotopy theory, in outline. By Quillen's theorem a complex-oriented cohomology theory has a formal group law, and the moduli of formal groups — stratified by height — organises the stable homotopy category. Ordinary rational cohomology sees height 0, K-theory height 1, elliptic cohomology and topological modular forms heights $\le 2$, and the Morava K-theories $K(n)$ isolate height $n$. Two deep theorems make this rigorous: the nilpotence theorem (Devinatz–Hopkins–Smith, 1988), which says $MU_*$ detects nilpotence of self-maps of finite spectra, and the periodicity theorem (Hopkins–Smith, 1998), which produces $v_n$-periodic self-maps. The stable stems are then built, prime by prime, from layers of height $0, 1, 2, \dots$; the image of J is (essentially) the height-1 layer.

Established. The theorems above; the chromatic convergence and thick subcategory theorems (Hopkins–Ravenel, Hopkins–Smith); the construction of topological modular forms (Goerss, Hopkins, Miller and others) and its use to detect large parts of the stable stems; the solution of the Kervaire invariant one problem outside dimension 126 by Hill, Hopkins and Ravenel (2016): elements of Kervaire invariant one exist only in dimensions $2, 6, 14, 30, 62$ and possibly $126$. Computations of the stable stems at the prime 2, using the Adams spectral sequence, motivic homotopy theory and machine computation, now reach dimension 90 (Isaksen, Wang and Xu, 2023); among their consequences, Wang and Xu (2017) showed $\pi_{61}^s = 0$, which implies that $S^{61}$ has a unique smooth structure — the only odd-dimensional spheres with this property are $S^1, S^3, S^5$ and $S^{61}$.

Recent and announced. A 2023 preprint by Burklund, Hahn, Levy and Schlank disproves Ravenel's telescope conjecture at all heights $\ge 2$; a 2024 preprint by Lin, Wang and Xu constructs Kervaire invariant one elements in dimension 126. These are major announcements whose refereeing and absorption are under way.

Open problems.

• The stable stems in general: no description of $\pi_k^s$ for all $k$ is known or expected; even the pattern of their orders is mysterious beyond the chromatic layers.
• Hopkins' chromatic splitting conjecture, describing how the $K(n)$-local spheres fit together, is open in general (known at low heights).
• Which smooth manifolds admit exotic structures in a given dimension, and the size of $\Theta_n$ in general, depend on the unknown parts of $\pi_n^s / \operatorname{im} J$.

Mathlib has homotopy groups of spaces, and proves them abelian from dimension 2 on — the reason every stable group is abelian:

/-- **Eckmann–Hilton.** For `n ≥ 0`, the homotopy group `π_{n+2}(X, x)` is abelian: two maps of the
cube `I^{n+2}` can be composed along two different coordinates, and the interchange law forces
both compositions to agree and commute. This is Mathlib's instance `HomotopyGroup.commGroup`.
Since the stable stem `πₖˢ = colim_n π_{n+k}(Sⁿ)` is a colimit of such groups, every stable
homotopy group is abelian — the first sign that stable homotopy theory is "linear". -/
theorem homotopyGroup_mul_comm {X : Type*} [TopologicalSpace X] (x : X) (n : ℕ)
    (a b : HomotopyGroup.Pi (n + 2) X x) : a * b = b * a :=
  mul_comm a b

It has no suspension theorem, spectra, cohomology theories, cobordism or K-theory. What can be formalised is the algebra that computes them. Formal group laws, in the form needed here — identities valid in every commutative ring, which for polynomial laws is the same as being a formal group law over $\Z$:

/-- The axioms of a (one-dimensional, commutative) **formal group law** `F`, stated as identities
in a commutative ring `A`: `F(x, 0) = x`, `F(x, y) = F(y, x)` and `F(F(x, y), z) = F(x, F(y, z))`.
A genuine formal group law is a power series in two variables; for the polynomial laws below,
holding in *every* commutative ring (for instance `A = ℤ[x, y, z]`) is the same as being a
formal group law over `ℤ`. A complex-oriented cohomology theory `E` has one: it records the first
Chern class of a tensor product of line bundles, `c₁(L ⊗ M) = F(c₁ L, c₁ M)`. -/
structure IsFormalGroupLaw (F : A → A → A) : Prop where
  zero_right : ∀ x, F x 0 = x
  comm : ∀ x y, F x y = F y x
  assoc : ∀ x y z, F (F x y) z = F x (F y z)

/-- The **additive formal group law** `F(x, y) = x + y`: ordinary cohomology,
`c₁(L ⊗ M) = c₁(L) + c₁(M)`. -/
def addFGL (x y : A) : A := x + y

/-- The **multiplicative formal group law** `F(x, y) = x + y + xy`. Complex K-theory has this law
(up to sign and a unit, the Bott class): with `c₁(L) = L − 1`, `L ⊗ M − 1 = (L − 1) + (M − 1) +
(L − 1)(M − 1)`. -/
def mulFGL (x y : A) : A := x + y + x * y

/-- `x + y` is a formal group law: the axioms are the ring axioms for addition. -/
theorem isFormalGroupLaw_add : IsFormalGroupLaw (addFGL (A := A)) where
  zero_right x := by simp [addFGL]
  comm x y := by simp only [addFGL]; ring
  assoc x y z := by simp only [addFGL]; ring

/-- `x + y + xy` is a formal group law. Associativity: both sides equal
`x + y + z + xy + xz + yz + xyz`. -/
theorem isFormalGroupLaw_mul : IsFormalGroupLaw (mulFGL (A := A)) where
  zero_right x := by simp [mulFGL]
  comm x y := by simp only [mulFGL]; ring
  assoc x y z := by simp only [mulFGL]; ring

/-- The multiplicative law is the multiplicative group in disguise: `1 + F(x, y) = (1 + x)(1 + y)`.
Over `ℚ` the logarithm `log(1 + x)` turns it into the additive law; over `ℤ/p` no such
isomorphism exists, which is what *height* measures. -/
theorem one_add_mulFGL (x y : A) : 1 + mulFGL x y = (1 + x) * (1 + y) := by
  simp only [mulFGL]
  ring

The $n$-series and Theorem 11, the heights of the additive and multiplicative laws:

/-- The **`n`-series** `[n]_F(x) = F(x, F(x, …, F(x, 0)))`, "`x` added to itself `n` times" with
the formal group law `F`. -/
def nSeries (F : A → A → A) : ℕ → A → A
  | 0, _ => 0
  | n + 1, x => F x (nSeries F n x)

/-- For the additive law, `[n](x) = n x`. -/
theorem add_nSeries (n : ℕ) (x : A) : nSeries addFGL n x = n * x := by
  induction n with
  | zero => simp [nSeries]
  | succ n ih =>
    simp only [nSeries, addFGL, ih]
    push_cast
    ring

/-- For the multiplicative law, `1 + [n](x) = (1 + x)ⁿ`, by induction using `one_add_mulFGL`. -/
theorem mul_nSeries (n : ℕ) (x : A) : 1 + nSeries mulFGL n x = (1 + x) ^ n := by
  induction n with
  | zero => simp [nSeries]
  | succ n ih =>
    rw [nSeries, one_add_mulFGL, ih, pow_succ, mul_comm]

/-- **The multiplicative formal group law has height 1 at every prime.** Over `𝔽_p`, its
`p`-series is `[p](X) = Xᵖ`: from `1 + [p](X) = (1 + X)ᵖ = 1 + Xᵖ` (the "freshman's dream" in
characteristic `p`, Mathlib's `add_pow_char`). In chromatic homotopy theory this is why complex
K-theory sits at chromatic height 1. -/
theorem mul_pSeries_charP : nSeries mulFGL p (X : (ZMod p)[X]) = X ^ p := by
  have h := mul_nSeries p (X : (ZMod p)[X])
  rw [add_pow_char, one_pow] at h
  exact add_left_cancel h

/-- **The additive formal group law has infinite height.** Over `𝔽_p`, its `p`-series is
`[p](X) = pX = 0`. Ordinary mod-`p` cohomology sits at chromatic height ∞; the Morava K-theories
`K(n)` interpolate, with formal groups of height exactly `n`. -/
theorem add_pSeries_charP : nSeries addFGL p (X : (ZMod p)[X]) = 0 := by
  rw [add_nSeries]
  simp

The binomial parities of Corollary 5 (the topology — Theorem 4 and the formula for $w(\R P^n)$ — is cited):

/-- **Odd projective spaces bound.** The total Stiefel–Whitney class of `ℝPⁿ` is `(1 + a)ⁿ⁺¹`, so
`w_i(ℝPⁿ) = C(n+1, i) aⁱ`. If `n + 1 = 2m` is even, then `C(2m, i)` is even for every odd `i`:
from `i · C(2m, i) = 2m · C(2m − 1, i − 1)`. So only even-degree classes survive mod 2, every
Stiefel–Whitney number `w_I[ℝPⁿ]` of the odd degree `n` vanishes, and by the theorems of
Pontryagin and Thom `ℝPⁿ` is the boundary of a compact `(n+1)`-manifold. -/
theorem rp_odd_sw_vanish (m i : ℕ) (hi : Odd i) : 2 ∣ Nat.choose (2 * m) i := by
  obtain ⟨j, rfl⟩ := hi
  rcases m with _ | m
  · rw [Nat.choose_eq_zero_of_lt (by omega)]
    exact dvd_zero 2
  · -- `(2m + 2) · C(2m + 1, 2j) = C(2m + 2, 2j + 1) · (2j + 1)`
    have h := Nat.add_one_mul_choose_eq (2 * m + 1) (2 * j)
    have hdvd : 2 ∣ Nat.choose (2 * m + 1 + 1) (2 * j + 1) * (2 * j + 1) :=
      ⟨(m + 1) * Nat.choose (2 * m + 1) (2 * j), by rw [← h]; ring⟩
    rcases (Nat.Prime.dvd_mul Nat.prime_two).mp hdvd with h2 | h2
    · simpa [show 2 * (m + 1) = 2 * m + 1 + 1 by ring] using h2
    · omega

/-- **Even projective spaces do not bound.** For `n = 2m`, the top Stiefel–Whitney class is
`w_n(ℝPⁿ) = C(n+1, n) aⁿ = (n+1) aⁿ`, and `n + 1` is odd, so the Stiefel–Whitney number
`w_n[ℝPⁿ]` is `1 ∈ 𝔽₂` (it is also the Euler characteristic mod 2). By Pontryagin's theorem,
`ℝP²ᵐ` is not the boundary of any compact manifold; `ℝP²` and `ℝP⁴` generate parts of Thom's
cobordism ring `𝔑_*`. -/
theorem rp_even_top_sw (m : ℕ) : ¬ 2 ∣ Nat.choose (2 * m + 1) (2 * m) := by
  rw [Nat.choose_succ_self_right]
  omega

And the Bernoulli arithmetic of Theorem 8, using Mathlib's Bernoulli numbers:

/-- **Bernoulli numbers in the stable stems.** `B₂/4 = 1/24` and `B₄/8 = −1/240`. By Adams'
work on the J-homomorphism (completed by the proof of the Adams conjecture by Quillen, Sullivan
and Becker–Gottlieb), the image of `J : π_{4k−1}(SO) → π_{4k−1}ˢ` is cyclic of order the
denominator of `B_{2k}/4k`: here `24` and `240`, which are the whole groups `π₃ˢ = ℤ/24` and
`π₇ˢ = ℤ/240`. Lean checks the arithmetic, from Mathlib's `bernoulli_two` and `bernoulli'_four`;
the homotopy theory is cited. -/
theorem image_of_j_orders :
    bernoulli 2 / (2 * 2) = 1 / 24 ∧ bernoulli 4 / (2 * 4) = -1 / 240 := by
  refine ⟨?_, ?_⟩
  · rw [bernoulli_two]
    norm_num
  · rw [bernoulli_eq_bernoulli'_of_ne_one (by norm_num), bernoulli'_four]
    norm_num

What is not formalised. Theorems 1–10 themselves, and every computation of a stable homotopy group. Formal group laws are stated for polynomials rather than power series, which covers the two laws used here but not, for example, the universal law of $MU$.

The first experiment computes Bernoulli numbers exactly and evaluates the two classical formulas of Theorems 8 and 9: the order of the image of J (compared with the known stems) and the number of exotic spheres bounding parallelisable manifolds.

"""Bernoulli numbers in stable homotopy: the image of J and exotic spheres.

Two classical theorems turn Bernoulli numbers into homotopy theory.

* Adams (with the Adams conjecture, proved by Quillen, Sullivan and
  Becker-Gottlieb): the image of the stable J-homomorphism in the stable stem
  pi_{4k-1}^s is cyclic of order m(2k) = denominator of B_{2k} / 4k.
* Kervaire-Milnor (1963): the group bP_{4k} of exotic (4k-1)-spheres that
  bound parallelisable manifolds has order
  2^(2k-2) (2^(2k-1) - 1) * numerator(4 |B_{2k}| / k), for k >= 2.

We compute the Bernoulli numbers exactly, evaluate both formulas, and compare
m(2k) with the known stable stems pi_3^s = Z/24, pi_7^s = Z/240,
pi_11^s = Z/504 and pi_15^s = Z/480 + Z/2 (Toda, 1962), which are quoted here,
not computed.
"""

from fractions import Fraction
from math import comb

def bernoulli_numbers(n):
    """B_0, ..., B_n (convention B_1 = -1/2), from sum_j C(m+1, j) B_j = 0."""
    b = [Fraction(1)]
    for m in range(1, n + 1):
        s = sum(comb(m + 1, j) * b[j] for j in range(m))
        b.append(-s / (m + 1))
    return b

def image_of_j_order(k, b):
    """m(2k): the denominator of B_{2k} / 4k."""
    return (b[2 * k] / (4 * k)).denominator

def bp_order(k, b):
    """Kervaire-Milnor order of bP_{4k}, k >= 2."""
    num = (4 * abs(b[2 * k]) / k).numerator
    return 2 ** (2 * k - 2) * (2 ** (2 * k - 1) - 1) * num

#: Known stable stems pi_{4k-1}^s (Toda 1962), as orders and descriptions.
KNOWN_STEMS = {1: (24, "Z/24"), 2: (240, "Z/240"), 3: (504, "Z/504"),
               4: (960, "Z/480 + Z/2")}

def main():
    b = bernoulli_numbers(16)
    print(" k  B_2k          m(2k) = den(B_2k/4k)  pi_(4k-1)^s (known)")
    for k in range(1, 9):
        m = image_of_j_order(k, b)
        known = KNOWN_STEMS.get(k)
        tail = f"{known[1]} ({known[0] // m} x |im J|)" if known else "-"
        print(f"{k:2d}  {str(b[2 * k]):12s}  {m:21d}  {tail}")
    print("Numerators such as 691 (B_12) and 3617 (B_16) reappear in |bP_4k|.")
    print()
    print("Exotic spheres bounding parallelisable manifolds (Kervaire-Milnor):")
    for k in range(2, 6):
        print(f"  |bP_{4 * k}| = {bp_order(k, b):>10d}"
              f"   (homotopy {4 * k - 1}-spheres)")
    print("Since pi_7^s = im J, all homotopy 7-spheres bound parallelisable")
    print("manifolds: S^7 has exactly 28 smooth structures up to orientation-")
    print("preserving diffeomorphism, Milnor's 1956 examples among them.")
    print()
    print("Epistemic status: the Bernoulli numbers and both formulas are exact")
    print("rational computations. That m(2k) is the order of the image of J,")
    print("and the Kervaire-Milnor count, are theorems cited from the literature;")
    print("the stable stems in the last column are quoted (Toda's computations),")
    print("not computed. Agreement is consistency, not proof.")

if __name__ == "__main__":
    main()

The second compares Thom's answer for $\dim \mathfrak{N}_n$ with what Stiefel–Whitney numbers of products of real projective spaces can see: they span $\mathfrak{N}_n$ in even degrees up to 8, and nothing in odd degrees, where Dold manifolds are needed.

"""Thom's unoriented cobordism ring, checked with Stiefel-Whitney numbers.

Thom (1954) computed the unoriented cobordism ring as a homotopy ring of a
Thom spectrum: N_* = pi_*(MO) = F_2[x_i : i not of the form 2^k - 1], so
dim N_n is the number of partitions of n into parts not of the form 2^k - 1.
Pontryagin and Thom: a closed manifold bounds iff all its Stiefel-Whitney
numbers vanish.

We compute (exactly, over F_2) the Stiefel-Whitney numbers of products of real
projective spaces from w(RP^a) = (1 + u)^(a+1), check which bound, and compare
the rank of the span of their Stiefel-Whitney number vectors with Thom's dim
N_n. In odd dimensions every such product bounds, so other generators (Dold
manifolds) are needed: the computation shows this, Thom's theorem explains it.
"""

from itertools import combinations_with_replacement
from math import comb

def partitions(n, largest=None):
    """All partitions of n as non-increasing tuples."""
    if largest is None:
        largest = n
    if n == 0:
        return [()]
    out = []
    for first in range(min(n, largest), 0, -1):
        for rest in partitions(n - first, first):
            out.append((first,) + rest)
    return out

def is_mersenne(i):
    """True when i = 2^k - 1 for some k >= 1."""
    return i >= 1 and (i + 1) & i == 0

def thom_rank(n):
    """dim N_n: partitions of n avoiding parts 1, 3, 7, 15, ..."""
    return sum(1 for p in partitions(n) if not any(is_mersenne(i) for i in p))

def sw_classes(dims):
    """The classes w_0, ..., w_n of RP^d1 x ... x RP^dr as polynomials.

    Each w_i is a set of exponent tuples (coefficients are in F_2): the
    degree-i part of the product of (1 + u_j)^(d_j + 1), truncated at
    u_j^(d_j + 1).
    """
    n = sum(dims)
    classes = []
    for i in range(n + 1):
        terms = set()
        for e in combinations_with_replacement(range(len(dims)), i):
            exps = tuple(e.count(j) for j in range(len(dims)))
            if all(x <= d for x, d in zip(exps, dims)):
                c = 1
                for x, d in zip(exps, dims):
                    c *= comb(d + 1, x)
                if c % 2:
                    terms.add(exps)
        classes.append(terms)
    return classes

def sw_number(dims, partition, classes=None):
    """w_I[RP^d1 x ... x RP^dr] in F_2, for a partition I of sum(dims):
    the coefficient of u_1^d1 ... u_r^dr in w_{i_1} ... w_{i_s}."""
    if classes is None:
        classes = sw_classes(dims)
    product = {tuple(0 for _ in dims)}
    for i in partition:
        new = set()
        for e1 in product:
            for e2 in classes[i]:
                e = tuple(a + b for a, b in zip(e1, e2))
                if all(x <= d for x, d in zip(e, dims)):
                    new ^= {e}
        product = new
    return 1 if tuple(dims) in product else 0

def rp_products(n):
    """All products RP^d1 x ... x RP^dr (d_i >= 1) of dimension n."""
    return [p for p in partitions(n)]

def rank_mod2(rows):
    """Rank over F_2 of a list of 0/1 vectors."""
    rows = [int("".join(map(str, r)), 2) for r in rows if any(r)]
    basis = []
    for r in rows:
        for b in basis:
            r = min(r, r ^ b)
        if r:
            basis.append(r)
    return len(basis)

def main():
    print("Thom: dim N_n = #partitions of n with no part 1, 3, 7, 15, ...")
    print("  n:     " + " ".join(f"{n:3d}" for n in range(11)))
    print("  dim:   " + " ".join(f"{thom_rank(n):3d}" for n in range(11)))
    print()
    print("Products of real projective spaces, via Stiefel-Whitney numbers")
    print("  n  products  non-bounding  rank of span  Thom's dim N_n")
    for n in range(1, 9):
        parts = partitions(n)
        vectors = []
        for d in rp_products(n):
            classes = sw_classes(d)
            vectors.append([sw_number(d, I, classes) for I in parts])
        nonbounding = sum(1 for v in vectors if any(v))
        print(f"{n:3d}  {len(vectors):8d}  {nonbounding:12d}"
              f"  {rank_mod2(vectors):12d}  {thom_rank(n):14d}")
    v = [sw_number((2,), I) for I in partitions(2)]
    print(f"RP^2: (w_2, w_1^2) = {tuple(v)}, so RP^2 does not bound.")
    print("Odd n: every product has an odd-dimensional factor, which bounds.")
    print()
    print("Epistemic status: all Stiefel-Whitney numbers and partition counts")
    print("are exact computations over F_2, exhaustive for n <= 8. That they")
    print("decide cobordism (Pontryagin, Thom) and that N_* is polynomial on")
    print("generators in degrees not of the form 2^k - 1 (Thom) are theorems;")
    print("the agreement of the last two columns in even degrees is evidence.")

if __name__ == "__main__":
    main()

The Hopf invariant. The fibres of the Hopf map $\eta : S^3 \to S^2$ over two points of $S^2$ are two circles that link once: this linking number is the Hopf invariant, and it shows $\eta$ is not null-homotopic. Its suspensions generate $\pi_{n+1}(S^n) \cong \Z/2$ for $n \ge 3$.

The suspension tower. Each column of the table is a sequence of groups and suspension maps that eventually consists of isomorphisms:

Degree is the zeroth stable stem. On the circle, the homotopy class of a loop around a hole is its winding number; for maps $S^n \to S^n$ it is the degree, and $\pi_0^s = \Z$.