# lgt — Per-file informal summaries

Auto-generated by `/lean-summarize` (one summary per Lean source file).
Each entry lists every definition and theorem in source order with
LaTeX statements and proof dependencies.

## Priority files (the public mass-gap surface)

| Source | Summary | Length | Sorries |
|---|---|---|---|
| [`LGT/Lattice/CellComplex.lean`](../LGT/Lattice/CellComplex.lean) | [CellComplex.md](LGT/Lattice/CellComplex.md) | 803 | 0 |
| [`LGT/GaugeField/UnitaryGroup.lean`](../LGT/GaugeField/UnitaryGroup.lean) | [UnitaryGroup.md](LGT/GaugeField/UnitaryGroup.md) | 223 | 0 |
| [`LGT/MassGap/YMMeasure.lean`](../LGT/MassGap/YMMeasure.lean) | [YMMeasure.md](LGT/MassGap/YMMeasure.md) | 353 | 0 |
| [`LGT/Gibbs/YMSpec.lean`](../LGT/Gibbs/YMSpec.lean) | [YMSpec.md](LGT/Gibbs/YMSpec.md) | 458 | 0 |
| [`LGT/Gibbs/YMIsGibbs.lean`](../LGT/Gibbs/YMIsGibbs.lean) | [YMIsGibbs.md](LGT/Gibbs/YMIsGibbs.md) | 961 | 0 |
| [`LGT/Gibbs/YMDobrushin.lean`](../LGT/Gibbs/YMDobrushin.lean) | [YMDobrushin.md](LGT/Gibbs/YMDobrushin.md) | 515 | 0 |
| [`LGT/MassGap/DobrushinVerification.lean`](../LGT/MassGap/DobrushinVerification.lean) | [DobrushinVerification.md](LGT/MassGap/DobrushinVerification.md) | 229 | 0 |
| [`LGT/MassGap/MassGap3D.lean`](../LGT/MassGap/MassGap3D.lean) | [MassGap3D.md](LGT/MassGap/MassGap3D.md) | 498 | 0 |
| [`LGT/MassGap/MassGap2D.lean`](../LGT/MassGap/MassGap2D.lean) | [MassGap2D.md](LGT/MassGap/MassGap2D.md) | 109 | 0 |
| [`LGT/MassGap/StrongCoupling.lean`](../LGT/MassGap/StrongCoupling.lean) | [StrongCoupling.md](LGT/MassGap/StrongCoupling.md) | 1962 | **1** (`ym_mass_gap_exponential_decay`) |

## Reading order for a new collaborator

1. **[CellComplex](LGT/Lattice/CellComplex.md)** — discrete geometry: links, plaquettes, boundary links, incidence lemmas.
2. **[UnitaryGroup](LGT/GaugeField/UnitaryGroup.md)** — concrete gauge group $U(n)$ with all the typeclasses + trace bounds.
3. **[YMMeasure](LGT/MassGap/YMMeasure.md)** — Wilson action, Boltzmann weight, partition function, the YM probability measure.
4. **[YMSpec](LGT/Gibbs/YMSpec.md)** — YM as a Gibbs specification (conditional measures + the four GibbsSpec axioms).
5. **[YMIsGibbs](LGT/Gibbs/YMIsGibbs.md)** — DLR identity: `ymMeasure` is a Gibbs measure for `ymGibbsSpec`.
6. **[DobrushinVerification](LGT/MassGap/DobrushinVerification.md)** — the column-sum bound `dobrushinAlpha < 1` at strong coupling.
7. **[YMDobrushin](LGT/Gibbs/YMDobrushin.md)** — `DobrushinCondition` instance for `ymGibbsSpec`.
8. **[MassGap3D](LGT/MassGap/MassGap3D.md)** — assembles the d ≥ 3 multisite covariance bound.
9. **[StrongCoupling](LGT/MassGap/StrongCoupling.md)** — distance-parameterized hypothesis-discharging wrapper + the open mass-gap target.
10. **[MassGap2D](LGT/MassGap/MassGap2D.md)** — the 2D Doeblin-path mass gap (with bridge hypothesis).

## Other files (not yet summarized)

19 additional `.lean` files in `LGT/Bridge/`, `LGT/Lattice/` (the
exterior derivative / forms), `LGT/GaugeField/` (Connection /
Holonomy / GaugeGroup / GaugeTransformation), `LGT/WilsonAction/`
(GaugeInvariance / PlaquetteAction / WilsonLoop), and the `MassGap/`
files not in the priority list (DoeblinCondition, GaugeFixing,
Integrability, Locality, SingleSiteKernel, TransferMatrix). Run
`/lean-summarize <path>` per file to generate them.

## Refresh

To regenerate a summary for one file (after the Lean source has
changed), run `/lean-summarize <path/to/File.lean>`. The skill
checks the source's mtime against the summary and skips if fresh.