The computable form: task decomposition is a (dynamic) CSP

Parent: recursive-harness

The "possible worlds / collapse" picture, made formal and implementable: it is a (dynamic) Constraint Satisfaction Problem. Plain-language "jigsaw/sudoku" was the intuition; this is the machine.

Structure ⟨X, D, C⟩

• Variables X = {x₁,…,xₙ} — each xᵢ is a choice point / sub-task exposed by decomposition. X grows as you decompose → a dynamic CSP (variables added on the fly).
• Domains D — Dᵢ = candidate methods for xᵢ. Two cases:
  • finite: Dᵢ = {m₁,…,m_k} (enumerable);
  • infinite: not enumerated — a predicate φᵢ describing the allowed set ("string ∧ <60 chars ∧ professional"), or a generator that samples candidates.
• Constraints C — each c ∈ C is a relation over some variables fixing which method-combinations are compatible. A relation is inherently bidirectional (fixing xᵢ constrains xⱼ and vice versa) — that is the "mutual influence," no extra machinery.

A possible world = a complete assignment A: X→values satisfying all of C. The world-set = the CSP's solution set.

"Collapse" = constraint propagation (arc-consistency / AC-3): v∈Dᵢ is removed iff some constraint c(xᵢ,xⱼ) leaves it with no compatible support in Dⱼ; propagate to fixpoint. Removing one value kills every world that used it.

□/◇ as (cheaply) computable — with a caveat

• □P (forced) ≈ the variable's domain has collapsed to a singleton (|Dᵢ|=1);
• ◇P (open) ≈ domain still has >1 value.

Read off the domains in O(1). Caveat: this is only propagation-visible forced-ness — a sound approximation of true entailment, not the real thing. See deducible-not-known.

Revisited: the caveat is now priced, not just admitted. Propagation-visible □ is a certificate — sound, incomplete, cheap — i.e. exactly the certificate axis of relaxation; the gap to true entailment is what P×C budgets (deducible-not-known). And the read-off itself is a mechanical gate with α ≈ 0 (operationalizing-tolerances), while LLM-guessed entailments are semantic gates with measured α — the two tiers of trust are now explicit.

Convergence — a computable P×C stop

Not "unique solution." Define a spread of the remaining solution set (product of remaining domain sizes, or a stakes-weighted diameter). Stop when

$$\text{spread}(D)\times\text{cost}\le\theta_{P\times C}.$$

Residual differences between surviving worlds are below the stakes (pc-well-founded-recursion).

The algorithm (a CSP solver / wave-function-collapse)

solve(task):
    X, D, C ← decompose(task)          # LLM: emit variables / domains / constraints
    propagate(D, C)                     # AC-3: collapse incompatibles
    while spread(D) * cost > θ_PC:
        x ← argmin_{|D[x]|>1} |D[x]|     # fail-first / MRV: most-constrained var
        for v in candidates(D[x]):       # enumerate; if infinite, LLM samples
            assign x ← v
            propagate(D, C)              # cascading collapse
            if some domain emptied:      # dead end
                backtrack
            else if v exposes a sub-task:
                X,D,C ← (X,D,C) ∪ decompose(sub-task)   # recursion deepens
    return readoff(D)

Standard: backtracking search + AC-3 propagation + fail-first ordering + P×C as the termination/depth bound + decomposition-deepening recursion. Terminates: P×C decreases (well-founded) and propagation only removes values (monotone within a branch).

The LLM enters at exactly three interfaces

interface	what the LLM does	mechanical?
decompose(task)	emit X, D, C (which sub-tasks, methods, compatibility constraints)	tacit (taste/common sense here)
candidates(Dᵢ)	sample a few candidates from an infinite domain	tacit
eval c(vᵢ,vⱼ)	judge "are these two methods compatible?"	mechanical constraint → code (reliable propagation); semantic → LLM (fallible)

Everything else — propagation, search, backtracking, termination, reading □/◇ — is pure computation. The writable/tacit seam (tacit-spec-as-spec-compression) lands precisely on whether a constraint's evaluation is mechanical or LLM-judged.