Witt Spectral Sequence
Definition
The Witt level spectral sequence is an algebraic machinery for deciding whether a CompleteType at Witt level W_n can be lifted to W_{n+1} without losing completeness. A WittLift record represents the candidate lift: it carries a liftBase (the W_n CompleteType), a liftTargetLevel (the target WittLevel), and a liftObstruction link.
Obstruction Theory
A LiftObstruction captures the algebraic obstruction to the lift. If obstructionTrivial is true the lift succeeds; otherwise it is localised to a single site coordinate (obstructionSite) and represented as a LiftObstructionClass — a cohomology class in H²(N(C(T)); ℤ/2ℤ).
Spectral Sequence Pages
The convergence of the obstruction computation is tracked page by page. Each SpectralSequencePage carries:
- pageIndex — the page index r (r=1 is the initial page).
- differentialIsZero — whether all differentials on this page vanish.
- convergedAt — the page index at which the sequence collapsed (only set on the final page).
Incremental Resolver
The IncrementalCompletenessResolver determines lift completeness without re-running the full ψ-pipeline from scratch. When the obstruction is non-trivial it returns a LiftRefinementSuggestion carrying liftSitePosition and obstructionClass.
Identity Algebra (WLS_ series)
| Identity | Statement |
|---|---|
| WLS_1 | WittLift T' is CompleteType iff spectral sequence collapses at E₂ |
| WLS_2 | LiftObstruction is localised to single site at position n+1 |
| WLS_3 | basisSize(T') = basisSize(T) + 1 for a closed constraint set |
| WLS_4 | Spectral sequence converges by E_{d+2} for depth-d configuration |
| WLS_5 | Every universally valid identity holds with lifted constraint set |
| WLS_6 | ψ-pipeline ChainComplex(T') restricts to ChainComplex(T) |