Incremental Completeness Guide

The IncrementalCompletenessResolver determines whether a CompleteType at Witt level W_n lifts to W_{n+1} without re-running the full psi-pipeline from scratch.

When to Use This Resolver

Use IncrementalCompletenessResolver instead of the full CompletenessResolver when:

You already have a certified CompleteType at W_n.
You want to promote it to W_{n+1} (the next Witt level).
Re-running the full psi-pipeline would be prohibitively expensive.

Identity WLS_4 guarantees the spectral sequence converges by page E_{d+2} where d is the constraint depth, making the incremental approach tractable.

Step 1 — Declare a WittLift

@prefix type:     <https://uor.foundation/type/> .
@prefix schema:   <https://uor.foundation/schema/> .
@prefix owl:      <http://www.w3.org/2002/07/owl#> .

type:my_lift a owl:NamedIndividual, type:WittLift ;
    type:liftBase         type:my_w8_complete_type ;
    type:liftTargetLevel  schema:W16 .

Step 2 — Run the IncrementalCompletenessResolver

@prefix resolver: <https://uor.foundation/resolver/> .

resolver:my_icr a owl:NamedIndividual, resolver:IncrementalCompletenessResolver ;
    resolver:liftTarget  type:my_lift .

The resolver computes the SpectralSequencePage sequence. When differentialIsZero becomes true at page r, the sequence has converged (QLS_4) and convergedAt is set to r.

Step 3 — Inspect the LiftObstruction

The lift carries a LiftObstruction:

If obstructionTrivial is true: the lift is complete — identity WLS_1 applies.
If false: the obstruction is a non-zero cohomology class localised to site position n+1 (WLS_2). The resolver returns a LiftRefinementSuggestion with:
- liftSitePosition — the site to target.
- obstructionClass — the LiftObstructionClass to kill.

Step 4 — Handle a Non-Trivial Obstruction

A non-trivial obstruction means the type is a TwistedType. Per identity MN_7, TwistedType implies a non-zero class in H²(N(C(T')); Z/2Z). Add the suggested constraint from liftSitePosition, re-run the synthesis step, and retry the lift. Identity WLS_3 guarantees basisSize(T') = basisSize(T) + 1 after a successful resolution.