pc-well-founded-recursion

Parent: recursive-harness

The recursion's well-foundedness is defined by P×C (HTA's failure-probability × failure-cost stopping rule, prior-art-task-decomposition) — not by an abstract syntactic size.

The measure

  • Descending relation = "is a sub-task of, and has lower P×C."
  • Minimal elements (leaves) = any sub-task with P×C ≤ threshold (the halting condition).
  • Termination is guaranteed: each decomposition strictly lowers P×C toward the threshold; an acceptable-P×C node is a leaf — you just do it.

Why P×C and not syntactic size: in tasks, "smaller" means "less can go wrong / cheaper to be wrong" = lower P×C. HTA decomposes to lower P×C and stops when it's acceptable. So P×C is the natural well-founded measure for tasks (contrast: structural recursion uses syntactic size with a fixed base case like empty-list).

Leaves are dynamic, and any acceptable sub-task is a first-class atom

  • The base case is not a fixed syntactic class — it's set by P×C. The same sub-task is a leaf in a low-stakes context (P×C already acceptable → just do it) but gets decomposed in a high-stakes one. → depth auto-adapts to stakes: deep where risk is high, shallow where low.
  • Any P×C-bounded chunk is a reusable, standalone unit — it can head its own tree or sit as a leaf elsewhere. Gives compositionality.

One measure does termination and convergence

P×C decreasing down the tree is the contraction measure. Convergence = reaching P×C-acceptable atoms. So termination (well-foundedness) and convergence (contraction toward a fixed point, recursion-convergence-contraction) are governed by the same quantity — not two separate concerns. Fixed points = the P×C-acceptable leaves.

Revisited — under the theory layer

This note is now the termination hypothesis (i) of safe-recursion-theorem — the well-founded measure, checked mechanically at every split gate (root-protocol clause 2d). Two sharpenings since: P×C is measured relative to the model's competence landscape (coupling-to-the-learner — "small" means familiar, not short), and when no split can lower it below a node's allowance, that's not a dead end but an infeasibility certificate flowing up (upward-reequilibration).

Subtlety: reassembly carries its own P×C

P×C of the whole ≠ sum of the parts: reassembly adds a join-failure P×C. So decompose-nodes lower P×C (well-foundedness holds on the way down), but the reassembly nodes are where residual P×C concentrates. If a join's P×C is still high, that reassembly must itself be decomposed + gated — the gate goes exactly where reassembly P×C isn't yet acceptable (see decompose-and-reassemble).