+++ 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:
- Apply all deduction passes iteratively until convergence.
- Display a summary report showing how many differentials were derived by each pass.
- 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:
| Counter | Meaning |
|---|---|
| Degree zeros | $d_r = 0$ because target group has dim 0 |
| Weight degree zeros | $d_r = 0$ because source/target weights disjoint |
| $\tau$-torsion zeros | $d_r = 0$ from torsion obstruction |
| $\tau$-survival zeros | $d_r = 0$ from Chua Lemma 12.4 |
| $\tau$-target nonzeros | $d_{k+1}$ forced by torsion order $k$ |
| Leibniz zeros | $d_r(hx) = 0$ from Leibniz rule |
| Leibniz nonzeros | $d_r(hx) = hy$ from Leibniz rule |
| Vanishing line zeros | $d_r = 0$ from vanishing line |
| Permanent cycles | Classes surviving to $E_\infty$ |
| Naturality zeros/nonzeros | Transferred from parent via $i^*$ |
| Reverse naturality zeros/nonzeros | Derived from parent via injectivity |
| LES subcomplex zeros | $d_r = 0$ from kernel/image sub-SS |
| Moss zeros/nonzeros | From Massey product structure |
| Moss reverse | Solved from known Massey + partial factor data |
| Iterations | Number of fixed-point loop iterations |
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:
- Computes the inclusion map $i^* : \operatorname{Ext}(C) \to \operatorname{Ext}(M)$
- Computes the projection map $\pi^* : \operatorname{Ext}(C/M) \to \operatorname{Ext}(C)$
- Propagates vanishing lines through the LES
- 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.