Reader route · Lean
Import a topic, then narrow to a theorem.
The v0.2 API is organized around four topic umbrellas. They remain the supported discovery surface; current-main endpoints added after the release are listed separately in the API-stability page, and individual implementation modules remain available when a downstream proof needs a smaller import.
Topic imports
import FormalSLT.PACBayesPAC-Bayes change of measure, empirical-Bernstein bounds, and posterior-risk endpoints.
import FormalSLT.SequentialSequential processes, filtrations, conditional means, and anytime-valid components.
import FormalSLT.StochasticDynamicsHistory-dependent trajectories, Markov risk, Poisson corrections, and empirical kernels.
import FormalSLT.VCVC dimension, growth functions, and finite-class learning bounds.
Worked applications are opt-in. Use import FormalSLT.Applications for the checked 20-state random-refresh load receipt. Application-specific declarations are not in the 19-name v0.2 compatibility allowlist.
Pin the dependency
Use the v0.2 release tag:
require «formal-slt» from git
"https://github.com/Robby955/FormalSLT.git" @ "v0.2.0"To reproduce this documentation build exactly:
require «formal-slt» from git
"https://github.com/Robby955/FormalSLT.git" @
"1752e0d9ede42a277cc69e277adc4d4802eccdac"Pin unreleased work by commit. The generated site replaces 1752e0d9ede42a277cc69e277adc4d4802eccdac with its full source commit. Use that commit for development beyond v0.2.0 rather than a moving branch.
Reuse discipline
- Start from the fully qualified declaration shown in doc-gen. Long names are deliberate: they carry the scope and mechanism.
- Check the theorem’s type before relying on prose. Finiteness, measurability, adaptation, boundedness, and positivity premises remain explicit arguments or typeclass assumptions.
- Use the stable-import examples as executable API receipts for the four umbrellas.
- For public capstone endpoints, inspect the associated
#print axiomsreceipt. The intended public profile is[propext, Classical.choice, Quot.sound].
Compatibility is scoped. The release tag and API stability policy cover the four topic imports and the named declaration allowlist, not every implementation module.
Inspection tools
- Declaration search
Search the generated Lean API by declaration or module name.
- Concept-keyed theorem index
Find declarations by mathematical vocabulary, with every source link pinned to this build.
- Module tree
Traverse the generated namespace and import hierarchy.
- Stable-import receipts
Concrete compile targets that import one public topic umbrella at a time.
Next step
Open one umbrella and check one endpoint.
The API search is the authoritative generated surface for this exact documentation build.