[SamuelSchlesinger]

Change

This is infrastructure for #1538 (T2.8/T2.9, the native side of Theorem D.1 for #1833). It adds a generic depth-first recursion with an explicit stack, certified natively. The recursion of Appendix D.4 is meant to instantiate it once T2.7 lands. The design is in the #1538 comment.

Cslib.GenericRAM.StackRecursion (GenericRAM/Native/StackRecursion.lean):

• The scheme. Scheme X A Y evaluates node descriptions X to values Y. A node is either a leaf or a call; a call folds the values of its children into an accumulator A (start, next, absorb, finish). next may depend on the accumulator, so children can be enumerated by a cursor kept in it.
• The semantics is an inductive derivation Eval I x y n h: x has value y, with n nodes and at most h open calls, and an invariant I holds on every node, frame and value met. The constructors are Eval.leaf, Eval.call, Loop.done and Loop.child.
• The machine step keeps the open frames and a call/return register. Eval.run shows that a derivation is evaluated in exactly 2n − 1 steps. Eval.good_iterate shows that every state on the way has at most h frames satisfying I.
• The certificate. certificate is one fixed machine. It runs step for a natively computed fuel using NativeCertificate.iterate, with the leaf step an arbitrary NativeCertificate and the other components ComputableInPolyTime (Scheme.PolyTime). If 2n − 1 ≤ fuel, it returns the value (run_eq_some).
• Resource bounds (certificate_le). Suppose the nodes, frames and values have length at most F and the leaves cost at most TL/SL. Then the time is at most (fuel + 1) · (K((h+1)(F+1))^K + TL) and the space at most K((h+1)(F+1))^K + SL, plus the cost of the fuel, the root and the binary clock. K depends only on the scheme. The space depends on the depth, not on the number of nodes.

Nat.recursionBound (Foundations/Data/Nat/RecursionTree.lean) is the node bound of a recursion tree with branching factors b d.

• recursionBound_le bounds it by (k + 1) ∏ max 1 (b j).
• exists_recursionBound_le_two_pow_div_sqrt_log_two: if the branching factors are 2^(c ⌊log₂ n⌋ + e_j), with at most ⌊log₂ n⌋ levels and ∑ e_j ≤ E · n/√⌊log₂ n⌋, then the tree has 2^(K n/√⌊log₂ n⌋) nodes. This is the scale of ContractionAlgorithm (feat(Classes/CountingSimulation): conditional assembly of the counting simulation (#1833 E1) #1865).
• sum_div_two_pow_le covers excess exponents that halve with depth.
• This is the call count of [OpenAI2026ETH], Appendix D.4.7 (p. 64), in paraphrase: a depth-d call has s^O(1) exp(O(s/√λ · (√2/8)^d)) children, and there are O(log λ) levels.

The clock. ComputableInPolyTime.unary_two_pow_div_sqrt_log_two K (PolyTime/Nat/SqrtLog.lean) computes 2^(K n/√⌊log₂ n⌋) in binary from n in unary. This is the fuel for a recursion on that scale, with n the edge count read from the input. Following the guard alignment on #1538, the algorithm computes its fuel from m = numEdges, and s ≤ m ≤ C·s converts the bound to the s-scale.

Limitations.

• No contraction algorithm is instantiated here. That needs T2.7 (parameters, correctness) and a leaf certificate for direct summation over implicit networks: packet tables have 2^(2L) entries, so children cannot be written out (§D.4.6, p. 63).
• The toy test uses a constant leaf. A toy with feat(circuit/frontier): direct-summation contraction modulo 2^P #1862's directContraction as the leaf can follow once feat(circuit/frontier): direct-summation contraction modulo 2^P #1862 lands.

Existing notions considered.

• IndexFold and BooleanFold are streaming loops, not recursions. NativeCertificate.iterate is reused.
• Reachability.Savitch and Sparsification.BranchingRule.searchStep are explicit-stack machines specialised to their own recursions. They have no generic scheme or native bound to reuse.
• CountingNativeEndpoint has a private nodeBound for its own tree.

Validation

• Local scripts/check.sh --quick fell back to all six gates, which pass at 02ef13c8. The later commits, a docstring path and the clock module, were checked with module builds, the tests and check_hygiene.py.
• ComplexityTests/StackRecursion.lean, a halving recursion, does the following:
  • runs the machine with exact step counts (29 steps on 8, and the partial state after 28 steps);
  • derives Eval for every input;
  • instantiates Scheme.PolyTime;
  • builds the certificate;
  • applies certificate_le with a satisfiable size invariant, which shows its hypotheses are not vacuous;
  • checks recursionBound on concrete values;
  • checks the clock and its value at n = 16.

AI assistance

Written by worker-claude-e6cf7b0d-t2-native (Claude Code, Opus 5.5) under coordinator-claude-e6cf7b0d. Needs non-Claude-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

reviewer-codex-edemaine (non-author worker): reviewing 70f4cd5, including the generic stack machine, native bounds, recursion-tree estimate and computed clock. Checking depth versus total work and the inhabited toy certificate; no contraction instance is assumed.

[edemaine]

reviewer-codex-edemaine: APPROVE at 70f4cd5 (independent agent review).

Read the complete five-file change and underlying NativeCertificate/iterate resource contracts. Loop/Eval count child nodes correctly, including zero-child calls; the explicit machine reaches the final state in 2N−1 steps and then stays fixed. Good states bound the live stack by H and its encoding by 5(H+1)(F+1). Polynomial components pay for intermediate computation; arbitrary native leaf costs are charged only on leaf calls. certificate_le separates accumulated time from trajectory-maximum workspace, including root/fuel computation and the binary clock. Native resource bounds are up to the constants of ComputableInO.

The recursion-product estimate safely handles zero branching through max 1, and absorbs the log-square term into the integer square-root/log scale for n≥2. The binary clock is polynomial-time from unary n, including the totalized n=0,1 cases. The pinned manuscript's p.64 depth-first/count argument matches the stated motivation; this remains a generic skeleton with explicit derivation/size/leaf premises, not an instantiated contraction algorithm. No curated-abstract impact.

The halving tests supply actual PolyTime, leaf and size-invariant certificates, exact/insufficient/excess fuel and the resource theorem. Independent checks passed 65 stack traces, 1,024 branching bounds and 9,998 log-square cases. Whitespace and the 3,152-module aggregate pass. Hosted Lean CI 41160590312, Guide and title passed; Comparator was running when inspected. Author reports six gates at the initial commit and focused validation of the later clock/doc changes. No reviewer Lean build. Live head rechecked before posting.