# Lean 4 formalization of Schlenker, "Anti-dynamics: presupposition projection without dynamic semantics"

Core Lean 4 only (no Mathlib); tested with Lean 4.34.0/4.34.1 (`~/.elan/bin/lean`, `~/.elan/bin/lake`).
**No `sorry`** in any file.

## How to check

```bash
cd lean
./check.sh            # rebuilds from scratch (about 5 s); fails on any error or sorry
# or, equivalently:
lake build
```

Single file (after `lake build` has produced the dependencies):

```bash
lake env lean AntiDynamics/Propositional.lean
```

To see the axioms used by a result, put `import AntiDynamics` and e.g.
`#print axioms AntiDyn.Propositional.theorem1_i` in a scratch file and run `lake env lean scratch.lean`
(expected: only `propext`, `Quot.sound`, and possibly `Classical.choice`).

## Files (in dependency order)

| File | Content |
|---|---|
| `Core.lean` | formulas `Fm` over leaf clauses; static semantics; Heim's `Upd`/`Def` (Beaver's `or`); Lemma S (`upd_eq_TS`: defined update = static truth set = Theorem 1(ii)); contexts and completions `Ctx`/`Compl`; Transparency `Transp`; the decomposition lemmas `transp_neg/conj/disj/cond` (paper's proof cases (c)-(f) and the Transparency Lemma) |
| `Lifting.lean` | accessed pairs; `Sys.lift` (connective steps of Theorems 1-2); Non-Triviality `NT`; Lemma 2; Dynamic Transparency (23) |
| `Propositional.lean` | propositional clauses; **Theorem 1** (`theorem1_i`, `theorem1_ii`); Transparency Lemma; examples (14)-(17); the naive requirement (10)-(12); Dynamic Transparency |
| `Deviants.lean` | `and*`, `or*` (24), the four `unless` rules (32), (33) |
| `Counting.lean`, `Arith.lean` | finite counting, rank pieces, realization lemmas; trees-of-numbers arithmetic (`find_step` = repaired Case 1/2 of Lemma 1(i)); the Zone B gap |
| `Quantified.lean` | quantificational model (domain `{0..n-1}`, trees of numbers), clauses `(Q P . R)` |
| `Lemma1.lean` | **Lemma 1(i), 1(ii)** |
| `Theorem2.lean` | Non-Triviality Corollary, `quant_leaf`, **Theorem 2 (corrected)**, Heim's claims, Dynamic Transparency with quantifiers |
| `Counterexamples.lean` | scenarios of §5.1, soccer example (34), **countermodel to Theorem 2 as stated** |
| `Infinite.lean` | footnotes 12 and 16 (infinite domains) |
| `Strings.lean` | serialization, Syntactic Lemma (19a,b), literal string definition of Transparency and its equivalence with the context version |
| `Theorem1Strings.lean` | Theorem 1 with the literal string definition |

See `../RESULTS.md` for the result-by-result table (paper location, statement, Lean statement, file:line, status),
the list of errors found, and the fidelity notes.