MarkovProcess consumer pilot

A small Lean 4 project that uses Scott Armstrong's MarkovProcess library to prove optional stopping for Brownian motion at a truncated exit time.

The result · Quick start · Proof outline · Reproducing and evidence · Citing · LLM index

Note

Credit: almost all of this is Scott Armstrong's work. This pilot is a thin consumer of Armstrong's MarkovProcess (Apache-2.0), which did the heavy lifting. If you use the pilot, please cite MarkovProcess.

MarkovProcess supplies: the canonical Brownian motion (MarkovProcess.brownianMotion) and its uniqueness; exit times and their truncations as stopping times; the heat generator ½ d² and its domain; Feller and Kolmogorov regularity of the heat semigroup; continuous-time optional stopping; and Dynkin's formula at a bounded stopping time, the expensive part.

The pilot adds (about 250 lines): a two-way bridge to Mathlib's IsBrownianReal, a smooth test function equal to the identity near [a, b], two pathwise facts about the exit time, and the final assembly. One helper lemma (mem_of_lt_exitTimeTrunc) is adapted from MarkovProcess, with Armstrong's copyright notice and a statement of the changes. It is a pilot, not a general library, and not a new theorem.

The result

Headline theorem. Brownian motion started at x ∈ (a, b) and stopped at its exit time from (a, b), truncated at any deterministic horizon K, has mean x:

theorem MarkovProcessPilot.integral_eval_exitTimeTrunc_Ioo
    (a b x : ℝ) (hax : a < x) (hxb : x < b) (K : ℝ≥0) :
    ∫ ω, ω (MarkovProcess.ContinuousPath.exitTimeTrunc (Set.Ioo a b) K ω)
      ∂(MarkovProcess.brownianMotion x) = x

Bridge to Mathlib. MarkovProcessPilot.isBrownianReal_iff shows that MarkovProcess.IsBrownianReal X P ↔ ProbabilityTheory.IsBrownianReal X P for every process X and measure P, so the library's Brownian motion is a Brownian motion in Mathlib's sense once recentred at its starting point (isBrownianReal_brownianMotion), and Mathlib's Brownian API applies to it.

Mathlib-only statement check. lake comparator confirms that the theorem exit_mean in Audit/Exit/Challenge.lean, stated in Mathlib's vocabulary only (any law on C(ℝ≥0, ℝ) that is Brownian started at x, with Mathlib's hittingBtwn as the stopping time), is exactly what Audit/Exit/Solution.lean proves. The bridge is judged by exists_unique_brownian_kernel in Audit/BrownianKernel/Challenge.lean: exactly one Markov kernel from ℝ to C(ℝ≥0, ℝ) has a recentred coordinate process that is IsBrownianReal at every starting point. A Mathlib-only statement cannot name the library's kernel, so the Solution proves this with MarkovProcess.brownianMotion as the witness. claims.yaml names the Challenge theorem that judges each claim (judged_as).

Important

Scope. The exit time is truncated at K. Untruncated exit times, and the exit probability P_x(exit at b) = (x - a)/(b - a), are out of scope and not claimed. The mathematics is classical; what this repository contributes is a machine-checked consumer of MarkovProcess, not a new theorem.

Check	Status
Build	lake build green at Lean v4.35.0-rc2, Mathlib 065356127b1d
Placeholders	no sorry, admit, custom axiom or native_decide in MarkovProcessPilot/
Axioms	propext, Classical.choice, Quot.sound only (logs/axioms.txt)
Comparator	pass, toolchain mechanism; con-ron, NanoDa and Lean kernels
Receipts	.lean-receipts/, bound to commit 1548828e63c8
Index	listed in the lean-pkg package index at that pin, trust level comparator

Quick start

git clone https://github.com/chenle02/markovprocess-pilot.git
cd markovprocess-pilot
lake update                         # once; fetches packages and the Mathlib cache
lake exe cache get                  # Mathlib oleans (no-op if already fetched)
lake build                          # builds MarkovProcess from source, then the pilot
lake env lean scripts/Axioms.lean   # prints the axioms of the main declarations

MarkovProcess ships no olean cache, so its 250 modules compile on the first build: about 3.5 minutes on 4 cores and 1.5 GB peak memory per process (measured). lake build Audit builds the comparator challenge and solution.

Find your way

You want to	Go to
Understand the proof and what came from MarkovProcess	docs/proof-outline.md
Rebuild, check pins, axioms and receipts	docs/reproducing.md
Read the Lean source	MarkovProcessPilot/BrownianExit.lean
Machine-readable claims	claims.yaml
Point a coding agent at the repository	llms.txt and AGENTS.md
Report a problem	open an issue

Repository map

Path	Contents
MarkovProcessPilot/BrownianExit.lean	the bridge and the exit-time theorem
MarkovProcessPilot.lean	umbrella import
Audit/Exit/	comparator statement (Mathlib only) and its proof
Audit/BrownianKernel/	comparator statement for the bridge (Mathlib only) and its proof
Audit/Smoke/, comparator/	comparator smoke test and configurations
scripts/Axioms.lean	#print axioms for the main declarations
.lean-receipts/	lower-tier and comparator receipts, bound to source commits
claims.yaml	machine-readable claims (schema claims/1)
logs/	build, cache and axiom logs
docs/	proof outline, reproduction notes, images

Citing

This pilot is a thin layer over Scott Armstrong's MarkovProcess, which did the hard part. If you use it, please cite MarkovProcess as its CITATION.cff asks:

Scott Armstrong. MarkovProcess: sub-Markov kernel semigroups and continuous-path Markov processes in Lean 4. Software, Apache-2.0. https://github.com/scottnarmstrong/MarkovProcess

This repository's CITATION.cff names MarkovProcess as the preferred citation, so GitHub's "Cite this repository" button shows it, and lists it under references at the pinned commit 666cda029098. To refer to the pilot itself, cite release v0.1.1, archived on Zenodo as doi:10.5281/zenodo.23452512 (all versions: doi:10.5281/zenodo.23452511); its Lean source is the source at commit 1548828e63c8 that the receipts cover (v0.1.1 changes documentation only).

Acknowledgments

The mathematics formalised here, and nearly all of the Lean, come from Scott Armstrong's MarkovProcess. Mathlib supplies the Brownian-motion API used by the bridge. Developed and verified with lean-pkg (doi:10.5281/zenodo.23272098); the receipts were made with lean-pkg 0.14.0 (doi:10.5281/zenodo.23445755).

Support

If this work is useful to you, you can sponsor Le Chen on GitHub. Sponsorship does not change what is claimed here or how it is checked. To support MarkovProcess, star and cite Armstrong's repository.

License

Apache-2.0, see LICENSE. MarkovProcess (Apache-2.0, Scott Armstrong) and Mathlib (Apache-2.0) are dependencies, not vendored, except one lemma adapted from MarkovProcess (mem_of_lt_exitTimeTrunc; its notice is in MarkovProcessPilot/BrownianExit.lean).

Maintained by Le Chen, Department of Mathematics and Statistics, Auburn University.