# Lean formalisation of the Appendix of "Local Contexts"

Lean 4 (checked with 4.34.x), **core only** (no Mathlib, no lake needed).

## How to check

```
cd lean
sh check.sh          # compiles all files in dependency order; prints ALL OK
```
`check.sh` uses `lean -o build/X.olean X.lean` with `LEAN_PATH=build`.  Set `LEAN=/path/to/lean` if `lean`
is not on `PATH` (default fallback: `~/.elan/bin/lean`).  Deprecation/unused-variable warnings are expected.
No file contains `sorry`.

## Files (dependency order)

| File | Content |
|---|---|
| `LCAbstract.lean` | abstract theory of transparent restrictions / local contexts (items 4, 10-11, 12-16, 17-21): Lemmas 1-5, Existence, Theorems 20, 21; the counterexample to the paper's proof of Lemma 1 |
| `PropSyntax.lean` | propositional fragment: syntax, classical semantics, syntactic contexts (`plug`, `occs`, frames) |
| `PropTheory.lean` | dynamic semantics, incremental/symmetric Transparency, Theorem 1, bridge to `LCAbstract`, Sat / Sat', Theorems 20-22 for the propositional fragment |
| `KleeneCore.lean` | supervaluations, Strong Kleene by supervaluation, standard Strong Kleene; Lemmas 6-7, Theorem 41 |
| `KleeneTheory.lean` | acceptability; Lemma 8, Theorem 36, Theorem 38a, Lemma 11, Theorem 39a; the collapse theorem for the propositional fragment |
| `Sanity.lean` | non-vacuity checks of the definitions |
| `Quantifier.lean` | `(No P . QQ')`: Theorem 38b / 39b (countermodel), general characterisations |
| `InfinitelyMany.lean` | Example 23 |
| `bruteforce_check.py` | Python exploration used to test conjectures before proving (not part of the proofs) |

See `../RESULTS.md` for the theorem-by-theorem table (with file:line), the errors found in the paper, and the
fidelity notes; `../TODO.md` for the extracted list of definitions/results and their status.