+++ title = “Introduction” section = “root” +++

What is htpy?

htpy is an interactive tool for computing and visualizing spectral sequences in stable homotopy theory. It runs as a single-binary server that embeds both the computation engine and the viewer interface, serving a browser-based frontend.

A persistent instance is available at htpy.app.

What it does

htpy computes $\operatorname{Ext}$ groups over the Steenrod algebra by constructing minimal free resolutions, then provides an interactive environment for working with the resulting spectral sequences. The core capabilities are:

• Computation. Minimal resolutions of modules over the Steenrod algebra $A$ at any prime $p$, with Yoneda products, Massey products, and secondary operations.

• Visualization. Interactive spectral sequence charts with pan/zoom, page navigation, product structlines, differentials, and per-generator detail panels.

• Differential propagation. Enter known differentials and propagate consequences via the Leibniz rule, naturality, the long exact sequence in Ext, and Moss’ theorem. The deduction engine applies 11 distinct mathematical passes in a fixed-point loop to derive all consequences.

• Contradiction detection. Speculatively assume a differential and check whether it leads to a contradiction, narrowing the space of possibilities by elimination.

• Motivic homotopy. Compute the motivic Adams spectral sequence, the $C\tau$ Ext module, and the algebraic Novikov spectral sequence. The $\tau$-LES (iterated long exact sequence from the $C\tau$ cofiber sequence) computes $\tau$-torsion orders and constrains differentials via Chua’s Lemma 12.4.

• Cross-validation. Systematic comparison against reference data from Isaksen, BFCC, LWX, and Bruner–Rognes, with a test suite verifying 7 independent consistency checks across 5 spectral sequences.

Modes

htpy has two main modes:

• The Archive — a curated collection of pre-computed spectral sequence data for the sphere spectrum, organized by spectral sequence type. These are read-only and serve as a reliable reference.

• The Playground — upload your own module definitions, explore the resulting spectral sequences, add labels and differentials, run the deduction engine, and investigate patterns interactively.

Lineage

The computation engine builds on the Ext computation machinery originally developed in ext-rs by Hood Chatham, Dexter Chua, and Joey Beauvais-Feisthauer. The Groebner basis module is ported from SSeqCpp by Weinan Lin. htpy extends these with a web-based viewer, an archival format, a deduction engine for differential propagation, motivic computations, and tools for working with the $C\tau$ bridge.

Source code

htpy is open source. The repository is hosted on sourcehut:

https://git.sr.ht/~maxmj/htpy

+++ 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

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

+++ title = “The Playground” section = “features” +++

The Playground

The Playground is where you work with your own spectral sequences. You can import module definitions, explore the resulting Ext charts, and annotate them with differentials, labels, and notes.

Importing modules

There are several ways to add a module to the Playground:

• Build a new module using the Module Builder
• Import a JSON file — either a module definition (which htpy will resolve on the fly) or a pre-computed spectral sequence in v1 or v2 format
• Attach a cell to an existing module to construct a cofiber (see Cell Complexes and Cofibers)
• Compute from a template — select a spectrum from the compute page and specify the desired range

Working with differentials

See Working with Differentials for the full guide. In summary:

• Add differentials — specify $d_r$ by clicking source and target
• Mark $d_r = 0$ — record that a class survives page $r$
• Mark $d_r = {?}$ — flag as unresolved (blocks deduction)
• Delete differentials — removes the differential and all propagated consequences, replaying from scratch

The deduction engine

See The Deduction Engine for the full guide. The “Deduce” button runs the automated reasoning engine; “Deep Deduce” adds elimination by contradiction.

Vanishing lines

You can specify vanishing lines — linear constraints above which all classes vanish. Format: $a \cdot s > b \cdot n + c$ with optional stem bounds. These are used by the deduction engine and are automatically propagated through cofiber sequences.

Labels and annotations

• Custom labels on generators at any bidegree — overrides the auto-inferred name from product propagation
• Named combinations — named linear combinations of basis elements (useful for identifying specific classes in higher-dimensional groups)
• Detects — record which stable homotopy element each generator detects (e.g., $h_0$ detects 2, $h_1$ detects $\eta$)
• Annotations — notes with tags (question, todo, proof, reference) attached to classes, differentials, or structlines

All user data is saved automatically to ~/.htpy/ and persists across sessions.

Recomputing

You can recompute a module at a different range (larger stem or filtration) from its module definition. This re-resolves the module and regenerates the Ext data. You can choose whether to keep or discard existing user differentials.

Computation options

From the compute pages, you can specify:

+++ title = “The Viewer” section = “features” +++

The Viewer

The spectral sequence viewer is the main interface for exploring computations in htpy. It displays the $E_r$ pages of a spectral sequence as a chart in the $(t-s, s)$ plane.

Navigation

• Pan — click and drag the chart background
• Zoom — scroll wheel or pinch gesture
• Select a class — click on a dot to open the detail panel. When multiple generators sit at the same bidegree, the dot closest to your click is selected

The detail panel

Clicking a class opens a panel showing:

• The bidegree $(t-s, s)$ and the internal degree $t$
• The dimension of the group at that bidegree
• Generator names — one input per generator. User-entered names override automatically inferred names (from product propagation)
• Named combinations — named linear combinations of basis elements, defined by selecting coefficients
• Differentials — known $d_r$ differentials originating from or landing in this bidegree, with delete buttons for user-entered ones
• Products — nontrivial products with named generators
• Massey products — computed brackets and their indeterminacy
• Detects — record which stable homotopy element a generator detects (e.g., $h_0$ detects 2, $h_1$ detects $\eta$)
• Annotations — sticky notes with tags (question, todo, proof, reference)

Clicking differentials and structlines

You can click differential lines and product structlines in the chart. Clicking a differential shows its page, source, target, origin (base computation or user-entered), and the dimension of source and target groups on each page. Clicking a structline shows the product name, shift, and relation formula.

Both detail views include buttons to navigate to the source or target class.

Page selection

The page scrubber at the top selects the $E_r$ page. Use the left/right arrow keys to step through pages, Home for $E_2$, and End for $E_\infty$. The viewer shows the surviving classes and differentials for the selected page.

Tabs

The tab bar lets you switch between multiple open modules. Click a module in the dropdown to open it in a new tab; click a tab to switch. Tab state (scroll position, zoom, selected class) is preserved.

Visual indicators

• Green diamonds mark classes identified as permanent cycles (surviving to $E_\infty$)
• Hollow circles mark $\tau$-torsion generators (motivic modules)
• Vanishing lines are drawn as dashed lines
• Orange ring on a class in differential entry mode
• Orange “?” marker for unknown differentials

Motivic features

For modules with motivic weight data:

• Weight filter dropdown: View a single weight slice at a time, filtering all nodes, structlines, and differentials by weight.
• Weight annotations: The detail panel shows the weight of each generator.
• $\tau$-torsion order: Shown in the detail panel; hollow circles in the chart distinguish torsion from non-torsion generators.

Export

• Export JSON — download the full computation data in htpy’s v2 archive format
• Lean certificate — download a Lean 4 file that formally verifies the Ext computation (available for resolvable modules)

+++ title = “The Module Builder” section = “features” +++

The Module Builder

The Module Builder lets you define new modules over the Steenrod algebra and compute their Adams spectral sequences.

Defining a module

A module definition specifies:

• Prime — the prime $p$ (currently 2, 3, 5, or 7)
• Type — the type of module (e.g., “finite dimensional module”)
• Generators — a list of generators with their degrees
• Actions — the Steenrod algebra actions on the generators ($\operatorname{Sq}^i$ for $p = 2$, or $P^i$ and $\beta$ for odd primes)

The JSON format

Module definitions are JSON objects. See Module Definition Format for the complete specification. A minimal example for $p = 2$:

{
  "type": "finite dimensional module",
  "p": 2,
  "gens": { "x0": 0, "x1": 1 },
  "actions": ["Sq1 x0 = x1"]
}

Cell complexes and cofibers

You can build modules as cell complexes — attaching cells to an existing module. See Cell Complexes and Cofibers for the full workflow.

The “Take Cofiber” workflow:

1. In the viewer, select a class at filtration 1 on the $E_\infty$ page.
2. Click “Take Cofiber” to open the builder with a pre-filled module definition.
3. The builder auto-checks the Steenrod operations suggested by the attaching map.
4. Submit to compute the cofiber’s spectral sequence.

The resulting module tracks its provenance — the parent module and attaching data — which enables the deduction engine to compute naturality maps automatically.

Computation range

When you submit a module definition, htpy resolves it to compute Ext groups. The default computation range is $n \leq 30$, $s \leq 7$, but you can adjust this when recomputing from the viewer.

Limitations

• The module builder is currently available for the Adams spectral sequence only. Motivic Adams, CESS, and algebraic Novikov modules must be provided as JSON definitions directly.
• At most $p = 7$ is supported (limited by the bit-packing in the linear algebra layer).

+++ title = “Working with Differentials” section = “features” +++

Working with Differentials

The differential workflow is htpy’s core interactive feature. You can enter known differentials, mark unknowns, propagate consequences via the Leibniz rule, and run the deduction engine to automatically derive all consequences.

Three-state differential tracking

htpy tracks differentials in three states:

• Nonzero: $d_r(x) = y$ for a specific nonzero target $y$. Displayed as a colored arrow from source to target in the chart.
• Zero: $d_r(x) = 0$, meaning $x$ survives page $r$. Recorded internally but not drawn (the class remains on the chart).
• Unknown: $d_r(x) = {?}$, meaning the differential is deliberately marked as unresolved. Displayed as an orange “?” marker. Unknown differentials block the deduction engine at that source/page pair, preventing it from making assumptions.

Adding a nonzero differential

1. In the viewer, ensure you are on a Playground module (not an archive module).
2. Click the source class to select it.
3. In the detail panel, click “Add differential” (or use the keyboard shortcut).
4. Click the target class. The viewer will determine the page $r$ from the bidegree shift.
5. If the source or target has dimension $> 1$, you will be prompted to choose specific basis vectors.
6. Choose whether to propagate via Leibniz rule: if checked, htpy will automatically compute all consequences through the product structure.

Marking $d_r = 0$

Click a class and use the “$d_r = 0$” button in the detail panel. This records that the class survives page $r$. If Leibniz propagation is enabled, htpy will propagate: $d_r(h \cdot x) = 0$ for all products $h$ where $h \cdot x$ is nonzero and survives to $E_r$.

Marking $d_r = {?}$ (unknown)

Click a class and use the “$d_r = {?}$” button. This flags the differential as deliberately unresolved. The deduction engine will not attempt to determine $d_r(x)$ at this bidegree/page until the unknown marker is removed.

This is useful when you know a differential exists but don’t yet know the exact target — it prevents the deduction engine from incorrectly concluding $d_r = 0$ via the degree argument.

Deleting a differential

Click on a differential line (or find it in the detail panel) and click “Delete”. htpy will:

1. Remove the differential and all its Leibniz-propagated consequences.
2. Replay all remaining user differentials from scratch to ensure consistency.

This replay-from-scratch approach guarantees that deleting one differential never leaves the spectral sequence in an inconsistent state.

Leibniz propagation

When you add a differential with Leibniz propagation enabled, htpy applies the Leibniz rule:

$$d_r(h \cdot x) = d_r(h) \cdot x + (-1)^{|h|}, h \cdot d_r(x)$$

For product generators $h$ from $E_2$ (where $d_r(h) = 0$ for structural reasons):

