The safe-recursion theorem (kernel shape)

Parent: recursive-harness

Why non-primitive recursion

Three families of recursion govern task delegation:

• primitive-recursion = structurally bounded loops: the loop body applies to a syntactically smaller object (list shrinks, tree descends), so termination is syntactically guaranteed. Safe, provably terminating — but provably too weak (Ackermann function cannot be expressed). Critical limitation for delegation: a giant task's depth is unknown in advance, so a manager restricted to primitive recursion cannot even express the plan.

• general-recursion (the μ-operator) = full Turing power. Every function computable-by-any-means is computable by recursion. Termination is undecidable (halting-problem). Nobody hands a giant task to one unbounded loop, however smart: you have no guarantee it finishes, no control over budget, no way to intervene.

• The third way = well-founded recursion: allow arbitrary non-structural recursion, but demand a termination measure (a quantity that must strictly decrease at each recursion step) that decreases into a well-founded order (no infinite descending chains). This is exactly how Lean accepts non-structural recursion (termination_by clause), and exactly what pc-well-founded-recursion does with P×C as the measure — failure-probability times failure-cost stops when acceptable, and the decomposition must lower P×C.

Setting

A task is a tree node. The executor has two fallible moves:

• SOLVE a leaf directly — inexact, error ≤ $\varepsilon_{\mathrm{exec}}$;

• DECOMPOSE into children plus a reassembly plan — itself fallible: with probability ≤ $\alpha_{\mathrm{split}}$ the split is wrong (children do not jointly entail the parent), and reassembly carries its own error $\varepsilon_{\mathrm{join}}$.

Each node's artifact passes a gate (gate-theory): sound up to false-accept rate $\alpha$, tolerance δ. The gate also checks that the measure decreased — each child's P×C is strictly below the parent's P×C.

Safe recursion (softened well-founded μ) — kernel shape

Theorem

Let the executor decompose a task recursively into a tree of sub-tasks and leaves. If (i) termination: at every decomposition the measure P×C strictly decreases into a well-founded order (verified at gates) — so the tree is finite and the recursion halts within the initial budget; (ii) local soundness: each gate's acceptance implies local correctness up to (δ, $\alpha$), false-accepts trimmed per gates-are-necessary-conditions; (iii) containment: every reassembly step is a contraction with factor k < 1 on the error metric — children's errors are damped, not amplified (inexact-contraction) — THEN the root artifact is within $\varepsilon/(1-k)$ of correct, with probability at least $1 - \sum \alpha$ (sum over all gates), within the initial P×C budget.

Summary: Termination + correctness + budget, all softened.

Proof

Sketch only — the hypotheses are design obligations, not yet formally verified for real harnesses.

Structural induction on the decomposition tree, which is finite by (i). Base case (leaves): by (ii), each leaf's artifact is correct up to its local tolerance $\varepsilon_{\mathrm{exec}}$ with high probability. Inductive case (internal nodes): assume all children's subtrees yield correct artifacts up to their respective bounds by the induction hypothesis. The reassembly step combines these corrected children; by (iii), the reassembled error obeys the inexact-contraction recurrence — errors from children are scaled down by k < 1, and the accumulated error across all depths converges to $\varepsilon/(1-k)$ (not to infinity). The union bound on gate false-accept rates $\alpha$ gives the probability bound: probability of any gate false-accepting scales as $\sum \alpha$, so correctness is high-probability. ∎

The control must control itself

Decomposition and delegation are not meta-moves above the theorem — they are fallible operations inside it, with their own $\varepsilon$, their own $\alpha$, their own gates. The plan is an artifact.

The distinctive failure when you forget this: one wrong split (a gate at the decomposition node accepting a faulty split), and an entire subtree perfectly solves the wrong problem. Every leaf gate green, every sub-artifact internally correct, the whole thing wrong. Only a reassembly gate that checks against the PARENT's spec (not the children's spec) catches it.

This does not regress into an infinite tower of controllers-of-controllers because of one asymmetry the whole harness leans on: verification is cheaper than generation. The same-level gate on a control output — a gate that verifies a split against the task it purports to break down — is affordable. It is not generating a plan; it is checking one.

So gates sit at every level of the control hierarchy, not just at execution leaves. Leaves are checked for correctness to spec; splits are checked for correctness as a decomposition; joins are checked for consistency with the parent; and the final root is checked against the original goal. Each gate catches the specific level's failure mode.

The Ashby echo. This is requisite variety, level by level: each level's failure modes are a different disturbance class (wrong leaf, wrong split, wrong join), and "only variety can destroy variety" demands a regulator matched to each — that is why per-level gates are structural, not decorative. The reassembly gate that checks against the parent's spec is the good-regulator-theorem in miniature: the gate embeds a model of the task (the spec) — you can't regulate what you can't model. And the no-regress asymmetry is Ashby's amplifier: a cheap, low-variety check regulating a high-variety generator is how regulation gets amplified up the hierarchy instead of regressing into a tower of controllers.

Proof obligations → lemmas

The theorem's hypotheses decompose into concrete lemmas you must establish for your harness:

Obligation	Proven in	What it means
(i) Termination: P×C strictly decreases toward a well-founded order	pc-well-founded-recursion	Each decomposition must lower the task's failure-probability–cost; the decomposition gate verifies this; no cycle possible
(ii) Local soundness: each gate's acceptance implies local correctness (δ, $\alpha$)	gates-are-necessary-conditions	A gate only passes what it can certify; false-accept rate $\alpha$ is intrinsic to the gate's verification; tolerance δ is the design choice
(iii) Error containment: reassembly is a contraction (factor k < 1)	inexact-contraction	Errors from sub-artifacts do not accumulate; each reassembly step scales them down; limit is $\varepsilon/(1-k)$
Budget & tolerance exchange	relaxation	How much $\varepsilon$ do you buy with a given P×C budget? How does tolerance δ price into the problem?
What can break	honest-caveats	The measure P×C is a proxy for true risk (Goodhart); the $\alpha$'s are correlated so $\sum \alpha$ is optimistic; contraction on text-state metrics is unproven in practice

Close

A giant task is safe to delegate not when the model is smart enough, but when the recursion is well-founded, every move — including the splits — is gated, and the reassembly contracts.