recursive-harness

Parent: engineering

How to safely get non-primitive (unbounded-depth) recursion in an agent harness, even though today's models can't converge under unrestricted general recursion.

The background (theory floor)

• recursion compounds value, but only if it converges → recursion-convergence-contraction
• general (non-primitive) recursion is a phase transition (Turing/Gödel) — and you can't take it because models can't guarantee convergence → recursion-is-a-phase-transition
• convergence needs an observable / identifiable target, not just a capable model → convergence-needs-an-observable-target

The construction (this subtree)

Thread the needle with well-founded recursion + per-level gating:

1. pc-well-founded-recursion — recurse on a measure that strictly decreases (P×C); leaves = any sub-task whose P×C is acceptable. Guarantees termination and convergence with one measure.

   • safe-recursion-theorem — the kernel shape: well-founded measure + gated moves (including the splits) + contracting reassembly ⟹ termination, correctness up to ε/(1−k), within budget.

   • operationalizing-tolerances — what ε, α, k are on the ground: acceptance-check bundles, mutation-tested false-accept rates, residual ratios, budget counters; understandability as the knob behind the knobs.

   • root-protocol — what the top actually issues: a self-reproducing constitution (SOLVE-or-SPLIT, four-part splits, pass C down, declare your heading, fail loudly); your whole leverage is S_root + C.

   • coupling-to-the-learner — the neural properties that are load-bearing: ε is a competence landscape (decomposition = projection onto it), k = feedback legibility (checks emit gradients), leaves must be PAC-learnable from their injection.

   • giant-tasks-nonprimitive — why depth-unknown tasks force μ-recursion, and why a capable agent still can't break the wall: diagonalization ignores cleverness; the game is construct-∃ (certify), not decide-∀; total ≠ r.e. so the constitution is forever incomplete; the only escape hatch is interactive extension (Turing's ordinal logics).

   • coordinator-not-arbiter — who handles failure: a mechanical kernel (global no-goods + provenance graph + ledgers + backjump computation, the DPLL(T) SAT-core isotope), never a standing LLM arbiter; semantic diagnosis is just one more gated move.

   • weak-auditor-by-design — why the auditor watching a strong actor should be weaker than the actor (Anthropic's hook auditor as the production precedent): hot-path economics, narrowed tasks, tripwire-not-wall, intelligence-as-attack-surface, decorrelation, calibrated suspicion; an auditor's strength comes from its position, not its IQ.

   • split-granularity-equilibrium — the granularity dilemma: split risk rises, leaf risk falls → a U-curve (bias–variance in P×C currency); and the techniques that move the curve — local grain, probe-then-split (conflict-driven decomposition), cut along Simon seams (certificate length = cut quality).

   • upward-reequilibration — when even the equilibrium is bad: the node emits an infeasibility certificate and the ancestor re-equilibrates — Benders feasibility cuts (hard, reshape the tree; no-goods ≡ combinatorial Benders cuts) + shadow prices (soft, rebalance α/B across siblings); monotone cuts + depleting ledgers = no oscillation.

   • grounding-in-logprobs — the Greek letters get real numbers: semantic entropy → α̂ pre-gates, gate-history-calibrated confidence → the α ledger, token-entropy profile → a ◇/□ readout (verify the high-entropy spans), perplexity → the ε-terrain probe. The metric proposes, the gate disposes.

Softened-logic imports (each a hard result, softened, with a harness payoff)

• blame-calculus — gradual typing: soft/hard crossings are casts = gates; "well-typed can't be blamed" ⟹ subtrees behind mechanical gates are provably not the culprit (up to α).
• spot-checkable-artifacts — the PCP move: demand error-amplifying artifact formats (assertions/types/checksums woven through) so cheap random spot-checks get global reach.
• paraconsistent-isolation — ex falso is fatal for an LLM-fed belief store; quarantine contradictions by provenance cone; isolation (control #5) gets its logical identity.
• soft-identity-transfer — equality → distance (bisimulation metrics): no-goods/subsumptions/prices transfer to ε-similar contexts with confidence decay; retrieval before generation; the metric proposes, the gate disposes.
• interface-p-belief — two generals: exact common knowledge is unattainable; common p-belief suffices (Monderer–Samet) — why written, both-ends-gated interface contracts work and negotiation doesn't.

2. decompose-and-reassemble — middle agents split a task into near-decomposable sub-tasks and recombine; the reassembly join is where a gate must live.
3. tacit-spec-as-spec-compression — the LLM supplies the unwritable part of the spec; recursion compresses the infinite case-space into a finite rule, concentrating tacit risk at dispatch (dangerous) and leaves (P×C-bounded, safe).
4. world-choice-and-consistency-gate — you don't need deterministic taste; a taste choice selects a possible world, convergence is per-world, and the gate becomes consistency-with-the-chosen-world (checkable) instead of match-the-truth (not).
5. drift-is-world-wandering — diagnosis: today's drift = wandering between incompatible worlds (no pinned world / no consistency gate / no provenance). The fix is the same machinery above.
6. csp-formalization — the computable form: a dynamic CSP (variables/domains/constraints), collapse = arc-consistency, convergence = spread×cost ≤ θ_PC, with a runnable solver algorithm; the LLM enters at 3 interfaces.
7. deducible-not-known — the third ceiling: constraints entail the answer but deriving it is NP-hard; □/◇ is only propagation-visible; P×C doubles as a deduction-search budget; the LLM is the heuristic for the intractable deduction.
8. conflict-learning-and-backjumping — CDCL: dead end → backjump to the real culprit (maybe another sub-tree) + learn a no-good. The assignment is non-monotone but learned collapse-info is monotone → that's what guarantees convergence (and it's the lazy answer to deducible≠known + the provenance against drift).
9. llm-as-fallible-theory-solver — the harness is DPLL(T) with the LLM as a fallible theory solver; therefore the LLM must explain its incompatibility verdicts (emit a small conflict), or there's no short no-good, no backjump, no convergence.
10. non-determinism-and-infinite-branching — but the agent is non-deterministic (no-goods can be false → soften to weighted/revisable beliefs) and infinitely-branching (sample, don't enumerate → MCTS, not DFS/BFS; no completeness, only P×C satisficing). The home shifts from CDCL to LLM-as-policy+value MCTS + soft constraints.
11. stages-gates-bound-the-search — the weld: stages-and-gates is the scaffold that makes the unsound/infinite MCTS converge — a gate is a soft→hard verifying collapse that re-grounds the search and stops unsound error from compounding across stages. Put gates at mechanically-verifiable seams. (Also: maps to 6 of the eight controls.)
12. modal-status-labels — why Kripke earns its place: not as logic, but as a labeling scheme (□ definite / ◇ possible / conditional + confidence). The agent's tracing is far harder than SAT's (richer, unsound modal landscape), so each fact's modal status must be explicit to backtrack correctly; accessibility = the dependency graph that says where to backjump.

One line

A safe non-primitive recursive harness = P×C-well-founded recursion (termination + convergence) × decompose/reassemble along weak seams × per-node world-commitment + consistency gate (correctness without determinism) × human as world-acceptor. The model supplies the unwritable spec; structure + P×C + consistency keep it converging.