• Nonzero propagation: $d_r(x) = y \implies d_r(h \cdot x) = \pm h \cdot y$
• Zero propagation: $d_r(x) = 0 \implies d_r(h \cdot x) = 0$

The propagation uses a BFS through the product graph, discovering all transitive consequences. Propagated differentials are marked with a propagated flag and are automatically removed when the source differential is deleted.

Contradiction detection

If you enter a differential that contradicts existing data (e.g., $d_r(x) = y$ when $d_r(x) = 0$ is already established), htpy will reject the entry with an error message. The viewer also prevents entering $d_r(x)$ when $d_s(x) = {?}$ is marked for any $s < r$ (the unknown must be resolved first).

Recommended workflow

For research exploration with the deduction engine:

1. Enter vanishing lines first. These give the deduction engine the most leverage for the degree argument.
2. Mark known permanent cycles (or let the engine detect them automatically via the sparsity argument).
3. Enter known differentials from the literature, with Leibniz propagation enabled.
4. Run the deduction engine (“Deduce” button) to propagate all consequences.
5. Review the deduction report to see what was derived and why.
6. Iterate: enter newly discovered information and re-run.

+++ title = “The Deduction Engine” section = “features” +++

The Deduction Engine

The deduction engine is htpy’s automated reasoning system for spectral sequence differentials. It applies a sequence of mathematically justified passes in a fixed-point loop, deriving all consequences of the data you provide.

Running the engine

From the viewer, click the “Deduce” button in the header bar. The engine will:

1. Apply all deduction passes iteratively until convergence.
2. Display a summary report showing how many differentials were derived by each pass.
3. Update the chart with all newly established differentials and permanent cycles.

The “Deep Deduce” button runs the same passes but also enables the elimination by contradiction pass, which speculatively tests candidate differentials and eliminates those leading to inconsistencies. This is slower but more powerful.

What the engine uses

The deduction engine takes as input:

• The current spectral sequence state (Ext dimensions, products, established differentials)
• User-entered differentials (nonzero, zero, and unknown)
• Vanishing lines
• Naturality maps (from cofiber sequences)
• Massey products (computed from the resolution)
• Known permanent cycles (from a lookup table for standard spectra)
• Motivic data (generator weights, $\tau$-torsion orders) when available

The deduction report

After running, the engine reports:

Seeding the engine

The engine is most effective when given good starting data:

Vanishing lines

Specify a line above which all classes vanish. Format: $a \cdot s > b \cdot n + c$ where $n$ is the stem and $s$ the filtration. Vanishing lines are automatically propagated through cofiber sequences using the long exact sequence bound.

Known permanent cycles

For standard spectra ($S^0$ at $p = 2$ and $p = 3$), htpy includes a lookup table of known permanent cycles ($h_0, h_1, h_2, h_3, \eta, \nu, \sigma$, etc.). These seed the product propagation pass.

For cofiber modules, permanent cycles are inherited from the parent: if $x$ is a known permanent cycle in $M$ and the inclusion $i^* : \operatorname{Ext}(C) \to \operatorname{Ext}(M)$ has a preimage of $x$ with trivial kernel, the preimage is seeded as a permanent cycle in $C$.

Cofiber sequences

When a module is constructed as a cofiber (via the “Take Cofiber” workflow), htpy automatically:

1. Computes the inclusion map $i^* : \operatorname{Ext}(C) \to \operatorname{Ext}(M)$
2. Computes the projection map $\pi^* : \operatorname{Ext}(C/M) \to \operatorname{Ext}(C)$
3. Propagates vanishing lines through the LES
4. Enables naturality, reverse naturality, and LES subcomplex passes

Mathematical details

For the precise mathematical statement and justification of each pass, see Deduction Engine: Mathematical Justification.

+++ title = “Products and Massey Products” section = “features” +++

Products and Massey Products

htpy computes and displays the multiplicative structure of Ext, including Yoneda products, Massey products, and matric Massey products.

Yoneda products

The Yoneda product on $\operatorname{Ext}_A(M, \mathbb{F}_p)$ is computed by composing chain maps along the minimal resolution. For the sphere spectrum, the standard generators are:

Products with these generators are displayed as structlines in the chart: lines connecting a class $x$ to $h_i \cdot x$.

Viewing products

In the toolbar, each product has a toggle button. Click to show/hide its structlines. The detail panel for any class shows all nontrivial products involving that class.

Product colors

Each product generator has a distinct color in the chart:

• $h_0$: vertical lines (filtration $+1$, stem $+0$)
• $h_1$: diagonal lines (filtration $+1$, stem $+1$)
• $h_2$: steeper diagonal (filtration $+1$, stem $+3$)

Massey products

When $\alpha\beta = 0$ and $\beta\gamma = 0$ in Ext, the Massey product $\langle \alpha, \beta, \gamma \rangle$ is a coset in Ext modulo the indeterminacy $\alpha \cdot \operatorname{Ext} + \operatorname{Ext} \cdot \gamma$.

htpy computes Massey products at the chain level:

1. Find null homotopies $a$ and $b$ with $d(a) = \alpha\beta$ and $d(b) = \beta\gamma$.
2. The representative is $a\gamma + \alpha b$.
3. Indeterminacy generators are computed from the kernel of the null homotopy construction.

Viewing Massey products

Computed Massey products are displayed in the detail panel when you select a class. Each entry shows:

• The factors $\alpha, \beta, \gamma$ with their bidegrees
• The computed value (as a linear combination of Ext generators)
• The indeterminacy (as a list of generators spanning the coset)

4-fold Massey products

htpy also computes $\langle \alpha, \beta, \gamma, \delta \rangle$ when all consecutive products and 3-fold sub-brackets vanish. These require additional null homotopies and have larger indeterminacy.

Matric Massey products

Matric Massey products generalize ordinary Massey products to matrices of Ext elements. Given matrices $A, B, C$ with $AB = 0$ and $BC = 0$, the matric bracket $\langle A, B, C \rangle$ is computed. htpy discovers matric vanishing relations automatically by searching for pairs of Ext elements whose products satisfy the required identities.

Role in the deduction engine

Products and Massey products feed into the deduction engine in several ways:

• Leibniz propagation (Pass 2): Differentials propagate through products via the Leibniz rule.
• Permanent cycle propagation (Pass 1.5): Products of permanent cycles are permanent.
• Moss’ theorem (Pass 1.6): The Massey product structure constrains differentials via the higher Leibniz rule.
• $E_r$ Massey products: Brackets on higher pages detect permanent cycles via Moss’ theorem (Belmont–Kong, Theorem 3.13).

+++ title = “Cell Complexes and Cofibers” section = “features” +++

Cell Complexes and Cofibers

htpy supports building new spectra from existing ones by attaching cells, constructing cofiber sequences, and using the induced long exact sequence for deduction.

Taking cofibers

The primary workflow for building cell complexes:

1. In the viewer, navigate to the $E_\infty$ page of a module.
2. Select a class at filtration 1 (these correspond to maps of spectra, i.e., potential attaching maps).
3. Click “Take Cofiber” in the detail panel.
4. Choose between:
   • Review: Opens the module builder with suggested Steenrod operations pre-checked. You can adjust before computing.
   • Quick compute: Constructs the cofiber definition automatically and computes immediately.

The resulting cofiber module tracks its provenance — the parent module, the cell degree, and the attaching operations — enabling the deduction engine to compute naturality maps automatically.

Built-in cell complexes

htpy includes several standard cell complexes:

These are available from the Cell Complexes tab on the compute page. Each complex specifies its cells, attaching maps, and expected generator names.

The long exact sequence

For a cofiber sequence $M \xrightarrow{f} C \to C/M$, the long exact sequence in Ext:

$$\cdots \to \operatorname{Ext}^s(C/M) \xrightarrow{\delta} \operatorname{Ext}^{s+1}(M) \xrightarrow{f^*} \operatorname{Ext}^{s+1}(C) \to \cdots$$

provides three maps that the deduction engine uses:

• Inclusion $i^*$: Transfers differentials from $C$ to $M$ (Pass 1.75).
• Projection $\pi^*$: Computed automatically; enables reverse naturality and LES subcomplex arguments.
• Connecting homomorphism $\delta$: Computed via the chain-level snake lemma.

Vanishing line propagation

Vanishing lines propagate through cofiber sequences. If the parent module $M$ and the root module have vanishing lines, htpy computes a vanishing line for the cofiber $C$ using the long exact sequence bound:

$$\operatorname{Ext}^s(C) = 0 \text{ when both } \operatorname{Ext}^s(M) = 0 \text{ and } \operatorname{Ext}^{s-1}(C/M) = 0$$

The propagated vanishing line is computed from the slopes and intercepts of the parent and root vanishing lines, adjusted by the cell connectivity.

The cell complex builder

The standalone Cell Complex Builder (accessible from the landing page) lets you define cell complexes from scratch:

1. Specify cells (dimension and name).
2. Define attaching maps as Steenrod algebra elements evaluated at a stem value.
3. Preview the module definition JSON.
4. Compute and view the result.

The builder includes a scalar evaluator that translates expressions like Sq4 Sq2 Sq1 into the corresponding module action.

+++ title = “Spectral Sequences” section = “mathematics” +++

Spectral Sequences

A spectral sequence is an algebraic gadget that computes homological invariants through a sequence of successive approximations. It consists of a sequence of pages $(E_r, d_r)$ for $r = 2, 3, 4, \ldots$, where each page is a bigraded abelian group and $d_r$ is a differential ($d_r \circ d_r = 0$) whose homology gives the next page:

$$E_{r+1}^{s,t} = \frac{\ker(d_r : E_r^{s,t} \to E_r^{s+r, t+r-1})}{\operatorname{im}(d_r : E_r^{s-r, t-r+1} \to E_r^{s,t})}$$

The idea is that $E_2$ is something computable (typically an Ext group), the differentials $d_r$ encode obstructions, and the spectral sequence converges to the object you actually want to compute.

Why spectral sequences?

Many problems in algebraic topology reduce to extension problems that are too hard to solve directly. Spectral sequences break these problems into a sequence of manageable steps. The trade-off is bookkeeping: tracking which classes survive, which differentials are nonzero, and how the pages relate to each other.

This is where computational tools like htpy become valuable. The combinatorial data in a spectral sequence — dimensions, differentials, product structures — is well-suited to machine computation and visualization.

The spectral sequences htpy computes

htpy works with several interrelated spectral sequences:

These are connected by natural maps, comparison theorems, and the Gheorghe–Wang–Xu isomorphism $\operatorname{Ext}{A{\mathrm{mot}}}(C\tau, \mathbb{F}2) \cong \operatorname{Ext}{BP_BP}(BP_, BP_*)$. See the Motivic Adams and $C\tau$ Bridge sections for details.

Chart conventions

htpy displays spectral sequences in the $(t-s, s)$ plane:

• The stem $n = t - s$ is the horizontal axis
• The Adams filtration $s$ is the vertical axis

Differentials $d_r : E_r^{s,t} \to E_r^{s+r, t+r-1}$ go one step to the left and $r$ steps up in this chart. Product structlines connect classes related by multiplication with standard generators ($h_0, h_1, h_2, \ldots$ at $p = 2$).

+++ title = “The Adams Spectral Sequence” section = “mathematics” +++

The Adams Spectral Sequence

The Adams spectral sequence is the primary computational tool in stable homotopy theory. For a spectrum $X$, it takes the form

$$E_2^{s,t} = \operatorname{Ext}_A^{s,t}(H^*(X; \mathbb{F}_p),; \mathbb{F}p) \implies \pi{t-s}(X)^\wedge_p$$

