Repository navigation
test(GenericRAM/Native): stack recursion with direct-contraction leaves - #1903
Draft
SamuelSchlesinger wants to merge 6 commits into
Draft
SamuelSchlesinger wants to merge 6 commits into
SamuelSchlesinger wants to merge 6 commits into
Conversation
A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…n docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…mial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
A chain of identity calls ending in #1862's direct summation: one fixed machine computes d.contraction % 2^P with linear fuel, and the resource theorem charges the exponential leaf only at the leaf. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Collaborator
Author
|
|
Collaborator
Author
|
|
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Change
This PR is a test only, and it is stacked on #1896. Until #1896 lands, the diff also shows #1896's files, so review only
ComplexityTests/StackRecursionDirect.lean. After #1896 merges I will mergemainback in.This is the toy recursion asked for under #1538 (T2.9-prep). It instantiates
StackRecursion.Schemewith #1862'sdirectContractionCertificateas the leaf step. A node(k, (P, r, d))is a chain ofkcalls, each with one child and the identity as combination step, and the chain ends in a leaf that contractsdmodulo2^P.eval_chain: every chain has a derivation withk + 1nodes andklevels.run_chain: with fuel2k + 1, the run returnssome (d.contraction % 2^P)on every input.chain_polyTimeandchainCertificate: the components are polynomial-time, so one fixed machine computes the contraction.chainCertificate_le:certificate_leapplied with a size invariant. The time is2k + 2rounds, each a polynomial in(k + 1)(3n + 2)plus the leaf'sL(n+1)^L 2^m. The space is polynomial. This shows that a non-polynomial leaf is charged only through the leaf bounds.Validation
Local
scripts/check.sh --quickfell back to all six gates, which pass on this branch (#1896 withmainmerged in, plus the test).check_hygiene.pypasses.AI assistance
Written by
worker-claude-e6cf7b0d-t2-native(Claude Code, Opus 5.5) undercoordinator-claude-e6cf7b0d. Needs non-Claude-fleet review of the test file.🤖 Generated with Claude Code
https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG