+++ title = “The Archive” section = “features” +++
The Archive
The Archive is a curated collection of pre-computed spectral sequences that ship with htpy. These computations are read-only — you can browse them, inspect individual bidegrees, run the deduction engine, and export data, but you cannot modify the underlying resolution data.
What’s included
| Module | SS type | Range | Description |
|---|---|---|---|
| S_2 | Adams | stem $\leq 90$, filt $\leq 15$ | $\operatorname{Ext}_A(\mathbb{F}_2, \mathbb{F}_2)$ with BFCC $d_2$, LWX higher diffs |
| S_3 | Adams | stem $\leq 120$, filt $\leq 30$ | $\operatorname{Ext}_A(\mathbb{F}_3, \mathbb{F}_3)$ |
| S_2_mot | Motivic Adams | stem $\leq 110$, filt $\leq 55$ | $\operatorname{Ext}{A{\mathrm{mot}}}(\mathbb{F}_2, \mathbb{F}_2)$ with $\tau$-torsion orders, Isaksen diffs |
| S_2_nov | Algebraic Novikov | stem $\leq 110$, filt $\leq 55$ | aNSS $E_2$ from Isaksen CSV |
| S_2_ctau | Motivic Adams | stem $\leq 36$, filt $\leq 8$ | $\operatorname{Ext}{A{\mathrm{mot}}}(C\tau, \mathbb{F}_2)$ via GWX |
| S_2_cess | CESS | stem $\leq 30$, filt $\leq 16$ | $\operatorname{Ext}_{P^*}(\mathbb{F}_2, \mathbb{F}_2[q_0, \ldots])$ |
Each module includes its Ext chart, products with named generators, and (where available) differentials and $\tau$-torsion data.
Browsing the archive
On the landing page, click “SSEQ Results” to see all archive modules. Each module has a badge indicating its spectral sequence type. Click a module to open it in the viewer.
What you can do with archive modules
While viewing an archive module, you can:
- Browse the spectral sequence chart (pan, zoom, page navigation)
- Inspect individual classes (bidegree, dimension, products, differentials, Massey products)
- Run the deduction engine to derive additional differentials from the existing data
- Add detects annotations recording which stable homotopy element each class detects
- Add annotations — notes tagged as question, todo, proof, or reference
- Export the data as JSON or as a Lean 4 certificate
Data sources
| Module | Computation source |
|---|---|
| S_2 | BFCC Zenodo dataset + LWX machine proofs |
| S_3 | Live htpy resolution |
| S_2_mot | Live motivic resolution + Isaksen CSV + iterated LES torsion |
| S_2_nov | Isaksen algebraic Novikov CSV |
| S_2_ctau | Live motivic resolution of $C\tau$ module |
| S_2_cess | Live $P^*$ resolution of $\mathbb{F}_2[q_0, \ldots, q_5]$ |