Iterative Resolution

Definition

Iterative resolution extends the resolution process into a learning loop. Rather than computing a partition in a single pass, the resolver proceeds iteratively: each iteration applies a constraint, pins sites, and checks whether the budget is closed. The process converges when all sites are pinned.

Resolution State

A ResolutionState tracks the progress of an iterative resolution:

PropertyRangeDescription
isCompletexsd:booleanTrue when all sites are pinned
iterationCountxsd:nonNegativeIntegerIterations performed so far
siteDeficitFreeRankRemaining unpinned sites
convergenceRatexsd:decimalSites pinned per iteration

A Resolver links to its state via resolutionState.

Refinement Suggestions

When the resolution is incomplete, the resolver produces RefinementSuggestion objects that guide the next iteration:

PropertyRangeDescription
suggestedAxisMetricAxisWhich metric axis to explore
suggestedClassowl:ClassWhich constraint class to apply
targetSitesSiteIndexWhich sites to target

Suggestions are linked from the state via suggestion.

Refinement Steps

Each iteration produces a RefinementStep that records the type-level change:

PropertyRangeDescription
previousTypeTypeDefinitionType before this step
appliedConstraintConstraintConstraint applied
refinedTypeTypeDefinitionType after this step
sitesClosedxsd:nonNegativeIntegerSites pinned in this step

RefinementStep is a subclass of DerivationStep, parallel to RewriteStep for term-level rewriting.

Convergence

The resolution loop terminates when:

  1. isComplete is true
  2. isClosed is true on the free rank budget
  3. siteDeficit shows zero free sites

The convergenceRate tracks the rate of progress, enabling early detection of stalled resolutions.

Example: Three-Iteration Resolution

Iteration 0: 0/8 sites pinned  (convergenceRate = 0.0)
Iteration 1: apply ResidueConstraint → 3/8 pinned (rate = 3.0)
Iteration 2: apply CarryConstraint   → 6/8 pinned (rate = 3.0)
Iteration 3: apply DepthConstraint   → 8/8 pinned (rate = 2.67, complete)

When resolution stalls (convergence rate drops to zero), the CechNerve provides topological diagnostics via the ψ-Pipeline — Betti numbers reveal whether the stall is due to cyclic constraint dependencies or insufficient constraint coverage.