Verifiability of the disagreement with Toda
The main conclusion of the comparison is that the rapacious rule leaves more classes than Toda's 2003 table. So that this need not rest on trust in our program, for the first five disagreements we made a proof that can be checked independently.
Claim. If the rapacious rule (arrows $d_r\colon(n,s,c)\to(n-1,s+r,c+1)$, $r\ge2$, maximal rank on every page) is applied to the actual $E^2$ page of the metalibrary, then over $\pi_n(S^2)$ there remain
| n | the rule (both filling orders) | Toda 2003 |
|---|---|---|
| 49 | 2 | 1 |
| 50 | 3 | 1 |
| 51 | 1 | 0 |
| 59 | 2 | 1 |
| 60 | 1 | 0 |
Toda's values are quoted, not proved.
How it works
- Locality. The rule draws arrows only between nonzero cells of $E^2$, so it runs separately on each connected component of the graph of possible arrows. For the given columns it suffices to know the exact dimensions of the cells of these components and that all the neighbouring cells and all the other cells of the columns are zero: 89 cells (100 blocks of the differential) for $\pi_{49}$–$\pi_{51}$ and 86 cells (111 blocks, the largest 308,910 × 269,346) for $\pi_{59}$–$\pi_{60}$.
- Certificates are written by a program that need not be trusted.
- Rank of a block $\ge r$: vectors $y_1,\dots,y_r$ of source words whose $d(y_i)$ have pairwise distinct leading terms (the matrix is triangular). Checking it is only computing $d$, with no Gaussian elimination; on average 1.5 words per vector.
- A nonzero cell of dimension $h$: $h$ cycles $z$ ($dz=0$) and $h$ cocycles $\varphi$ ($\varphi\circ d=0$) with an invertible matrix $\varphi_j(z_i)$.
- Together with the rank bounds this gives the exact dimension of every cell.
- The checker is written from scratch following §2 of the Ivanov–Mikhailov–Wu paper (relations, $\partial$, admissibility, enumeration of words) and does not use the code that computed $E^2$. It checks the certificates and the completeness of the set of cells, and runs the rule itself. It rejects a corrupted certificate (tested with four kinds of corruption).
- Lean 4 is a third independent implementation of the algebra and of the same checks. The theorem on the number of
surviving classes is proved by computation (
native_decide, that is, trusting the Lean compiler); Lean rejects a wrong value.
Runs
| columns | generator | checker (Python) | Lean |
|---|---|---|---|
| π49–π51 | 3 s | 34 s, 1.1 GB | 4.6 min, 1.6 GB |
| π59–π60 | 72 s | 8 min, 4.3 GB | 3 h 28 min, 7.7 GB |
The certificates take 1.5 and 19 MB (compressed).
What is not covered here
- Toda's values are not checked.
- That the $E^2$ of this complex is the $E^2$ of the spectral sequence of the paper, and that the formulas of §2 define the lambda algebra correctly, is the mathematics of the paper. The checkers verify $d^2=0$ on small cells as a test of the conventions.
- The rule itself is our reading of the lecture (differentials).
- It is not proved in Lean that the computational checks imply the statements of linear algebra: Lean here is an independent program with a theorem about the result of its own run.
The code of the generator, the checker and the Lean project, and the certificates themselves, are available on request.