Experiment: certified E[T] bounds from one prompt

The prompt

Consider the following Markov chain on ℕ³ (natural numbers, so decrements saturate at zero). Start at (1,1,1). At each step: choose one of the three coordinates uniformly at random; with probability 1/4 increment that coordinate by 1; with probability 3/4 decrement it by 1, where decrementing 0 leaves it at 0. The chain absorbs at the origin (0,0,0). Let T be the number of steps until absorption.

Give me upper and lower bounds on E[T], as tight as you can make them, each with a complete Lean 4 proof that compiles.

Note the saturating decrement at zero is essential to the problem — a coordinate at 0 that is selected and "decremented" stays at 0. Please state explicitly the theorem you are proving and confirm it is about this chain.

Report the width of your bracket. A sound but loose bound is a weaker result than a tight one. Treat this as a serious challenge, orchestrate to find the best solution possible.

The result (Claude Code, August 2026)

RWBound/Main.lean proves, for the chain of the prompt,

18351933175568 / 2⁴⁰  ≤  E[T]  ≤  18351933242915 / 2⁴⁰

a bracket of width 67347/2⁴⁰ < 6.13·10⁻⁸ (expected_absorption_time_bounds). Both bounds are Foster-Lyapunov certificates: integer super- and subsolution tables on the box {0..20}³ (the upper one extended by one ring layer), scaled by 2⁴⁰. decide +kernel checks the in-box inequalities; outside the box the upper certificate continues as a closed-form supersolution and the lower one as a constant. E[T] is the tail sum Σₙ P(T > n) (ET in the sources). PathSpace.lean constructs the trajectory measure of the absorbed chain with Mathlib's Ionescu-Tulcea theorem (ProbabilityTheory.Kernel.traj) and proves ∫⁻ ω, T ω ∂pathMeasure = ET, so the bracket also holds for the path-space expectation of the first hitting time (expected_absorption_time_bounds_pathspace). RWBound/README.md describes the proof file by file. Nothing is proved here about other chains, or about continuous state spaces.

To rebuild and audit:

cd RWBound && lake exe cache get && lake build
cat > audit.lean <<'EOF'
import RWBound.Main
#print axioms RW.expected_absorption_time_bounds
#print axioms RW.expected_absorption_time_bounds_decimal
#print axioms RW.expected_absorption_time_finite
#print axioms RW.expected_absorption_time_bounds_pathspace
#print axioms RW.lintegral_T_eq_ET
EOF
lake env lean audit.lean

The Mathlib pin is in lake-manifest.json (4d6f9893…); lakefile.toml tracks master, so do not run lake update. On a fresh checkout the build passes, and the audit gives [propext, Classical.choice, Quot.sound] for the four theorems of Main.lean and for lintegral_T_eq_ET; no sorry, no native_decide.

Notes for readers

RWBound/, numerics/ and session-report.md are the unedited output of the run described in Details below.

• S3 in the Lean development abbreviates the state space ℕ × ℕ × ℕ (Defs.lean); it is not the symmetric group and not the 3-sphere. Within the RW namespace, dist is the n-step distribution of the absorbed chain, flip is the 1/4-vs-3/4 coin, and Path is the type ℕ → S3; none has its usual Mathlib meaning.
• Five module headers begin "Contract (statements are FIXED; do not change them, only replace the sorrys)": the orchestrating session's instructions to its subagents, left in place. No sorry survives. Where BoxChecks.lean says the inequalities were "verified in exact integer arithmetic externally", the decide +kernel theorems beneath that comment re-prove them in Lean's kernel.
• session-report.md and RWBound/README.md print the upper endpoint as "16.690986051721666…". The exact endpoint is 16.690986051721665717…; the printed string is the shortest round-trip decimal of its float64 value, so the last digit is rounded up where the ellipsis suggests the expansion continues. Both displayed inequalities remain true, and the decimal corollary in Main.lean rounds outward (16.6909859904 ≤ E[T] ≤ 16.6909860518).
• session-report.md is the closing message of the orchestrating session; its "previous summary" and "optional strengthening" refer to earlier turns of the same session. Its machine paths, and RWBound/check-remote.sh, refer to the session's build machines and do not run elsewhere.

How the tables were found

The session solved the expected-hitting-time system numerically, then repaired and verified the inequalities in exact integer arithmetic before emitting Lean source; Lean re-checks them in its kernel, so nothing in numerics/ is in the trust base. The numerics scratch files are in numerics/; the session's build scripts and logs are not included.

Origin of the question and related work

The chain is the "3-D asymmetric random walk" from the benchmark suite of Diabolo (Zaiser, Murawski and Ong, Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops, POPL 2025; tool). MAITRIA's technical report Certificates, not printouts: exact-rational bounds for probabilistic programs (davidad's AI ensemble, 3 August 2026) ran nine cases from the suites of Diabolo and of GuBPI (Beutner, Ong and Zaiser, PLDI 2022) through an exact-rational certificate pipeline, with this chain as its case 8. This experiment was run the following day.

The model used methods and results from the literature, e.g. supermartingale certificates for the upper bound (Foster 1953; Chakarov and Sankaranarayanan, CAV 2013; Kaminski, Katoen, Matheja and Olmedo, JACM 2018), bounded subinvariants for the lower bound (Hark, Kaminski, Giesl and Katoen, POPL 2020), and Mathlib's probability and measure theory, including Étienne Marion's 2025 formalization of the Ionescu-Tulcea theorem.

Details

The run: one prompt to Claude Code on 4 August 2026; the model finished about 75 minutes later. Everything in RWBound/ and numerics/, together with session-report.md, is its output, unedited. The orchestrating session (model claude-fable-5) wrote the definitions, the theorem statements, the numerics and both READMEs; five subagent sessions it spawned (model claude-opus-5) filled in the proofs: four against fixed statements in the contract-headed files, one building the path-space certification (PathSpace.lean). I wrote the prompt. The only other human message, half an hour in, interrupting a tool call: "you can use the dgx spark to run lean etc if we're short on disk space here". This was the only run; I discarded no earlier attempt.