# FormalSLT v0.2.0

Released 2026-08-24.

FormalSLT v0.2.0 expands the library from its classical learning-theory base
into anytime-valid inference and learning from adaptive or dependent data.

## Highlights

- Finite-sample VC, Rademacher, stability, and metric-entropy results,
  including finite chaining bounds and continuous entropy-integral endpoints
  under explicit assumptions.
- PAC-Bayes change-of-measure tools and all-sample-size empirical-Bernstein
  bounds for IID data.
- Confidence sequences, e-processes, mixture and stitched boundaries, and
  explicit allocation costs for adaptive selection.
- PAC-Bayes guarantees for adaptive trajectories with finite hypothesis
  catalogs and with arbitrary measurable state and hypothesis spaces.
- Finite-state stationary-risk certification with Poisson corrections,
  Dobrushin contraction, empirical transition confidence, and predeclared
  candidate-kernel selection.
- Checked applications showing how the library components compose, including
  the random-refresh load model and a structured controlled-queue example.
- A theorem map, searchable generated documentation, focused checker files,
  and a short overview film.

## Supported API

The v0.2 compatibility surface consists of four topic imports:

```lean
import FormalSLT.PACBayes
import FormalSLT.Sequential
import FormalSLT.StochasticDynamics
import FormalSLT.VC
```

The exact declaration allowlist and compatibility policy are in
[Public API stability](../api-stability.md). Implementation modules outside
that allowlist remain available but are not frozen for the v0.2.x line.

## Install

```lean
require «formal-slt» from git
  "https://github.com/Robby955/FormalSLT.git" @ "v0.2.0"
```

Then run:

```bash
lake update
lake exe cache get
lake build
```

FormalSLT v0.2.0 uses Lean 4.32.2 and Mathlib 4.32.2.

## Verification

The release commit passes the repository CI suite, including:

- a full Lean build and all checked examples;
- isolated public-import and v0.1 compatibility checks;
- downstream installation on Linux and macOS;
- scans for `sorry`, `admit`, and custom axioms;
- `#print axioms` checks for the public theorem surface; and
- deterministic source and documentation asset packaging.

The expected public axiom set is
`[propext, Classical.choice, Quot.sound]`. The tag workflow resolves
`v0.2.0` once, checks the exact commit on Linux and macOS, compares the two
identity receipts, and packages source, documentation, a manifest, and
checksums. See the
[release workflow](https://github.com/Robby955/FormalSLT/actions/workflows/release-tag-smoke.yml)
and [verification guide](../public-release-checklist.md).

## Scope boundaries

- The IID empirical-Bernstein endpoint is uniform over sample size but is not
  itself an optional-stopping theorem.
- Data-dependent selection is covered only where the theorem quantifiers make
  it explicit, typically over a family fixed before observation.
- Current stationary-risk results are finite-state. Continuous-state
  certification remains open.
- The general continuous Dudley theorem is not yet part of the stable API.
  Existing continuous entropy-integral results retain explicit boundary,
  separability, and modulus assumptions.
- The controlled-queue receipt is retrospective and conditional on its
  one-parameter refresh-family model; it is an application, not a
  specification test for that model.

The detailed assumption ledger is
[Assumptions and nonclaims](../assumptions-and-nonclaims.md).

## Citation and artifacts

Citation metadata is in [`CITATION.cff`](../../CITATION.cff). No DOI is
claimed for this release unless one is later recorded in that file and on the
GitHub Release.

The [GitHub Release](https://github.com/Robby955/FormalSLT/releases/tag/v0.2.0)
provides the release notes and the deterministic asset bundle generated from
the tagged commit.