where $A$ is the mod-$p$ Steenrod algebra and the convergence is to the $p$-completed stable homotopy groups.

The $E_2$ page

htpy computes the $E_2$ page — that is, the Ext groups $\operatorname{Ext}_A^{s,t}(M, \mathbb{F}_p)$ for an $A$-module $M$ — by constructing a minimal free resolution of $M$ over $A$:

$$\cdots \to F_2 \xrightarrow{d_2} F_1 \xrightarrow{d_1} F_0 \xrightarrow{\varepsilon} M \to 0$$

where each $F_s$ is a free module over the Steenrod algebra. “Minimal” means the differentials have no linear (degree 0) component, ensuring the resolution is as small as possible. The dimension of the degree-$t$ part of $F_s$ equals $\dim \operatorname{Ext}_A^{s,t}(M, \mathbb{F}_p)$, so constructing the resolution directly gives the $E_2$ page.

Differentials

The $d_r$ differentials go

$$d_r : E_r^{s,t} \to E_r^{s+r, t+r-1}$$

In the $(t-s, s)$ chart, $d_r$ goes one step to the left and $r$ steps up. The first nontrivial differential $d_2$ can be computed algebraically via secondary Steenrod operations (following Bruner and Nassau). Higher differentials generally require geometric input or indirect arguments.

htpy’s deduction engine propagates known differentials using the Leibniz rule, naturality, Massey products (Moss’ theorem), and several other techniques. See Deduction Engine: Mathematical Justification for the complete list.

Products

The Adams spectral sequence carries a product structure induced by the Yoneda product in Ext:

$$\operatorname{Ext}_A^{s_1, t_1}(M, \mathbb{F}_p) \otimes \operatorname{Ext}_A^{s_2, t_2}(M, \mathbb{F}_p) \to \operatorname{Ext}_A^{s_1 + s_2,; t_1 + t_2}(M, \mathbb{F}_p)$$

htpy computes products with standard generators by composing chain maps along the resolution. At $p = 2$, the generators are $h_i \in \operatorname{Ext}^{1, 2^i}$ corresponding to the Hopf invariant one elements. The products are displayed as structlines in the viewer.

This product structure is essential for the Leibniz rule:

$$d_r(a \cdot x) = d_r(a) \cdot x + (-1)^{|a|} a \cdot d_r(x)$$

When $a$ is a permanent cycle ($d_r(a) = 0$ for all $r$), this simplifies to $d_r(a \cdot x) = \pm a \cdot d_r(x)$, allowing differentials to propagate multiplicatively through the spectral sequence.

Massey products

When $\alpha \beta = 0$ and $\beta \gamma = 0$ in Ext, the Massey product $\langle \alpha, \beta, \gamma \rangle$ is defined as a coset in Ext. htpy computes Massey products at the chain level using the Yoneda resolution and tracks indeterminacy explicitly. These are used by the deduction engine via Moss’ theorem to derive differentials from the $E_r$ Massey bracket structure.

The sphere spectrum at $p = 2$

The archive module S_2 contains the Adams spectral sequence for $S^0$ at $p = 2$:

• $E_2$ page: $\operatorname{Ext}_A(\mathbb{F}_2, \mathbb{F}_2)$ through stem 90
• $d_2$ differentials from the BFCC secondary resolution
• Higher differentials from the LWX machine proofs
• Products with $h_0, h_1, h_2, h_3, h_4$
• Named generators following classical conventions

The archive module S_3 contains the corresponding data at $p = 3$ through stem 120.

+++ title = “How htpy Computes” section = “mathematics” +++

How htpy Computes

htpy computes Ext groups over the Steenrod algebra by constructing minimal free resolutions. This page gives an overview of the computational pipeline.

Minimal resolutions

To compute $\operatorname{Ext}_A(M, \mathbb{F}_p)$, htpy constructs a minimal free resolution

$$\cdots \to F_2 \xrightarrow{d_2} F_1 \xrightarrow{d_1} F_0 \xrightarrow{\varepsilon} M \to 0$$

where each $F_s$ is a free module over the Steenrod algebra. “Minimal” means that the differentials have no linear (degree 0) component, which ensures that the resolution is as small as possible.

The dimension of the degree-$t$ part of $F_s$ equals $\dim \operatorname{Ext}_A^{s,t}(M, \mathbb{F}_p)$. So constructing the resolution directly gives the $E_2$ page.

The algorithm

The resolution is built inductively. At each homological degree $s$, htpy:

1. Row reduces the matrix representing $d_s$ to compute the kernel (the $s$-cycles).
2. Extends to surjection by adding new generators for $F_{s+1}$ to cover the kernel.
3. Computes the quasi-inverse $q_s$ satisfying $q_s \circ d_s = \mathrm{id}$ on the image, which is used for chain map lifting.

The key computational bottleneck is linear algebra over $\mathbb{F}_p$ — specifically, row reduction of large matrices representing the Steenrod algebra action.

Linear algebra

htpy uses bit-packed vector representations for efficient $\mathbb{F}_p$ arithmetic:

• At $p = 2$: each vector is a sequence of bits packed into 64-bit limbs. Row reduction uses the Method of Four Russians (M4RI), which processes $k$ rows at a time using lookup tables. With NEON SIMD on ARM, this achieves 1–17 $\mu$s for typical resolution matrices (50–2000 rows).

• At odd primes: elements of $\mathbb{F}_p$ are packed into $\lceil \log_2 p \rceil$ bits per entry. Row reduction uses an adapted M4RI with $k$-scaling optimized for each prime. At $p = 3$, performance is 4.1–4.8$\times$ slower than $p = 2$ due to the larger field arithmetic.

Motivic resolutions

For the motivic Steenrod algebra $A_{\mathrm{mot}}$, the resolution carries an additional weight grading. htpy resolves one weight at a time within each $(s, t)$ step, with a fast-path that skips degrees where all modules have dimension zero (saving 70–95% of row reductions at large $t$).

The motivic resolution uses a wavefront scheduler for parallelism: each $(s, t)$ step depends on $(s, t-1)$ and $(s-1, t)$, forming a diagonal wavefront that can be parallelized across weight values. On a 96-core machine, this gives a 3.8$\times$ speedup for the motivic sphere at $s = 15$, $t = 60$.

Products

The product structure on Ext (the Yoneda product) is computed by composing chain maps along the resolution. For the sphere spectrum, the products with standard generators $h_0, h_1, h_2, \ldots$ give the structlines displayed in the viewer.

Concretely, to compute the product $h_i \cdot x$ for $x \in \operatorname{Ext}^{s,t}$, htpy:

1. Represents $h_i$ as a chain map $\tilde{h}i : F\bullet \to F_\bullet[1, 2^i]$.
2. Evaluates $\tilde{h}_i$ on the generator representing $x$.
3. Reads off the result in $\operatorname{Ext}^{s+1, t+2^i}$.

The chain map is constructed once and cached for reuse across all products.

Massey products

For Massey products $\langle \alpha, \beta, \gamma \rangle$ where $\alpha\beta = 0$ and $\beta\gamma = 0$:

1. Lift $\alpha, \beta, \gamma$ to chain-level cocycles.
2. Construct null homotopies $a$ and $b$ satisfying $d(a) = \alpha\beta$ and $d(b) = \beta\gamma$ via the quasi-inverse.
3. The Massey product is represented by $a\gamma + \alpha b$ at the chain level, with indeterminacy from the choices of $a$ and $b$.

htpy computes both 3-fold and 4-fold Massey products, as well as matric Massey products (where $\alpha, \beta, \gamma$ are matrices of Ext elements).

From algebra to the web

The computation pipeline connects to the web viewer as follows:

1. A module definition (JSON) specifies the module $M$ over the Steenrod algebra.
2. The resolution engine (htpy-resolution) computes the minimal resolution and extracts Ext groups, differentials, and products.
3. The result is serialized into htpy’s v2 archive format — a JSON structure containing the spectral sequence data.
4. The web server (htpy-web) serves the data to the browser, where the viewer renders it as an interactive chart.

For archive modules, steps 1–3 are done ahead of time and the pre-computed data is embedded in the binary. For playground modules, the resolution is computed on the fly when you import a module definition.

+++ title = “The Motivic Adams Spectral Sequence” section = “mathematics” +++

The Motivic Adams Spectral Sequence

The motivic Adams spectral sequence is the Adams spectral sequence in motivic homotopy theory over $\operatorname{Spec} \mathbb{Z}$. It is trigraded by stem, filtration, and motivic weight, and converges to the motivic stable homotopy groups.

Setup

The motivic Steenrod algebra $A_{\mathrm{mot}}$ over $\mathbb{F}2$ is generated by Steenrod squares $\operatorname{Sq}^i$ subject to the Adem relations, but now carries a weight grading. In htpy’s conventions, a degree is a pair $(t, w)$ where $t$ is the internal degree and $w$ is the weight. The element $\tau \in \pi{0,-1}$ plays a central role: it has stem 0, filtration 0, and weight $-1$.

The motivic Adams spectral sequence takes the form

$$E_2^{s,t,w} = \operatorname{Ext}{A{\mathrm{mot}}}^{s,t,w}(\mathbb{F}2,; \mathbb{F}2) \implies \pi{t-s,w}(S^{0,0}{\mathrm{mot}})^\wedge_2$$

htpy computes the $E_2$ page by constructing a minimal free resolution of $\mathbb{F}2$ over $A{\mathrm{mot}}$, keeping track of the weight grading at each step.

Weight grading

Each generator of Ext has a well-defined weight $w$. The key constraint is:

Differentials preserve weight. The motivic Adams differential $d_r : E_r^{s,t,w} \to E_r^{s+r, t+r-1, w}$ has weight 0.

This is the basis of the weight degree argument (Pass 1.1 in the deduction engine): if the source and target of a potential $d_r$ have no generators at a common weight, then $d_r = 0$.

$\tau$-torsion

The element $\tau$ acts on $\operatorname{Ext}{A{\mathrm{mot}}}$ by shifting weight by $-1$. An element $x$ is $\tau$-torsion if $\tau^k \cdot x = 0$ for some $k \geq 1$. The minimal such $k$ is the $\tau$-torsion order of $x$.

$\tau$-torsion is a structural invariant of the $E_2$ page — it does not change across pages of the spectral sequence. The $\tau$-torsion orders constrain differentials in several ways:

1. $\tau$-torsion obstruction (Pass 1.2): If $x$ has torsion order $k$, then $d_r(x)$ must land in an element with compatible torsion order $\leq k$. If no such target exists, $d_r(x) = 0$.

2. $\tau$-survival (Pass 1.3): If $x$ has torsion order $k$, then $d_r(x) = 0$ for all $r \leq k$. This follows from Chua’s Lemma 12.4: $\tau^k$-torsion classes lie in $\operatorname{im}(d_{k+1})$, so they survive until page $E_{k+1}$.

3. $\tau$-target forcing (Pass 3): If $x$ has exact torsion order $k$, then $x \in \operatorname{im}(d_{k+1})$. When the source of $d_{k+1}$ is 1-dimensional and the target is uniquely determined, the differential is forced.

See Deduction Engine: Mathematical Justification for the precise statements.

Computing $\tau$-torsion

htpy computes $\tau$-torsion orders from the long exact sequence in Ext associated to the cofiber sequence

$$0 \to \Sigma^{0,1}\mathbb{F}_2 \xrightarrow{i} C\tau \xrightarrow{\pi} \mathbb{F}_2 \to 0$$

The connecting homomorphism $\delta : \operatorname{Ext}^s(\mathbb{F}_2) \to \operatorname{Ext}^{s+1}(\Sigma^{0,1}\mathbb{F}_2)$ detects $\tau$-torsion:

