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