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