$$x \in \operatorname{im}(\delta_{s-1}) \iff x \text{ is } \tau\text{-torsion}$$

For higher torsion orders, htpy uses the iterated LES: the short exact sequence $0 \to \Sigma^{0,1}C_{k-1} \to C_k \to \mathbb{F}_2 \to 0$ where $C_k = \mathbb{F}_2[\tau]/(\tau^k)$ gives a connecting homomorphism $\delta_k$ whose image detects ${x : \tau^{k-1} \cdot x = 0}$. The exact torsion order is $\min{m : x \in \operatorname{im}(\delta_m)}$.

See $C\tau$ Bridge for the full story.

The archive module S_2_mot

The archive module S_2_mot contains:

• $E_2$ page through stem 110, filtration 55
• $\tau$-torsion orders (computed via iterated LES for $k \leq 4$, supplemented by Isaksen’s CSV data at higher stems)
• Differentials $d_2$ through $d_6$ from Isaksen’s tables
• Products with $h_0, h_1, h_2, h_3$
• Weight annotations per generator

In the viewer, $\tau$-torsion generators are displayed with hollow circles and their torsion order is shown in the detail panel. The weight filter dropdown allows viewing a single weight slice at a time.

+++ title = “The Cτ Bridge” section = “mathematics” +++

The $C\tau$ Bridge

The $C\tau$ bridge connects the motivic Adams spectral sequence to the algebraic Novikov spectral sequence via the Gheorghe–Wang–Xu theorem. It provides a powerful tool for computing $\tau$-torsion orders and constraining motivic differentials.

The cofiber of $\tau$

In motivic homotopy theory, $\tau \in \pi_{0,-1}(S^{0,0}{\mathrm{mot}})$ is the element detecting the algebraic $K$-theory class. Its cofiber $C\tau$ fits into a short exact sequence of $A{\mathrm{mot}}$-modules:

$$0 \to \Sigma^{0,1}\mathbb{F}_2 \xrightarrow{;i;} C\tau \xrightarrow{;\pi;} \mathbb{F}_2 \to 0$$

Here $i$ is the top cell inclusion (the generator at weight 1 maps to $\tau \cdot \iota$, where $\iota$ is the bottom cell) and $\pi$ is the bottom cell projection.

As an $A_{\mathrm{mot}}$-module, $C\tau \cong \mathbb{F}_2[\tau]/(\tau^2)$: it has two generators $\iota$ at degree $(0, 0)$ and $\tau\iota$ at degree $(0, 1)$, with $\tau \cdot \iota = \tau\iota$ and all Steenrod squares acting as zero.

The Gheorghe–Wang–Xu theorem

Theorem (Gheorghe–Wang–Xu, 2018). There is an isomorphism of trigraded $\mathbb{F}_2$-algebras:

$$\operatorname{Ext}{A{\mathrm{mot}}}^{s,t,w}(C\tau,; \mathbb{F}2) ;\cong; \operatorname{Ext}{BP_BP}^{s, 2(t-s)-w}(BP_,; BP_*)$$

Moreover, the $C\tau$ Adams spectral sequence collapses at $E_2$: all differentials are zero.

This is a remarkable result: it identifies the Ext of a simple motivic module ($C\tau$, a two-cell complex) with the Adams–Novikov $E_2$ page, which is one of the deepest objects in stable homotopy theory.

Consequence for htpy. Since the $C\tau$ spectral sequence collapses, every generator of $\operatorname{Ext}(C\tau)$ is a permanent cycle. This is used directly by Pass B of the deduction engine.

The long exact sequence in Ext

Applying $\operatorname{Ext}{A{\mathrm{mot}}}(-, \mathbb{F}_2)$ to the short exact sequence above gives a long exact sequence:

$$\cdots \to \operatorname{Ext}^s(\mathbb{F}_2) \xrightarrow{\pi^} \operatorname{Ext}^s(C\tau) \xrightarrow{i^} \operatorname{Ext}^s(\Sigma^{0,1}\mathbb{F}_2) \xrightarrow{;\delta;} \operatorname{Ext}^{s+1}(\mathbb{F}_2) \to \cdots$$

where all Ext groups are taken over $A_{\mathrm{mot}}$.

Detecting $\tau$-torsion

The connecting homomorphism $\delta$ detects $\tau$-torsion:

$$x \in \operatorname{im}(\delta_{s-1}) \iff x \text{ is } \tau\text{-torsion in } \operatorname{Ext}^s(\mathbb{F}_2)$$

This follows from the exact sequence: $x \in \ker(\pi^)$ if and only if $\tau \cdot x = 0$ (since $\pi$ is the quotient by $\tau$), and $\ker(\pi^) = \operatorname{im}(\delta)$ by exactness.

Implementation. htpy resolves $\mathbb{F}2$, $C\tau$, and $\Sigma^{0,1}\mathbb{F}2$ over $A{\mathrm{mot}}$, constructs chain maps lifting $i$ and $\pi$, and computes the connecting homomorphism $\delta$ via the chain-level snake lemma. The rank of $\delta{s-1}$ at each tridegree $(s, t, w)$ gives the number of $\tau$-torsion generators.

Computing higher torsion orders

For $\tau$-torsion order (not just detection), htpy uses the iterated LES. Define $C_k = \mathbb{F}_2[\tau]/(\tau^k)$, so $C_2 = C\tau$. For each $k \geq 2$, there is a short exact sequence:

$$0 \to \Sigma^{0,1}C_{k-1} \xrightarrow{;i_k;} C_k \xrightarrow{;\pi_k;} \mathbb{F}_2 \to 0$$

The connecting homomorphism $\delta_k$ of this sequence detects $\tau^{k-1}$-torsion:

$$T_{k-1} := \operatorname{im}(\delta_k) = {x \in \operatorname{Ext}(\mathbb{F}_2) : \tau^{k-1} \cdot x = 0}$$

The exact torsion order of $x$ is

$$\operatorname{ord}(x) = \min{m \geq 1 : x \in T_m}$$

with $\operatorname{ord}(x) = 0$ if $x$ is not $\tau$-torsion.

Early termination. The iterated LES terminates when an iteration produces no new torsion globally. In practice, for the sphere at $p = 2$:

• Order 1 torsion first appears at stem 1 ($h_1$)
• Order 2 torsion first appears at stem 40
• Orders 3 and 4 appear at still higher stems

Chain map computation

htpy constructs the chain maps $\tilde{i}$ and $\tilde{\pi}$ lifting the module maps $i$ and $\pi$ to the resolution level. At homological degree $s = 0$, the chain maps are given directly by the module maps. At $s > 0$, the chain maps are extended inductively using the lift_generators_via_qi routine, which lifts generators through the quasi-inverse of the resolution differential.

The connecting homomorphism $\delta$ is then computed by the standard construction: given $x \in \operatorname{Ext}^s(\Sigma^{0,1}\mathbb{F}_2)$, lift to a chain in the $C\tau$ resolution via $\tilde{i}^{-1}$ (the chain-level homotopy), apply $d$, and project via $\tilde{\pi}$ to get $\delta(x) \in \operatorname{Ext}^{s+1}(\mathbb{F}_2)$.

Validation

htpy cross-validates the $C\tau$ computation in several ways:

• $d^2 = 0$: verified through $s \leq 6$, $t \leq 15$ for the motivic resolution of $C\tau$.
• GWX isomorphism: $C\tau$ Ext dimensions match the algebraic Novikov $E_2$ page from Isaksen’s CSV through $s \leq 8$, stem $\leq 20$.
• $\tau$-torsion counts: $\operatorname{rank}(\delta_{s-1})$ matches Isaksen’s CSV $\tau$-torsion counts at all 86 tridegrees tested ($s \leq 8$, stem $\leq 30$).
• $\pi^ \circ \tilde{i} = 0$*: the composition of chain maps from the short exact sequence is verified to be zero.

The archive modules

• S_2_mot: The motivic Adams $E_2$ page with $\tau$-torsion orders, computed via the iterated LES and supplemented by Isaksen’s CSV at higher stems.
• S_2_ctau: The $\operatorname{Ext}(C\tau)$ module, with generator names matched from the algebraic Novikov CSV via the GWX isomorphism.
• S_2_nov: The algebraic Novikov $E_2$ page, imported from Isaksen’s CSV data for comparison.

References

• B. Gheorghe, G. Wang, and Z. Xu, The special fiber of the motivic deformation of the stable homotopy category is algebraic, Acta Math. 226 (2021), no. 2, 319–407.
• D. Chua, The $E_3$ page of the Adams spectral sequence, 2021.
• D.C. Isaksen, Stable stems, Mem. Amer. Math. Soc. 262 (2019), no. 1269.

+++ title = “The Cartan-Eilenberg Spectral Sequence” section = “mathematics” +++

The Cartan–Eilenberg Spectral Sequence

The Cartan–Eilenberg spectral sequence (CESS) arises from the factorization of the Steenrod algebra into its polynomial and exterior parts. It provides a way to compute the Adams $E_2$ page from simpler pieces.

Setup

The dual Steenrod algebra $A_*$ at $p = 2$ factors as

$$A_* \cong P_* \otimes E_*$$

where $P_* = \mathbb{F}2[\xi_1, \xi_2, \ldots]$ is the polynomial part and $E* = E(\tau_0, \tau_1, \ldots)$ is the exterior part. Dually, the Steenrod algebra $A$ has subalgebras $P^$ and quotient $E^ = A // P^*$.

The CESS takes the form

$$E_2^{s,u} = \operatorname{Ext}_{P^}^{s}(\mathbb{F}2,; \operatorname{Ext}{E^}^{u}(\mathbb{F}_2, \mathbb{F}_2)) \implies \operatorname{Ext}_A^{s+u}(\mathbb{F}_2, \mathbb{F}_2)$$

where the target is the Adams $E_2$ page. Since $\operatorname{Ext}_{E^*}(\mathbb{F}_2, \mathbb{F}_2) \cong \mathbb{F}_2[q_0, q_1, q_2, \ldots]$ (a polynomial algebra on classes $q_i$ of degree $2^{i+1} - 1$), the CESS $E_2$ page is

$$\operatorname{Ext}_{P^*}(\mathbb{F}_2,; \mathbb{F}_2[q_0, q_1, \ldots])$$

What htpy computes

htpy resolves $\mathbb{F}_2[q_0, \ldots, q_N]$ as a module over $P^*$ using a minimal free resolution. This gives the CESS $E_2$ page directly. The resolution carries a CE-filtration (the $u$-grading from the exterior part) and a weight grading from the monomial structure of the polynomial module.

The same $E_2$ page serves double duty:

• As the CESS $E_2$ page converging to $\operatorname{Ext}_A(\mathbb{F}_2, \mathbb{F}_2)$ (the Adams $E_2$ page)
• As the algebraic Novikov spectral sequence (aNSS) $E_2$ page converging to $\operatorname{Ext}{BPBP}(BP_, BP_*)$ (the Adams–Novikov $E_2$ page)

The two spectral sequences share the same $E_2$ page but have different differentials.

CESS differentials

The CESS differentials $d_r : E_r^{s,u} \to E_r^{s+r, u-r+1}$ arise from the extension structure $P^* \to A \to E^*$ of Hopf algebras. In Adams coordinates, $d_r$ shifts by $(-1, +r)$ in the $(n, s)$ chart.

htpy computes CESS differentials via the deduction engine, using the degree argument, Leibniz propagation, convergence constraints (CESS $E_\infty$ must equal Adams $E_2$), and elimination by contradiction.

