feat(proofs): transport charged execution clocks

[windsornguyen]

What does this change?

Proves that a typed two-stack execution with allowance t is exactly reproduced by the charged interpreter with allowance transitionCharge(P) * t, where transitionCharge(P) = |encode(P)| + 1.

The equality is established first for arbitrary runtime configurations, then lifted to initialized execution and finally to ComputesWithin. For each fixed translator program, the overhead multiplier is independent of the input.

This transports clock certificates through the executable charge specification. It still does not claim that a bit-level interpreter realizes one charged transition in constant time; that is the next refinement boundary.

How was it tested?

• lake env lean ComplexityTheory/ProofComplexity/TwoStackChargedSimulation.lean
• lake build --wfail passes
• lake lint passes
• git diff --check passes
• No sorry or new axioms

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3877ae2d3f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Describe the product as an allowance, not an exact step count

When the initial state is halted, or execution halts before using all t typed steps, runFrom returns immediately, so fewer than transitionCharge P * t charged transitions execute. The theorem proves equality of returned results under the multiplied allowance, not exact transition consumption; describe this as an upper bound or as the cost per running source transition to avoid overstating the formal result.

AGENTS.md reference: AGENTS.md:L18-L22

Useful? React with 👍 / 👎.