# KTV Proof Formalization

Lean formalization for *Spectral Gap for the Binary Fixed-Margin Swap Chain*.

## Build

This project uses Lean through Lake and mathlib.

```bash
lake exe cache get
lake build KTV
```

The Lean toolchain is pinned in `lean-toolchain`; mathlib is pinned in
`lakefile.toml` / `lake-manifest.json`.

## Main Entry Point

The top-level file is [`KTV.lean`](KTV.lean).

The paper-facing closed statement exposed there is:

- `KTV.Johnson.binaryFixedMarginLazySwapChain_spectralGap_card`

The supporting closed statements in `KTV/Johnson/MainTheorems.lean` are:

- `KTV.Johnson.fixedMarginDistinctRowPairHeatBathGenerator_gap_card`
- `KTV.Johnson.fixedMarginOrderedDistinctRectangleSwapOperator_gap_half_colPair_card`
- `KTV.Johnson.fixedMarginOrderedDistinctRectangleLazySwapOperator_gap_card`

These are assembled from the module-level results under `KTV/Johnson/`.

## Project Structure

The formalization is organized under `KTV/Johnson/`. The top-level theorem wrappers are in `KTV/Johnson/MainTheorems.lean`; the detailed file-by-file map is in [`MODULE_LAYOUT.md`](MODULE_LAYOUT.md).

## Verification Notes

The repository is intended to build without `sorry`, `admit`, `axiom`, or
`unsafe` declarations in the `KTV` sources.

Useful local checks:

```bash
lake env lean -D maxErrors=30 KTV.lean
lake build KTV
rg -n "sorry|admit|axiom|unsafe" KTV KTV.lean
```

Generated Lean artifacts such as `.olean` files and Lake build outputs are
ignored by `.gitignore`.