Cross-validation

The CESS computation is validated by two key checks:

• V1b: Per-stem totals of CESS $E_2$ dimensions are $\geq$ Adams $E_2$ dimensions (the CESS can only lose classes through differentials).
• V1c: CESS weight counts at each bidegree match the Ext dimension (weight decomposition is consistent).

The archive module S_2_cess

The archive module S_2_cess contains:

• The CESS/aNSS $E_2$ page through stem 30, filtration 16
• Computed using $q_0$ through $q_5$
• Generator names matched from the algebraic Novikov CSV where possible
• Weight annotations per generator

Limitations

• Currently $p = 2$ only. Odd-prime CESS requires generalizing the $P^*$ algebra degree formulas and the bitmask basis encoding.
• Algebraic CESS $d_2$ (from the Hopf extension structure, Ravenel A1.3.16) is not yet computed directly; instead, CESS differentials are derived via the deduction engine.

+++ title = “Deduction Engine: Mathematical Justification” section = “mathematics” +++

Deduction Engine: Mathematical Justification

htpy’s deduction engine applies a sequence of mathematically justified passes to derive differentials in a spectral sequence from known data. This page gives the precise statement and justification for each pass.

The engine operates as a fixed-point loop: it applies all passes in sequence, and repeats until no new information is discovered. Each pass produces either zero differentials ($d_r(x) = 0$) or nonzero differentials ($d_r(x) = y \neq 0$). Both are propagated through subsequent passes.

Overview of passes

Passes A and B are motivic-specific. Passes 1.1, 1.2, 1.3, and 3 apply only when weight and $\tau$-torsion data are available.

Pass 1: Degree argument

Statement. If $\dim E_r^{s+r, t+r-1} = 0$, then $d_r(x) = 0$ for all $x \in E_r^{s,t}$.

Justification. The differential $d_r : E_r^{s,t} \to E_r^{s+r, t+r-1}$ has codomain zero, so it is the zero map.

Implementation details. The pass iterates over $E_r$ generators (not just $E_2$ basis vectors) to catch surviving linear combinations that might have trivial targets even when $E_2$ does not. A secondary check identifies targets above a user-specified vanishing line, which also forces $d_r = 0$.

This is the workhorse pass: it resolves the majority of differentials in any computation where the $E_2$ page is sparse.

Pass 1.1: Weight degree argument

Statement. Let $x \in E_r^{s,t,w}$ in a motivic spectral sequence. If no generator of $E_r^{s+r, t+r-1}$ has weight $w$, then $d_r(x) = 0$.

Justification. The motivic Adams differential preserves weight: $d_r : E_r^{s,t,w} \to E_r^{s+r, t+r-1, w}$. If the target group has no elements at weight $w$, the differential must vanish.

Scope. This pass runs only when motivic weight data is available (the generator_weights map is nonempty). For classical (ungraded) spectral sequences, it is skipped.

Validation. Without the weight check, Pass 3 ($\tau$-target forcing) produced 189 of 212 false positive forced differentials. The weight constraint reduced this to 14 genuine forced differentials.

Pass 1.2: $\tau$-torsion obstruction

Statement. Let $x \in E_r^{s,t}$ with $\tau$-torsion order $\operatorname{ord}(x) = k > 0$. If no surviving generator of $E_r^{s+r, t+r-1}$ has $\tau$-torsion order in ${1, \ldots, k}$, then $d_r(x) = 0$.

Justification. The Yoneda product respects torsion: if $\tau^k \cdot x = 0$, then $\tau^k \cdot d_r(x) = d_r(\tau^k \cdot x) = 0$. So $d_r(x)$ must itself be $\tau$-torsion with order $\leq k$. If no element with compatible torsion order survives at the target bidegree, $d_r(x) = 0$.

Note. Non-torsion elements ($\operatorname{ord}(x) = 0$) are unconstrained by this pass — their image can have any torsion order.

Pass 1.3: $\tau$-survival

Statement. Let $x \in E_r^{s,t}$ with all nonzero $E_2$-basis components having $\tau$-torsion order $\geq k$. Then $d_r(x) = 0$ for all $r \leq k$.

Justification. By Chua [Lemma 12.4], if $x$ has $\tau$-torsion order $k$, then $x \in \operatorname{im}(d_{k+1})$ in the Adams spectral sequence. In particular, $x$ survives to the $E_{k+1}$ page, so $d_r(x) = 0$ for $r \leq k$.

The pass checks that all nonzero components of $x$ (in the $E_2$ basis) are $\tau$-torsion. If any component is non-torsion, the bound does not apply and the pass skips $x$.

Differs from Pass 1.2. Pass 1.2 checks whether the target has compatible torsion; Pass 1.3 uses only the source torsion order, unconditionally forcing $d_r = 0$ regardless of what the target looks like.

Reference. D. Chua, The $E_3$ page of the Adams spectral sequence, 2021, Lemma 12.4.

Pass 1.5: Permanent cycle detection

A class $x \in E_2^{s,t}$ is a permanent cycle if $d_r(x) = 0$ for all $r \geq 2$ — equivalently, $x$ survives to $E_\infty$. htpy detects permanent cycles via three mechanisms:

Sparsity argument

Statement. If $\dim E_r^{s+r, t+r-1} = 0$ for all $r \geq 2$ (in the computed range), then $x$ is a permanent cycle.

Justification. Every potential target of every $d_r$ is zero, so all differentials on $x$ vanish. Classes at the minimum stem are automatically permanent by connectivity.

Massey product argument

Statement. If $\langle \alpha, \beta, \gamma \rangle = \delta$ is a nonzero Massey product and all of $\alpha, \beta, \gamma$ are permanent cycles, then $\delta$ is a permanent cycle.

Justification. The Massey product construction is natural with respect to the spectral sequence filtration. Permanent factors produce a permanent result.

Product propagation

Statement. If $x$ is a permanent cycle and $h \in E_2$ is a product generator, then $h \cdot x$ is a permanent cycle (when nonzero).

Justification. By the Leibniz rule: $$d_r(h \cdot x) = d_r(h) \cdot x + (-1)^{|h|} h \cdot d_r(x)$$

Since $h \in E_2$ and $x$ is permanent, both terms vanish for all $r$.

Implementation. Permanent cycles are propagated via BFS through the product graph. The seed set consists of sparsity-detected cycles, Massey product cycles, and user-provided known permanent cycles (from a lookup table for standard spectra).

Pass 1.6: Moss’ theorem (Massey operations on spectral sequences)

This pass uses the structure of Massey products to derive differentials. It has four sub-cases.

Moss zero

Statement. If $\delta = \langle \alpha, \beta, \gamma \rangle$ and $d_r(\alpha) = d_r(\beta) = d_r(\gamma) = 0$, then $d_r(\delta) = 0$.

Justification. The Leibniz rule applied to the Massey product construction: when all factors survive page $r$, the bracket does too.

Moss forward

Statement. If $\delta = \langle \alpha, \beta, \gamma \rangle$ and all $d_r$ on the factors are determined, then $d_r(\delta)$ can be computed from the formula:

$$d_r(\delta) \equiv \pm, d_r(\alpha) \cdot \langle \beta, \gamma \rangle ;\pm; \alpha \cdot d_r(\beta) \cdot \gamma ;\pm; \langle \alpha, \beta \rangle \cdot d_r(\gamma) \pmod{\text{indeterminacy}}$$

where the signs depend on the total degrees of the factors (trivial at $p = 2$).

Justification. This is the higher Leibniz rule for Massey products, expressing $d_r$ of a bracket in terms of $d_r$ of the factors. The computation uses chain-level representatives from the resolution.

Indeterminacy. After computing $d_r(\delta)$, the pass checks whether the result is definitive modulo the Massey product’s indeterminacy coset. Three verdicts are possible:

• Definitive: the value is uniquely determined.
• Nonzero mod indeterminacy: the value is nonzero but the exact representative is ambiguous.
• Ambiguous: the indeterminacy coset contains both zero and nonzero elements; no conclusion.

Moss reverse

Statement. If $\delta = \langle \alpha, \beta, \gamma \rangle$, $d_r(\delta)$ is known, and all but one factor’s $d_r$ is determined, then the remaining factor’s $d_r$ can be solved by linear algebra.

Justification. The Moss formula is linear in each factor. Build the map $M : e_j \mapsto \langle \ldots, e_j, \ldots \rangle$ (Massey product with $e_j$ at the undetermined slot). If $M$ is injective, solve $M \cdot x = \text{residual}$ where the residual accounts for the known terms.

$E_r$ Massey products and Moss’ theorem

Statement. Let $\langle a’‘, a’, a \rangle_r$ be the $E_r$ Massey bracket (Belmont–Kong, Definition 3.11). If the crossing differentials hypothesis (Definition 2.4) holds — all factors survive to $E_r$ — and the bracket has a unique nonzero value with all indeterminacy generators permanent, then that value is a permanent cycle.

Justification. Moss’ theorem: an $E_r$ Massey bracket with permanent indeterminacy determines a permanent cycle. This is the spectral sequence analog of the classical Massey product permanence theorem.

Reference. E. Belmont and H. Kong, An algebraic approach to the Adams spectral sequence, Definition 2.4, Definition 3.11, and Theorem 3.13 (Moss).

Pass 1.75: Naturality

Statement. Let $\varphi : \operatorname{Ext}(A) \to \operatorname{Ext}(B)$ be the map induced by a map of spectra. If $d_r(x) = y$ in the spectral sequence for $A$ and $\varphi(x) \neq 0$ in $B$, then $d_r(\varphi(x)) = \varphi(y)$ in $B$.

Justification. Maps of spectra induce maps of spectral sequences that commute with all differentials: $d_r \circ \varphi_* = \varphi_* \circ d_r$.

Application. For a cofiber sequence $M \to C \to C/M$, the inclusion $i^* : \operatorname{Ext}(C) \to \operatorname{Ext}(M)$ transfers differentials from $C$ to $M$.

Pass 1.8: Reverse naturality

Statement. Let $\varphi : \operatorname{Ext}(C) \to \operatorname{Ext}(M)$ be an induced map. If $\varphi(e_i) = a$ in $M$, $d_r(a) = b$ is known in $M$, and $\varphi$ is injective at the target bidegree, then $d_r(e_i) = \varphi^{-1}(b)$ in $C$.

Justification. By naturality, $\varphi(d_r(e_i)) = d_r(\varphi(e_i)) = d_r(a) = b$. If $\varphi$ is injective at the target, $d_r(e_i)$ is uniquely determined by solving $\varphi(v) = b$.

Implementation. For each basis vector $e_i$ of the cofiber module whose image under $\varphi$ is a nonzero element $a$ in the parent: look up known differentials on $a$, check injectivity via rank computation, and solve the linear system $\varphi(v) = b$ by RREF of the augmented matrix $[\varphi^T \mid b]$.

Pass 1.85: LES subcomplex

Statement. Let $\varphi : \operatorname{Ext}(C) \to \operatorname{Ext}(M)$ be an induced map. Then $\ker(\varphi)$ and $\operatorname{im}(\varphi)$ are preserved by all differentials $d_r$.

• Kernel mode: If $x \in \ker(\varphi)$ and $\varphi$ is injective at the $d_r$ target bidegree (so $\ker(\varphi) = 0$ there), then $d_r(x) = 0$.

• Image mode: If $x \in \operatorname{im}(\varphi)$ and $\operatorname{im}(\varphi) = 0$ at the target bidegree, then $d_r(x) = 0$.

