# Morse–Bott theory of free loop spaces: Lean formalizations

This collection contains partial Lean formalizations of results in the
[notes on Morse–Bott theory of free loop spaces](https://ncatlab.org/nlab/show/nLab+materials#MaterialsMorseBottOfLoopSpaces).
Additional formalization projects may be added alongside the present one.

## Current project

[`fundamental-groups-of-s2xs2-quotient`](fundamental-groups-of-s2xs2-quotient/README.md)
studies the concrete quotient

\[
Q=(S^2\times S^2)/((x,x)\sim(x,-x))
\]

and its free-loop space. It constructs the universal cover of Q,
computes its second homotopy group and deck action, and determines the
fundamental groups of the components of LQ, including their named generators.
The application to L L₁S² takes the classical geometric equivalence
Q ≃ L₁S² as a separate input; that analytic equivalence is not formalized here.

Its Lean library and namespace are `S2xS2Quotient`.

## Checking a project

Enter the project folder and follow its README. Each project keeps its own
Lean toolchain and dependency manifest. For the current project:

```text
cd fundamental-groups-of-s2xs2-quotient
lake exe cache get
lake build
lake env lean -DwarningAsError=true Audit.lean
lake env lean -DwarningAsError=true Contracts.lean
```

The archive contains source and verification records, without downloaded
toolchains, dependency caches, or compiled outputs. Included third-party
proof sources retain their licenses and provenance.
