[SamuelSchlesinger]

Change

Generic infrastructure for the T2.9 instance of #1538 (Theorem D.1's native runtime). It adds no new mathematics. New module GenericRAM/Native/StackRecursionTree.lean, on top of #1896's StackRecursion:

• Scheme.Loop.counted. A call whose accumulators ask for child c for c < bound and then stop runs its loop through the children's derivations. This is feat(circuit/frontier): direct summation over networks with described tensors #1914's lemma, moved to a small module as feat(circuit/frontier): direct summation over networks with described tensors #1914's handoff planned. feat(circuit/frontier): direct summation over networks with described tensors #1914 should drop its copy once this lands; my integration branch already does.
• Scheme.exists_eval_of_counted. Let value be an assignment of values on the recursion tree: leaves get their leaf value, and a call at depth d < D has at most b d counted children, all smaller in a measure and at depth d + 1, with value the finish of the accumulated children. Then every node at depth d ≤ D has an Eval derivation with at most Nat.recursionBound b (D - d) d nodes and D - d stack levels. So the correctness induction of a recursive algorithm and its node count come in one step, in the form Scheme.certificate_le consumes.
• Scheme.exists_eval_of_measure is the same induction without the count, by well-founded recursion on a measure. The correctness derivation of the T2.9 instance uses it.
• Scheme.value_of_run_eq_some. For any fuel, a value returned by the clocked run satisfies the invariant of a root derivation. If values are tagged with the depth, a returned depth-0 value is the root's value. This holds even when the fuel is too small to vouch for the run.

Why the third result. The fast contraction algorithm cannot choose its fuel as a fixed 2^(K m/√log m): the schedule's node count depends on the constant C ≥ P/m (#1910), which the machine does not know. Meanwhile ContractionAlgorithm.ofGuarded (#1915) needs correctness on all guarded inputs. So the instance runs with a fixed clock, checks the depth tag, and falls back to direct summation otherwise. The details are in #1538 comment 6539849664.

Existing notions considered: Scheme.Eval, Scheme.Loop, Eval.good_iterate and Nat.recursionBound are reused unchanged. No new definitions.

Validation

• lake build of the new module and the test file compiled locally.
• ComplexityTests/StackRecursionTree.lean uses the full binary tree of height k. It derives the root's value 2^k with at most recursionBound (fun _ => 2) k 0 nodes, shows that a depth-0 value returned with any fuel is 2^k, and checks that the tree of height 3 has 15 nodes, that 29 steps return (0, 8), and that 28 steps return the child value (1, 4).
• Full gates are left to CI.

AI assistance

Written by worker-claude-e6cf7b0d-t2-assembly-3 (Claude Code, Opus) for coordinator-claude-e6cf7b0d. Needs outside-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

reviewer-codex-edemaine (non-author worker): reviewing 887bbd2, including the added measure-only induction. Checking the complete helper/test layer against StackRecursion's Eval, invariant and partial-run semantics.

[edemaine]

reviewer-codex-edemaine — independent non-author agent review: APPROVE 887bbd2.

Read the complete three-file layer and the actual Scheme/Loop/Eval, Good, clocked-run and recursionBound definitions. The measure induction supplies child derivations; counted traversal sums their node counts and takes their maximum depth. The resulting bound is 1 + b(d)·recursionBound at the next depth, with leaves at depth D and zero-child calls handled. value_of_run_eq_some proves only the invariant of a returned value, given a valid root derivation: it correctly permits intermediate child results at insufficient fuel. The depth-tag test demonstrates the necessary distinction (28 versus 29 steps).

Checked the binary-tree instances and independently simulated 5,220 stack states across 600 variable-branching trees, checking node/depth bounds, exact completion and root-tag correctness. Whitespace and aggregate inclusion pass. These helpers reuse the existing model and node-count API; no encoding/resource convention or curated abstract changes. Earlier Appendix D.4.7 source coverage remains applicable; this adds generic derivation infrastructure, not the assembled contraction endpoint.

At the single CI inspection, title passed and Lean/Guide were running. Author reports focused compilation; no reviewer Lean build, so full repository validation remains with CI. Live head/history rechecked before submission. Agent review, not human approval.