Justification. The long exact sequence in Ext induces sub-spectral sequences for $\ker$ and $\operatorname{im}$ of the connecting maps. If the subcomplex is zero at the target, the restricted differential vanishes.

This is a refinement of the degree argument: even when the full target group is nonzero, the relevant subgroup (kernel or image) may be trivial.

Pass 2: Leibniz propagation

Statement. The Leibniz rule for the Adams spectral sequence:

$$d_r(h \cdot x) = d_r(h) \cdot x + (-1)^{|h|}, h \cdot d_r(x)$$

For products $h$ from the $E_2$ page (which satisfy $d_r(h) = 0$ for structural reasons), this simplifies to:

• If $d_r(x) = 0$: then $d_r(h \cdot x) = 0$.
• If $d_r(x) = y \neq 0$: then $d_r(h \cdot x) = \pm, h \cdot y$.

Implementation. Both zero and nonzero Leibniz propagation use a BFS through the product graph. Starting from a newly established differential, the BFS applies the product matrices at each step and records all new consequences. A visited set prevents duplicate work.

Sign convention. At $p = 2$, all signs are trivial. At odd primes $p$, the sign $(-1)^{|h|}$ contributes a factor of $p - 1 \equiv -1 \pmod{p}$ when the total degree of $h$ is odd.

Ordering. Leibniz propagation (Pass 2) runs after all zero-producing passes (1 through 1.85) in each iteration. This ensures that all zero constraints are visible before any nonzero forcing occurs, preventing cascading contradictions.

Pass 3: $\tau$-target forcing

Statement. Let $x \in E_2^{s,t}$ have exact $\tau$-torsion order $k$. Then $x \in \operatorname{im}(d_{k+1})$. If the source of $d_{k+1}$ at the appropriate bidegree is 1-dimensional and there is a unique $E_{k+1}$-surviving element with order $k$ at the target, then the nonzero differential $d_{k+1}(\text{source}) = x$ is forced.

Justification. By Chua Lemma 12.4, $\tau^k$-torsion elements must be killed by $d_{k+1}$. When the source and target are both uniquely determined (1-dimensional), the differential is completely forced.

Safety checks. This pass includes three guards against false positives:

1. Weight compatibility. The source and target must have matching motivic weight ($d_r$ preserves weight). Without this check, 189 of 212 candidates were false positives.

2. Already-determined guard. If $d_{k+1}$ is already determined by an earlier pass, skip (to avoid contradictions).

3. Unknown-set guard. If the user has marked $d_{k+1}(x)$ as “unknown” (deliberately undetermined), skip.

Ordering. Pass 3 runs after Leibniz zero propagation (Pass 2), not before. This is critical: if Pass 3 forces $d_{k+1}(y) = x$ but Leibniz in the same iteration would independently establish $d_{k+1}(y) = 0$, the result is a contradiction. Running Pass 3 last ensures all zero constraints are already in place.

Reference. D. Chua, The $E_3$ page of the Adams spectral sequence, 2021, Lemma 12.4.

Pass A: Classical lifting ($\tau$-inversion)

Statement. Let $d_r(x) = y$ be a known differential in the classical Adams spectral sequence. Then the same differential holds in the motivic Adams spectral sequence at the top weight $w = n + s$ (where $n$ is the stem and $s$ the filtration).

Justification. The classical Adams spectral sequence embeds into the motivic one at the top weight slice: the $\tau$-localization map sends motivic classes at weight $w = n + s$ to their classical counterparts. Known classical differentials lift directly.

Implementation. The classical staircase data is extracted, generator indices are shifted to account for the motivic generator ordering (which places top-weight generators at the end), and both zero and nonzero differentials are transferred.

Pass B: $C\tau$ permanent cycle survival

Statement. Let $\pi^* : \operatorname{Ext}{A{\mathrm{mot}}}(\mathbb{F}2, \mathbb{F}2) \to \operatorname{Ext}{A{\mathrm{mot}}}(C\tau, \mathbb{F}_2)$ be the map induced by the projection $C\tau \to \mathbb{F}_2$. If all generators in $\pi^*(x)$ are permanent cycles in the $C\tau$ Adams spectral sequence, then $x$ is a permanent cycle in the motivic Adams spectral sequence.

Justification. By the Gheorghe–Wang–Xu theorem, the $C\tau$ Adams spectral sequence collapses at $E_2$: all differentials are zero and all generators are permanent. Naturality of $\pi^$ then gives: if $\pi^(x) \neq 0$ in $\operatorname{Ext}(C\tau)$, the only way $x$ could support a nonzero $d_r$ is if $\pi^(d_r(x)) = d_r(\pi^(x)) = 0$, which requires $\pi^*(x)$ to be in the image of a differential — but there are no nonzero differentials in the $C\tau$ spectral sequence.

Reference. B. Gheorghe, G. Wang, and Z. Xu, The special fiber of the motivic deformation of the stable homotopy category is algebraic, 2018.

Elimination by contradiction

In addition to the passes above, the deduction engine has a global elimination pass that does not rely on any single mathematical theorem but instead uses proof by contradiction.

Algorithm. For each bidegree with an undetermined differential $d_r(x)$:

1. Enumerate all possible values of $d_r(x)$ (up to a configurable cap, typically $2^{10}$ candidates).
2. For each candidate value $v$:
   • Checkpoint the spectral sequence state.
   • Speculatively set $d_r(x) = v$.
   • Run the degree argument to propagate consequences.
   • Check for contradictions (e.g., $d_r(y) = 0$ and $d_r(y) \neq 0$ simultaneously, or dimension violations).
   • Rollback to the checkpoint.
3. If all candidates except one lead to a contradiction, force the surviving candidate.

Soundness. This is exhaustive search over a finite set: each candidate is either consistent or contradictory, and at least one must be consistent (the true value of $d_r$). If exactly one survives, it must be the true value.

Proof logging. The engine records which candidates were eliminated and why, providing an audit trail for the forced differential.

Fixed-point convergence

The deduction engine terminates when a complete iteration of all passes produces no new information. Specifically, it tracks 17 counters (one per pass/sub-pass) and exits when all are zero in a single iteration.

Termination guarantee. Each pass only adds information (setting a previously unknown differential to a definite value). Since the number of undetermined differentials is finite and strictly decreasing, the loop must terminate.

Typical behavior. For the sphere spectrum $S^0$ at $p = 2$ with stem $\leq 90$ and filtration $\leq 15$, the engine converges in 3–5 iterations with the degree argument resolving the majority of differentials and Leibniz propagation handling the rest.

Extensibility

The deduction engine is designed to be extensible. Each pass is a standalone function that inspects the current spectral sequence state and produces new differential information. Adding a new pass requires:

1. Writing a function that iterates over bidegrees, checks a mathematical condition, and calls add_differential when the condition is met.
2. Adding the function call to the main loop in the appropriate position (zero-producing passes before Leibniz, nonzero-producing passes after).
3. Adding a counter to DeductionResult for tracking.

The staircase data structure provides the necessary queries: undetermined_sources() to find unknowns, e_r_dimension() and e_r_gens() to inspect pages, add_differential() to record results, and try_diff() with checkpoint/rollback for speculative reasoning.

See Extending the Deduction Engine for implementation details.

+++ title = “Cross-Validation Methodology” section = “mathematics” +++

Cross-Validation Methodology

htpy computes five interrelated spectral sequences. These computations are not independent: they are connected by natural maps, comparison theorems, and convergence relationships. htpy exploits these connections as a validation framework, checking that independently computed data agrees where it should.

The validation checks

htpy implements 7 systematic checks, labeled V1 through V7. Each compares two independently computed datasets:

V1: CESS $E_2$ $\geq$ Adams $E_2$ (per-stem totals)

$$\sum_s \dim E_2^{s,n+s}(\text{CESS}) ;\geq; \sum_s \dim E_2^{s,n+s}(\text{Adams})$$

Justification. The CESS converges to the Adams $E_2$ page. Differentials can only decrease dimensions, so the $E_2$ page is at least as large as $E_\infty$.

Sub-checks:

• V1b: Per-bidegree inequality (stronger, but sensitive to the $h_0$ generator placement between $E^$ and $P^$).
• V1c: CESS weight counts at each bidegree match Ext dimensions.

V3: aNSS $E_2$ $\geq$ aNSS $E_\infty$ (per-stem totals)

$$\sum_s \dim E_2^{s,n+s}(\text{aNSS}) ;\geq; \sum_s \dim E_\infty^{s,n+s}(\text{aNSS})$$

Justification. Same reasoning as V1: the aNSS differentials can only decrease dimensions.

Sub-check V3b: aNSS $d_2$ matrix dimensions match $E_2$ dimensions at both source and target bidegrees (849 entries verified).

V5: $C\tau$ Ext $\geq$ Novikov $E_2$ generator counts

$$\dim \operatorname{Ext}^{s,t,w}(C\tau) ;\geq; \text{(Novikov CSV generator count)}$$

Justification. By the Gheorghe–Wang–Xu isomorphism, $C\tau$ Ext equals the Adams–Novikov $E_2$ page. The CSV generator counts may undercount due to $h_0$-tower truncation, so the inequality is $\geq$.

V6: Motivic Adams (JSON) = Isaksen CSV $E_2$

Four sub-checks:

• V6: Round-trip CSV $\to$ JSON fidelity (dimensions match at every tridegree).
• V6b: Per-stem $E_2 \geq E_\infty$ monotonicity.
• V6c: $d_2$ matrix dimensions match $E_2$ at source and target.
• V6d: Metadata consistency (weight ranges, torsion flags).

V7: $\tau$-free motivic Adams $E_2$ = Classical Adams $E_2$

$$\dim \operatorname{Ext}{A{\mathrm{mot}}}^{s,t,t}(\mathbb{F}_2, \mathbb{F}_2) ;=; \dim \operatorname{Ext}_A^{s,t}(\mathbb{F}_2, \mathbb{F}_2)$$

Justification. At the top weight $w = t$ (equivalently $w = n + s$), the motivic Steenrod algebra reduces to the classical Steenrod algebra. The $\tau$-free (top-weight) part of the motivic $E_2$ page equals the classical $E_2$ page.

Verified for $n = 1, \ldots, 33$ and $s \leq 9$.

Test suite

All checks are implemented as automated tests in tests/cross_validate_ss.rs. The test suite runs as part of cargo test (quick checks) and cargo test -- --ignored (full validation including expensive CSV parsing).

Reference data sources

What “validated” means

When htpy says a computation is “validated,” it means:

1. The computation was performed independently by htpy’s resolution engine.
2. The output was compared against at least one external reference dataset.
3. All applicable V-checks passed within the overlapping range.

This does not constitute a formal proof. For formal verification, htpy can export Lean 4 certificates that check $d^2 = 0$ and exactness of the resolution.

+++ title = “Architecture Overview” section = “technical” +++

Architecture Overview

htpy is organized as a Rust workspace with 14 crates. The core computation is pure Rust with no external dependencies beyond the standard library; the web interface uses Axum and Askama.

Crate dependency graph

                    htpy-fp
                      |
                  htpy-algebra
                      |
               +------+------+
               |      |      |
          htpy-sseq   |   htpy-resolution
               |      |      |
               +------+------+
                      |
              htpy-deduction
                      |
          +-----------+-----------+
          |           |           |
     htpy-web    htpy-wasm    htpy-tools
     (local)     (browser)    (CLI)

Supporting crates: htpy-fp, htpy-once, htpy-bivec, htpy-maybe-rayon, htpy-archive, htpy-groebner.

Core crates

htpy-fp

Field arithmetic and linear algebra over $\mathbb{F}_p$.

• Bit-packed vector representation (FpVector, FqVector)
• Matrix operations with M4RI (Method of Four Russians)
• NEON SIMD on ARM, optimized odd-prime row reduction
• Subspace computation, affine subspaces

htpy-algebra

The Steenrod algebra and module categories.

• AdemAlgebra, MilnorAlgebra: both bases of the Steenrod algebra
• MotivicAdemAlgebra: the motivic Steenrod algebra over $\mathbb{F}_2$
• PStarAlgebra: the polynomial subalgebra $P^*$ (for CESS)
• Module types: finite-dimensional, free, $C\tau$, truncated-$\tau$, $P^$-polynomial, $P^$-exterior
• Generic grading framework: Grading trait with i32 (classical) and MotivicDegree (trigraded) instances

htpy-sseq

Spectral sequence data structures and deduction algorithms.

• Sseq<P>: bigraded spectral sequence with differential tracking
• Staircase data structure: per-bidegree echelon form with level encoding for page-by-page survival
• Deduction algorithms: degree argument, Leibniz propagation, Moss’ theorem, $E_r$ Massey products, elimination by contradiction
• Profile-specific implementations: StaircaseSseq<Adams>, StaircaseSseq<Cess> with motivic and CESS deduction passes

htpy-resolution

Minimal free resolution engine.

• Resolution: classical resolution of $A$-modules
• MotivicResolution<T>: motivic resolution, generic over target module
• Chain map computation and connecting homomorphism
• Yoneda products and Massey products (3-fold, 4-fold, matric)
• $\tau$-torsion via iterated LES (motivic_chain_map.rs)
• resolution_core.rs: shared two-phase resolution step (extend_resolution_matrix + finalize_resolution_step)

htpy-deduction

Standalone deduction engine (extracted from htpy-web).

• run_deduction(): 11-pass fixed-point loop
• Types: UserDifferential, DiffKnowledge, VanishingLine, NaturalityInput, DeductionResult
• Can be used by htpy-web, htpy-wasm, and future CLI tools

htpy-web

Axum web server with embedded viewer.

• Routes for archive browsing, computation, deduction, export
• Askama HTML templates with Canvas-based chart renderer
• Module library with persistence to ~/.htpy/
• Build binaries for generating archive data (build_motivic, build_ctau, build_cess, build_novikov)

Data flow

Module definition (JSON)
        |
        v
htpy-resolution: minimal free resolution
        |
        v
htpy-archive: ComputationRecord (Ext dims, products, diffs)
        |
        v
htpy-web: ChartData (pre-computed pages, products, annotations)
        |
        v
Browser: Canvas renderer (pan/zoom, selection, detail panel)

Parallelism

htpy uses optional parallelism via the concurrent Cargo feature, which enables rayon through htpy-maybe-rayon. Without it, all computation is sequential (useful for WASM targets).

Parallel workloads:

• Classical resolution wavefront scheduler (diagonal parallelism)
• Motivic resolution weight batching within each $(s, t)$ step
• LES chain map and homotopy inner loops
• Cofiber/fiber resolution via rayon::join

+++ title = “Extending the Deduction Engine” section = “technical” +++

Extending the Deduction Engine

The deduction engine is designed to be extensible. This page explains how to add new deduction passes that apply novel mathematical arguments to derive differentials.

Architecture

The deduction engine lives in two crates:

• htpy-deduction (engine.rs): The main run_deduction() function that orchestrates passes, manages the fixed-point loop, and accumulates results.
• htpy-sseq (staircase_deduction.rs, staircase_deduction_motivic.rs): Lower-level algorithms that operate on the staircase data structure directly.

A deduction pass is a function that:

1. Inspects the current spectral sequence state.
2. Identifies bidegrees where a mathematical argument applies.
3. Calls sseq.add_differential() to record new information.
4. Returns a count of newly established differentials.

The staircase data structure

The staircase stores per-bidegree data in echelon form:

• Levels: Each $E_2$ generator has a “level” encoding when it dies. Level $\leq$ LEVEL_PERM means permanent cycle; level $=$ LEVEL_MAX $- r$ means killed by $d_r$.
• Basis: Sparse $\mathbb{F}_2$ vectors (Int1d) representing each generator.
• Diffs: Option<Int1d> for each generator’s determined differential.

Key queries:

#![allow(unused)]
fn main() {
// Iterate over generators with unknown differentials
sseq.undetermined_sources(bidegree)

// Dimension of E_r at a bidegree
sseq.e_r_dimension(bidegree, r)

// Iterate over E_r generators (surviving to page r)
sseq.e_r_gens(bidegree, r)

// Check if a bidegree has any d_r target at pages >= r
sseq.has_any_target(bidegree, r)

// Add a differential (returns true if new information)
sseq.add_differential(page, &source, target_slice)
}

Writing a new pass

Step 1: Write the pass function

A typical pass has this structure:

#![allow(unused)]
fn main() {
fn my_new_pass(
    sseq: &mut Sseq<Adams>,
    // ... additional data your pass needs ...
) -> (DeduceResult, Vec<(i32, Bidegree, FpVector)>) {
    let mut result = DeduceResult::Unchanged;
    let mut leibniz_queue = Vec::new();

    // Phase 1: Collect candidates (avoid borrow conflicts)
    let mut candidates = Vec::new();
    for b in sseq.iter_bidegrees() {
        for r in 2..sseq.max_page_at(b) {
            // Check your mathematical condition
            if my_condition_holds(sseq, b, r) {
                candidates.push((r, b, zero_vector));
            }
        }
    }

    // Phase 2: Apply candidates
    for (r, b, target) in candidates {
        let source = sseq.e_r_gen(b, r);
        if sseq.add_differential(r, &source, &target) {
            result = DeduceResult::Changed;
            leibniz_queue.push((r, b, source));
        }
    }

    (result, leibniz_queue)
}
}

The two-phase pattern (collect then apply) is important to avoid borrow conflicts: the collection phase reads from the sseq, and the application phase mutates it.

Step 2: Add to the main loop

In engine.rs, add your pass call in the appropriate position:

• Zero-producing passes (concluding $d_r = 0$): Add between Pass 1.85 and Pass 2 (Leibniz). Push results to leibniz_queue for downstream propagation.
• Nonzero-producing passes (forcing $d_r \neq 0$): Add after Pass 2 (Leibniz) to ensure all zero constraints are visible first.

Step 3: Add tracking

Add a counter to DeductionResult:

#![allow(unused)]
fn main() {
pub struct DeductionResult {
    // ... existing fields ...
    pub my_new_pass_count: usize,
}
}

Include the counter in the fixed-point convergence check and in the deduction report.

Speculative reasoning

For passes that need to test hypothetical differentials:

#![allow(unused)]
fn main() {
// Checkpoint the current state
let checkpoint = sseq.checkpoint();

// Speculatively set a differential
sseq.add_differential(r, &source, &candidate);

// Check for contradictions
let contradiction = run_degree_argument(sseq).is_err();

// Rollback
sseq.rollback(checkpoint);

if contradiction {
    // This candidate is impossible
}
}

The try_diff() method wraps this pattern. The elimination pass (deduce_diff_4_nd) enumerates all $2^k$ candidates for a $k$-dimensional source/target and eliminates those leading to contradictions.

Example: Adding a new zero-producing pass

Suppose you want to add a pass that uses the Kudo transgression theorem: if $x$ is in the image of a Kudo transgression, then $d_r(x) = 0$ for certain values of $r$.

1. Write deduce_kudo_transgression(sseq, kudo_data) following the two-phase pattern above.
2. Add kudo_zeros: usize to DeductionResult.
3. In engine.rs, call it after Pass 1.85 and before Pass 2.
4. Push new zeros to leibniz_queue.
5. Include kudo_zeros in the fixed-point check.

The engine’s convergence guarantee is preserved as long as your pass only adds information (never removes established differentials).

DiffReason enum

Each established differential carries a DiffReason recording why it was derived. To add a new reason:

#![allow(unused)]
fn main() {
pub enum DiffReason {
    // ... existing variants ...
    KudoTransgression,
}
}

This enables the proof logging / audit trail system to track which mathematical argument justified each differential.

+++ title = “The Archive Format” section = “technical” +++

The Archive Format (v2)

htpy uses a self-describing JSON archive format for storing and exchanging spectral sequence data. The format has two entity types: ModuleDefinition (input) and ComputationRecord (output).

ModuleDefinition

A module definition specifies an $A$-module:

{
  "htpy_archive": "module_definition",
  "version": 2,
  "algebra": { "type": "adem", "p": 2 },
  "generators": [
    { "name": "x0", "degree": 0 },
    { "name": "x4", "degree": 4 }
  ],
  "actions": [
    { "op": "Sq4", "input": "x0", "output": { "x4": 1 } }
  ]
}

Fields:

ComputationRecord

A computation record stores the output of an Ext computation:

{
  "htpy_archive": "computation_record",
  "version": 2,
  "prime": 2,
  "coordinate_system": "adams",
  "max_stem": 60,
  "max_filtration": 15,
  "num_gens": [[0, 0, 1], [1, 1, 1], ...],
  "products": { "h0": { "bidegree": [0, 1], "matrices": [...] } },
  "differentials": [...],
  "generator_names": [...]
}

Fields:

Product matrices

Each product entry specifies the bidegree shift and a list of matrices:

{
  "h0": {
    "bidegree": [0, 1],
    "matrices": [
      { "source": [0, 0], "matrix": [[1]] },
      { "source": [1, 1], "matrix": [[1, 0], [0, 1]] }
    ]
  }
}

The matrix at source bidegree $(n, s)$ has dimensions $\dim \operatorname{Ext}^{s,n+s} \times \dim \operatorname{Ext}^{s+s_h, n+n_h+s+s_h}$ where $(n_h, s_h)$ is the product’s bidegree shift.

Differential matrices

Each differential entry specifies a page, source bidegree, and matrix:

{ "page": 2, "source": [14, 2], "matrix": [[1, 0, 1]] }

The matrix has dimensions $\dim E_2^{s,n+s} \times \dim E_2^{s+r, n-1+s+r}$.

Motivic extensions

For motivic spectral sequences, the computation record includes:

• has_weight: true
• weight_range: [min_w, max_w]
• Per-generator weights: [w_1, w_2, ...] in each node
• Per-generator tautorsion: [k_1, k_2, ...] ($\tau$-torsion orders)

Content hashing

Module definitions include a SHA-256 content hash computed from the canonical JSON serialization (sorted keys, no whitespace). This allows verification that a computation record was produced from a specific module definition.

Backward compatibility

The v2 format uses the JSON field htpy_archive (with serde(alias = "homotopy_archive") for backward compatibility with the v1 field name). The loader tries v2 first, then falls back to v1 format.

+++ title = “Module Definition Format” section = “technical” +++

Module Definition Format

htpy accepts module definitions in JSON format. A module definition specifies a module $M$ over the Steenrod algebra $A$, which htpy then resolves to compute $\operatorname{Ext}_A(M, \mathbb{F}_p)$.

Minimal example

A module with two generators and one Steenrod square action:

{
  "type": "finite dimensional module",
  "p": 2,
  "gens": { "x0": 0, "x1": 1 },
  "actions": ["Sq1 x0 = x1"]
}

Fields

Required

Module types

• "finite dimensional module": Explicitly specified generators and actions. Most common.
• "finitely presented module": Generators plus relations (quotient of a free module).

Actions format

The actions field is an array of strings, each specifying one Steenrod operation:

"Sq<i> <gen> = <linear combination>"

At $p = 2$:

• "Sq1 x0 = x1" means $\operatorname{Sq}^1(x_0) = x_1$
• "Sq2 x0 = x1 + x2" means $\operatorname{Sq}^2(x_0) = x_1 + x_2$
• "Sq4 x0 = 0" means $\operatorname{Sq}^4(x_0) = 0$

At odd primes:

• "P1 x0 = x1" means $P^1(x_0) = x_1$
• "b x0 = x1" means $\beta(x_0) = x_1$

Actions not listed are assumed to be zero. The Steenrod algebra relations (Adem relations) are checked automatically; specifying an action that violates the Adem relations will produce an error.

The v2 archive format

For interoperability, module definitions can also use the v2 archive format with structured actions:

{
  "htpy_archive": "module_definition",
  "version": 2,
  "algebra": { "type": "adem", "p": 2 },
  "generators": [
    { "name": "x0", "degree": 0 },
    { "name": "x1", "degree": 1 }
  ],
  "actions": [
    { "op": "Sq1", "input": "x0", "output": { "x1": 1 } }
  ]
}

See The Archive Format for the complete specification.

Examples

The mod-2 Moore spectrum

$C(2) = S^0 \cup_2 e^1$: a sphere with a cell attached via the degree-2 map.

{
  "type": "finite dimensional module",
  "p": 2,
  "gens": { "i": 0, "j": 1 },
  "actions": ["Sq1 i = j"]
}

The Joker

A 5-cell complex with specific Steenrod structure:

{
  "type": "finite dimensional module",
  "p": 2,
  "gens": { "x0": 0, "x1": 1, "x2": 2, "x3": 3, "x4": 4 },
  "actions": [
    "Sq1 x0 = x1",
    "Sq2 x0 = x2",
    "Sq1 x2 = x3",
    "Sq2 x2 = x4",
    "Sq4 x0 = x4"
  ]
}

Computation range

When importing a module definition, htpy prompts for the computation range:

• max stem ($n_{\max}$): maximum value of $t - s$
• max filtration ($s_{\max}$): maximum homological degree

Larger ranges produce more data but take longer to compute. The resolution time scales roughly as $O(n_{\max}^2 \cdot s_{\max})$ for typical modules.

+++ title = “Acknowledgements” section = “root” +++

Acknowledgements

htpy builds on a substantial body of prior work in both software and mathematics. This page records the contributions that have made the project possible.

Software

htpy’s computation engine descends from two open-source projects:

ext-rs — Hood Chatham, Dexter Chua, and Joey Beauvais-Feisthauer. The Rust library ext-rs (MIT / Apache-2.0) implements minimal free resolutions over the Steenrod algebra with Yoneda and Massey products, secondary operations, and $\mathbb{F}_p$ linear algebra. htpy’s crates htpy-fp (vector and matrix arithmetic, M4RI row reduction), htpy-algebra (Adem and Milnor basis implementations, module types, free module homomorphisms), and htpy-resolution (the classical resolution engine, chain map lifting, Yoneda products, Massey products, secondary operations) are direct descendants of ext-rs code. The augmented-matrix resolution step, the quasi-inverse machinery, and the $\mathbb{F}_2$ bit-packed vector representation all originate in ext-rs.

SSeqCpp — Weinan Lin. The C++ library SSeqCpp (Apache-2.0) implements spectral sequence computation using Groebner bases over polynomial rings. htpy-groebner is a Rust port of SSeqCpp’s Buchberger algorithm, including the fixed-size monomial representation, the divisibility trie for leading-term reduction, and the critical-pair management with Buchberger criteria.

Reference data

htpy validates its computations against several published datasets:

Daniel C. Isaksen — Motivic and classical Adams spectral sequence charts. CSV data for the $E_2$ through $E_\infty$ pages of the classical Adams, motivic Adams, and algebraic Novikov spectral sequences. Source: Zenodo 6987157 and Zenodo 6987227. These datasets are the primary reference for cross-validating htpy’s motivic resolution and $C\tau$ computation.

Joey Beauvais-Feisthauer, Hood Chatham, and Dexter Chua — The $E_2$ page of the 2-primary Adams spectral sequence in a large range. Source: Zenodo 7339848 (CC BY 4.0). Provides $\operatorname{Ext}_A$ ranks through stem 256, $d_2$ differentials through stem 200, and all Yoneda products with $h_0$ through $h_6$.

Robert Bruner and John Rognes — The cohomology of the mod 2 Steenrod algebra (arXiv:2109.13117). SQLite database with the full Ext computation including named generators, basis elements, and relations. Source: Zenodo 7786290.

Weinan Lin, Guozhen Wang, and Zhouli Xu — Machine proofs for Adams differentials and extension problems among CW spectra (arXiv:2412.10876). Machine-proved Adams differentials and complete spectral sequence data for 220 CW spectra. Source: Zenodo 14475507 (CC BY 4.0).

Mathematics

The algorithms and theoretical foundations draw on work by many people. The following contributions are directly used in htpy’s code:

Minimal resolutions and Ext computation. The resolution algorithm (row reduce, extend to surjection, compute quasi-inverse) is standard homological algebra. The augmented-matrix formulation with chain-map/differential/identity segments was developed in ext-rs.

The Steenrod algebra. The Adem basis implementation follows the classical construction via admissible sequences. The Milnor basis implementation uses the coproduct formulas of J.W. Milnor (1958). Both support arbitrary primes $p$.

M4RI row reduction. The Method of Four Russians for $\mathbb{F}_2$ matrix operations, as described by Albrecht, Bard, and Hart. htpy’s implementation includes SIMD vectorization for x86-64 (AVX2/AVX-512) and aarch64 (NEON).

The motivic Steenrod algebra. The motivic Adem algebra and its bigraded structure follow Voevodsky’s construction, with conventions as in Dugger–Isaksen.

The Gheorghe–Wang–Xu theorem. The identification $\operatorname{Ext}{A{\mathrm{mot}}}(C\tau, \mathbb{F}2) \cong \operatorname{Ext}{BP_BP}(BP_, BP_*)$ and the collapse of the $C\tau$ Adams spectral sequence at $E_2$ are due to Bogdan Gheorghe, Guozhen Wang, and Zhouli Xu (Acta Math. 226, 2021).

$\tau$-torsion and differentials. The connection between $\tau$-torsion order and Adams differentials — specifically, that $\tau^k$-torsion classes lie in $\operatorname{im}(d_{k+1})$ — is Lemma 12.4 of Dexter Chua’s paper “The $E_3$ page of the Adams spectral sequence” (2021, arXiv:2105.07628). This result powers Passes 1.3 and 3 of the deduction engine.

Massey products and Moss’ theorem. The deduction engine’s use of $E_r$ Massey brackets follows the framework of Eva Belmont and Hana Kong (“An algebraic approach to the Adams spectral sequence”), specifically Definitions 2.4 and 3.11 and Theorem 3.13.

Secondary Steenrod operations. The $d_2$ computation via pair algebras follows Hans-Joachim Baues (“The algebra of secondary cohomology operations”) and Christian Nassau (“On the secondary Steenrod algebra”).

Vanishing lines. The propagation of vanishing lines through cofiber sequences uses Lemma 6.3 of Brian Johnson (“Quantitative Bounds for Nilpotence and Vanishing Lines”).

The Cartan–Eilenberg spectral sequence. The CESS and algebraic Novikov spectral sequence setup follows Douglas Ravenel (“Complex Cobordism and Stable Homotopy Groups of Spheres”, 2003), particularly the treatment of the $P_*$-comodule Ext computation.

Classical and motivic computations. The computation of stable stems via the motivic approach is due to Daniel Isaksen, Guozhen Wang, and Zhouli Xu (“Stable homotopy groups of spheres”, Proc. Natl. Acad. Sci. 117, 2020). The motivic Adams charts and naming conventions follow Isaksen (“Stable stems”, Mem. Amer. Math. Soc. 262, 2019).

The Kervaire invariant problem. The CW-spectrum data and machine-proved differentials used for cross-validation are from Weinan Lin, Guozhen Wang, and Zhouli Xu (“On the Last Kervaire Invariant Problem”, 2024, arXiv:2412.10879).

Textbooks

The following textbooks inform the mathematical background throughout:

• J.F. Adams, Stable Homotopy and Generalised Homology, Chicago Lectures in Mathematics, 1974.
• J.P. May, A General Algebraic Approach to Steenrod Operations, Lecture Notes in Mathematics 168, Springer, 1970.
• D.C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, 2nd edition, AMS Chelsea Publishing, 2003.

+++ title = “References” section = “root” +++

References

Textbooks

• J.F. Adams, Stable Homotopy and Generalised Homology, Chicago Lectures in Mathematics, University of Chicago Press, 1974.

• J.P. May, A General Algebraic Approach to Steenrod Operations, Lecture Notes in Mathematics 168, Springer, 1970.

• D.C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, 2nd edition, AMS Chelsea Publishing, 2003. Available online: https://people.math.rochester.edu/faculty/doug/mu.html

Papers

• E. Belmont and H. Kong, An algebraic approach to the Adams spectral sequence. (E_r Massey products, Moss’ theorem: Definition 2.4, Definition 3.11, Theorem 3.13.)

• D. Chua, The $E_3$ page of the Adams spectral sequence, 2021. https://arxiv.org/abs/2105.07628 (Lemma 12.4: $\tau$-torsion survival and target forcing.)

• B. Gheorghe, G. Wang, and Z. Xu, The special fiber of the motivic deformation of the stable homotopy category is algebraic, Acta Math. 226 (2021), no. 2, 319–407. ($C\tau$ collapse theorem; $\operatorname{Ext}(C\tau) \cong$ Adams–Novikov $E_2$.)

• D.C. Isaksen, Stable stems, Mem. Amer. Math. Soc. 262 (2019), no. 1269. (Motivic Adams computations, CSV data for $E_2$ through $E_\infty$.)

• D.C. Isaksen, G. Wang, and Z. Xu, Stable homotopy groups of spheres, Proc. Natl. Acad. Sci. 117 (2020), no. 40, 24757–24763. (Motivic approach to classical computations.)

• W. Lin, G. Wang, and Z. Xu, On the Last Kervaire Invariant Problem, 2024. https://arxiv.org/abs/2412.10879 (Machine-proved Adams differentials and CW-spectrum data.)

• B. Johnson, Quantitative Bounds for Nilpotence and Vanishing Lines. (Lemma 6.3: vanishing line propagation through cofiber sequences.)

• D. Dugger and D.C. Isaksen, Motivic cell structures, Algebr. Geom. Topol. 5 (2005), 615–652.

Software

• H. Chatham, D. Chua, and J. Beauvais-Feisthauer, ext-rs — Rust library for computing Ext over the Steenrod algebra. htpy’s resolution engine, linear algebra, and Steenrod algebra crates descend from ext-rs. License: MIT OR Apache-2.0.

• W. Lin, SSeqCpp — C++ spectral sequence computation library using Groebner bases and SQLite databases. htpy-groebner is ported from SSeqCpp’s Buchberger algorithm implementation. License: Apache-2.0.

Data

• J. Beauvais-Feisthauer, H. Chatham, and D. Chua, The $E_2$ page of the 2-primary Adams spectral sequence in a large range, Zenodo, 2022. https://zenodo.org/records/7339848 License: CC BY 4.0. Used for verification benchmarks.

• W. Lin, G. Wang, and Z. Xu, Machine Proofs for Adams Differentials and Extension Problems among CW Spectra, Zenodo, 2024. https://zenodo.org/records/14475507