# Results: Lean verification of Schlenker, "Anti-dynamics" (JoLLI 2007)

All Lean files are in `lean/` (`lean/README.md` explains how to check; `lean/check.sh` rebuilds from
scratch and fails on any `sorry`).  Core Lean 4 only (no Mathlib), Lean 4.34.  **No `sorry` anywhere.**
`#print axioms` shows only `propext`, `Quot.sound`, and (for theorems using classical reasoning)
`Classical.choice`.

Notation in the "Lean" column: `S := sys v i0` (propositional) or `sys M` (quantified);
`S.Transp C F` = Transparency; `S.Def F C` = `C[F] ≠ #`; `S.Upd F C` = `C[F]`;
`S.TS F C = {w ∈ C : w ⊨ F}`.  File:line are `lean/AntiDynamics/<file>.lean:<line>`.

## 1. Table of results

**Verdict** (does the paper's claim hold?): **confirmed** = holds as stated; **corrected-proof** = statement holds but the paper's proof was wrong or had a gap, repaired in Lean; **modified-statement** = statement as printed is false or ill-posed, a corrected statement is proven; **disconfirmed** = false with no repair; **n/a** = definition, new result of ours, or not formalized. The **Status** column records only the formalization status.


Status: **proven** / **proven-corrected** / **counterexample found** / **confirmed** (a claim of the paper checked
in Lean, e.g. a worked example) / **not formalized (why)**.

### Definitions and background

| # | Result | Paper | Informal statement | Lean (as formalized) | File:line | Verdict | Status |
|---|---|---|---|---|---|---|---|
| R1 | Language and Heim/Beaver dynamic semantics | §3.1 (18), §3.2 (21), p.335-336 | formulas over clauses with `not/and/or/if`; CCPs with definedness (`or` per Beaver; `if F.G` = `C − C[F][not G]`) | `Fm`, `Sys.Upd`, `Sys.Def`; propositional clauses `PLeaf`; quantified clauses `QLeaf`, `QModel.qupd/qdef` | Core.lean:29,93,101; Propositional.lean:21,37; Quantified.lean:78,83 | n/a | formalized (definitions) |
| R2 | Static semantics | §3.2 (25), p.338 | `p̲p'` = conjunction; `if` = material implication; `(Q P.R)` = `f(\|P−R\|,\|P∩R\|)` | `evalF`, `QModel.qsem` | Core.lean:40; Quantified.lean:73 | n/a | formalized (definitions) |
| R3 | Transparency (two readings) | §2.1 (5),(6); §3.2 (26), p.330-1, 338 | for every initial string `α d̲d'` and completion `β`: `C ⊨ α(d and γ)β ⇔ αγβ` | (a) `Sys.Transp` (contexts/completion contexts); (b) `Sys.StrTransp` (literal strings) | Core.lean:206; Strings.lean:451 | n/a | formalized (definitions) |
| R4 | The two readings coincide | implicit in §3.1 Syntactic Lemma | `StrTransp C F ↔ Transp C F` for every model and every `F` | `Sys.strTransp_iff_transp` | Strings.lean:458 | confirmed | proven |
| R5 | Syntactic Lemma (19b) | §3.1 (19b), p.335 | no formula string is a proper initial string of another | `ser_append_inj : ser F ++ s = ser G ++ t → F = G ∧ s = t` | Strings.lean:45 | confirmed | proven (hypothesis "starts with `(s`, `s` not a parenthesis" is not needed) |
| R6 | Syntactic Lemma (19a) | §3.1 (19a), p.335 | if `α φ β` is a formula (`α` initial string of an occurrence) then `φ` is a constituent of it and the formula is a completion context applied to `φ` | `syntactic_lemma_a : pre c ++ ser φ ++ β = ser G ++ tl → ∃ c'', Compl c c'' ∧ G = c''.plug φ ∧ β = post c'' ++ tl` | Strings.lean:203 | confirmed | proven (paper's proof is a sketch) |

### Section 2 (motivation, worked examples)

| # | Result | Paper | Informal statement | Lean | File:line | Verdict | Status |
|---|---|---|---|---|---|---|---|
| R7 | Naive requirement (10) is symmetric in `and` | §2.2 (10), p.332 | `C ⊨ F ⇔ F*` cannot derive the asymmetry of `and` | `naive_conj_symmetric : Naive C (G and H) ↔ Naive C (H and G)`; `transp_conj_asymmetric` (Transparency is asymmetric) | Propositional.lean:224,231 | confirmed | confirmed |
| R8 | Naive requirement is too weak for atoms | §2.2 (11),(12), p.332-3 | for `p̲p'` naive = `C ⊨ p'⇒p`, strictly weaker than `C ⊨ p` | `naive_atomic : Naive C p̲_a p'_b ↔ ∀w∈C, p'_b → p_a`; `naive_strictly_weaker` (1-world countermodel) | Propositional.lean:199,215 | confirmed | confirmed |
| R9 | Transparency of an atom | §2.2 (13), p.333 | `Transp(C, p̲p')` iff `C ⊨ p` | `transp_atomic` | Propositional.lean:135 | confirmed | confirmed |
| R10 | (14) `(p̲p' and q)` presupposes `p` | §2.3, p.333 | `Transp ↔ C ⊨ p` | `ex14` (proved from the decomposition lemmas, not from Heim) | Propositional.lean:145 | confirmed | confirmed |
| R11 | (15) `(p and q̲q')` presupposes `p⇒q` | §2.3, p.333 | `Transp ↔ C ⊨ p⇒q` | `ex15` | Propositional.lean:151 | confirmed | confirmed |
| R12 | (16) `(if p̲p'. q)` presupposes `p` | §2.3, p.334 | `Transp ↔ C ⊨ p` | `ex16` | Propositional.lean:164 | confirmed | confirmed |
| R13 | (17) `(if p. q̲q')` presupposes `p⇒q` | §2.3, p.334 | `Transp ↔ C ⊨ p⇒q` | `ex17` | Propositional.lean:170 | confirmed | confirmed |
| R14 | Dynamic Transparency | §2.2 (8), §3.2 (23), p.332, 337 | `C[F] ≠ # ⇒ C[F] = C[F*]` | `dynamic_transparency` (propositional), `dynamic_transparency_quant` (with quantifiers), generic `Sys.dyn_transparency`; `star_defined` (`F*` always defined) | Propositional.lean:243,248; Theorem2.lean:233; Lifting.lean:255 | confirmed | proven |
| R15 | Dynamic Transparency fails for `or*` | §3.2 (24), p.337-8 | for `H = ((not p) or* p̲p')` and `C[p̲p'] = #`: `C[H]` defined but `C[H] ≠ C[H*]` | `or_star_breaks_dynamic_transparency` (explicit 4-world model) | Deviants.lean:112 | confirmed | confirmed |
| R16 | Deviant `and*` | §1.3 (2), p.328 | `C[F and* G] = C[G and F]`; agrees with `and` on trigger-free `F, G`; Moldavia predictions reversed | `andStar_eq_swap`, `andStar_agrees_trigfree`, `andStar_not_transparency`, `andStar_too_strong` (Transparency, which is fixed by syntax + bivalent content, does not yield `and*`) | Deviants.lean:48,53,70,87 | confirmed | confirmed |

### Section 4 (propositional case)

| # | Result | Paper | Informal statement | Lean | File:line | Verdict | Status |
|---|---|---|---|---|---|---|---|
| R17 | Transparency Lemma (a) | (27a), p.339 | `Transp(C,(G and δ)) ⇒ Transp(C,G)` | `transparency_lemma_a`; underlying `transp_conj : Transp C (G and H) ↔ Transp C G ∧ Transp (TS G C) H` | Propositional.lean:101; Core.lean:242 | confirmed | proven |
| R18 | Transparency Lemma (b) | (27b), p.339 | `Transp(C,(if G.δ)) ⇒ Transp(C,G)` | `transparency_lemma_b`; `transp_cond` | Propositional.lean:106; Core.lean:300 | confirmed | proven |
| R19 | Proof cases (c)-(f) of Thm 1 | pp.339-342 | `Transp` decomposes through `not/and/or/if` exactly as Heim's `Def` | `transp_neg/conj/disj/cond`; `Sys.lift` (induction); typo in (e) (see Q4) | Core.lean:227,242,271,300; Lifting.lean:35 | confirmed | proven |
| R20 | **Theorem 1 (i)** | p.338 | for every `F` and every `C ⊆ W` (language containing `⊤,⊥`): `Transp(C,F) ↔ C[F] ≠ #` | `theorem1_i : (sys v i0).Transp C F ↔ (sys v i0).Def F C` and, with literal strings, `theorem1_i_strings : StrTransp C F ↔ Def F C` | Propositional.lean:91; Theorem1Strings.lean:16 | confirmed | proven (statement correct) |
| R21 | **Theorem 1 (ii)** | p.339 | `C[F] ≠ # → C[F] = {w ∈ C : w ⊨ F}` | `theorem1_ii` (`Sys.upd_eq_TS`; independent of Transparency) | Propositional.lean:96; Core.lean:110 | confirmed | proven |

### Section 5 (quantificational case)

| # | Result | Paper | Informal statement | Lean | File:line | Verdict | Status |
|---|---|---|---|---|---|---|---|
| R22 | Heim's claims for `Q` | §5 intro, p.343 | `(Q P̲P'.R)` presupposes `∀d P(d)`; `(Q P.R̲R')` presupposes `∀d[P(d)⇒R(d)]` | `heim_claim_i`, `heim_claim_ii`; with a presuppositional restrictor: `qdef_both` (see Q5) | Theorem2.lean:189,195,205 | confirmed | confirmed |
| R23 | Scenario 5.1(i) | §5.1, p.343 | 2 P-individuals, `Q = less than three`: Transp holds trivially, Heim's presupposition fails, NT violated | `less_than_three_scenario` (model expressive, restrictor size constant = 2); `not_nt_of_lt3` (general: all worlds `<3` P-individuals ⇒ NT fails) | Counterexamples.lean:80,40 | confirmed | confirmed |
| R24 | Scenario 5.1(ii): Constancy is needed | §5.1, p.343-4 | `C={w,w',w''}`, restrictor sizes 2,4,4: NT and Transp hold but Heim fails | `constancy_needed` (`NT ∧ Transp ∧ ¬qdef ∧ ¬∃p constant`, expressive model, any `Y`) | Counterexamples.lean:104 | confirmed | confirmed |
| R25 | Non-Triviality Corollary | (29), p.344-5 | NT (+ constant domain size `n`) ⇒ `f` not constant on `{a+b ≤ n}`; NT (+ constant restrictor size `p`) ⇒ not constant on `{a+b = p}` | `nt_corollary_i`, `nt_corollary_ii` | Theorem2.lean:80,96 | confirmed | proven |
| R26 | Infinite domains, `Q = infinitely many` | fn 12, p.344 | if `P^w − R^w` is finite then `(Q P.(R and γ)) ⇔ (Q P.γ)` at `w` for all `γ` | `transpInf_of_finite`; **new**: converse `not_transpInf_of_infinite` and `transpInf_iff : TranspInf P R ↔ Fin' (P∖R)` | Infinite.lean:25,42,58 | confirmed | proven (single-world semantic version) |
| R27 | Infinite-domain example | fn 16, p.355 | integers, `P−Q = {13}` finite ⇒ Transp holds although Heim's presupposition (all integers ≠ 13) fails | `footnote16` | Infinite.lean:65 | confirmed | confirmed |
| R28 | Realization lemma (constructions of `X`,`Y`) | Lemma 1 proofs, p.346-8 | subsets with prescribed intersection sizes exist | `realize_four`, `realize_two`, `exists_subset` (rank pieces) | Counting.lean:144,101,94 | n/a | proven (new; replaces the paper's informal "take b elements from ...") |
| R29 | **Lemma 1(i)** | p.345-7 | domain constant size `n`, every property expressible, `f` non-constant on `{a+b ≤ n}` ⇒ `Transp(C,(Q P̲P'.R)) ↔ C ⊨ ∀d P(d)` | `lemma1_i : M.Expressive → (∃ a b a' b', a+b ≤ n ∧ a'+b' ≤ n ∧ f a b ≠ f a' b') → (RT M C q k ↔ ∀w∈C ∀d<n, I k w d)` | Lemma1.lean:102 | corrected-proof | proven-corrected (statement true; Case 2/Zone B of the paper's proof has a gap: Q2, repaired in `find_step`) |
| R30 | **Lemma 1(ii)** | p.347-8 | restrictor of constant size `p`, every property expressible, `f` non-constant on `{a+b = p}` ⇒ `Transp(C,(Q P.R̲R')) ↔ C ⊨ ∀d[P(d)⇒R(d)]` | `lemma1_ii` (restrictor `P` may itself carry underlined material; `P(d)` = its static value) | Lemma1.lean:157 | confirmed | proven |
| R31 | Accessed pairs; **Lemma 2** | §5.3, p.348-350 | NT is inherited by all pairs accessed by `⟨C,F⟩` | `Accessed`; `Sys.lemma2 : NT C₀ F₀ → Accessed C₀ F₀ C F → NT C F` | Lifting.lean:17,201 | confirmed | proven (Q6) |
| R32 | Lemma 1 + NT for a clause | Remark after Lemma 1 / step (g), p.345, 351 | under NT and Constancy, `Transp(C,(Q P.R)) ↔ Heim's definedness` | `quant_leaf` | Theorem2.lean:116 | confirmed | proven |
| R33 | **Theorem 2 as stated** | p.350 | hypotheses: (i) constant domain size, (ii) constant restrictor sizes, (iii) NT | `theorem2_needs_expressiveness`: a 2-world model with these three properties, a clause where `Transp` holds but `C[F] = #` | Counterexamples.lean:179 | modified-statement | **counterexample found** (missing hypothesis, Q1) |
| R34 | **Theorem 2 corrected** | p.350 | (i)-(iii) + every property expressible ⇒ for every accessed `⟨C',F'⟩`: `Transp(C',F') ↔ C'[F'] ≠ #` and `C'[F'] = {w∈C': w⊨F'}` | `theorem2 (hexp : M.Expressive) C F (ConstRestr M C F) (NT IsQ C F) : ∀ C' F', Accessed C F C' F' → (Transp C' F' ↔ Def F' C') ∧ (Def F' C' → Upd F' C' = TS F' C')` | Theorem2.lean:155 | modified-statement | proven-corrected |
| R35 | Vacuity of Constancy/NT/expressiveness hypotheses | discussion §5.1, §6 | each hypothesis is needed | (a) NT needed: R23; (b) Constancy needed: R24, R39 (soccer); (c) expressiveness needed: R33 | Counterexamples.lean | confirmed | counterexamples found |

### Section 6

| # | Result | Paper | Informal statement | Lean | File:line | Verdict | Status |
|---|---|---|---|---|---|---|---|
| R36 | `unless`: rules (32)a-d | §6.1, p.352 | rules (a)-(d) agree on trigger-free `F,G` and diverge otherwise; (a) = `if not F, G` | `unlessA_is_if_not`, `unless_variants_agree_trigfree` (with corrected (d)), `unless_rules_differ`; **printed (d) is wrong**: `unlessD_paper_is_wrong` | Deviants.lean:171,177,249,195 | modified-statement | confirmed, with typo found (Q7); (b),(c): `unlessB_update_ill_defined` (Deviants.lean:266) |
| R37 | (33) predictions | §6.1, p.352-3 | (a): "if John came, he is here"; (b): "if John didn't come ..."; (c),(d): "John is here"; Transparency gives (a) | `unless_33` (all five equivalences) | Deviants.lean:220 | confirmed | confirmed |
| R38 | `unless` vs `if not` under Transparency | §6.1, fn 13, p.353 | same projection | `transp_unless_eq_if_not : Transp C (F or G) ↔ Transp C (if (not F) . G)` | Deviants.lean:206 | confirmed | confirmed (for the static content `F ∨ G`; `unless` itself is not added to the syntax) |
| R39 | Soccer example (34) | §6.5, p.354-5 | in each world either every P-individual has decided or fewer than 3 P-individuals: Transp holds; Heim predicts failure | `soccer_example` (W = {A wins, B wins}, 6 individuals) | Counterexamples.lean:138 | confirmed | confirmed |
| R40 | Overgeneration claim | §6.1, p.353 | same syntax + same bivalent contribution ⇒ same projection | true by construction (`Transp` mentions only syntax and static semantics); instance R38 | – | confirmed | confirmed trivially (no separate theorem) |
| R41 | Accommodation (global/local) | §6.2, p.353 | informal | – | – | n/a | not formalized (informal proposal, no formal claim) |
| R42 | Meta-constraint on the lexicon (Shan/Heim), linear vs processing order, DRT | §6.3, 6.4, 6.6 | research suggestions | – | – | n/a | not formalized (open questions, not claims) |
| R43 | Empirical data (1), (3), (4), (7); Stalnaker's (i)-(iii) | §1-2 | judgments; historical background | – | – | n/a | not formalized (empirical/historical) |

## 2. Errors and issues found in the paper

Severity: **S** = statement false/incomplete (checked in Lean), **P** = proof gap with a true statement (repaired in
Lean), **T** = typo / imprecision.

**Q1 (S). Theorem 2 omits a hypothesis it needs (p.350).**  Lemma 1 assumes "(b) any property over the domain can be
expressed by some predicate", but Theorem 2 lists only constant domain size, constant restrictor sizes and NT, and its
proof (case (g)) simply invokes Lemma 1.  Without (b) the theorem is false.  Countermodel
(`Counterexamples.lean:179`, decided by computation): worlds `{0,1}` (two), individuals `{0,1}`, predicate letters
`P, P', R` all with extension `⊆ {0}` (so `P` fails of individual 1), `Q = at least one`, `F = (Q P̲P'. R)`, `R` true of
`0` in one world only.  Domain size 2 (constant), restrictor `P∧P'` has 1 element in every world (constant), NT holds
(`F` true in one world, false in the other), yet every available predicate is included in `P`, so `Transp(C,F)`
holds while `C[F] = #` (individual 1 violates `P`).  The corrected theorem (`theorem2`) adds `M.Expressive`.
(Natural in spirit since §2.1 says the language is "quite expressive", but it must be a hypothesis of Theorem 2.)

**Q2 (P). Lemma 1(i), Case 2, "Zone B" (p.347).**  Once `f` is constant (value `v`) on the small triangle
`a+b ≤ |P^w|` and `f(a*,b*) ≠ v` for a point of the big triangle, the paper projects `(a*,b*)` "horizontally" onto the
line `a+b = |P^w|` (same `a`-coordinate) when `b* > |P^w|`.  Such a point exists only if `a* ≤ |P^w|`.  For `a* > |P^w|` and
`b* > |P^w|` the claim "for some `c` with `0 < c ≤ |D^w−P^w|`, `f(a*,b*−c) ≠ f(a*,b*)`" can be false: with `|P|=2`,
`n=8`, `f(a,b)=[a+b>2]`, `(a*,b*)=(3,3)` there is no such `c` (`paper_zoneB_step_fails`).  The lemma itself is true:
project along any step `(i,j)` with `i+j = a*+b*−|P|` (`find_step`, `zoneB_repaired`).  The whole of Lemma 1(i) is
proved in Lean (`lemma1_i`) with this repair.  Also: the statement of the general "some point where the value changes"
step must be restricted to the small triangle (Q3).

**Q3 (T). Lemma 1(i), Case 1 (p.346).**  "for some `(a,b)` for which `a+b ≤ n` with `a ≥ 1`, `f(a−1,b) ≠ f(a,b)`" must read
`a+b ≤ |P^w|` (the construction takes `a+b−1` elements of `P^w`).

**Q4 (T). Typos in proofs.**
(a) Proof of Theorem 1, case (e)(i), end of the converse (p.341): "Thus Transp(C, (G and H)), i.e. Transp(C, F)" should
be `(G or H)`.
(b) Proof of Theorem 2, case (f) (p.351): "By the Transparency Lemma (part (b)), this entails that Transp(C', (if G. H))"
must be "**not** Transp(C', (if G. H))".
(c) Transparency Lemma (27), p.339: "for some formula G and some sentence completion δ, Transp(C,(G δ))" — the connective
in `(G and δ)` is lost and "for some" should be "for all"; what is proved is `Transp(C,(G and δ)) ⇒ Transp(C,G)` for every
`G, δ` (and `Transp(C,(if G.δ)) ⇒ Transp(C,G)`).  Also the proof of (e) uses that the completion can contain either `and` or
`or` after the left disjunct/conjunct; this is correct but nowhere said (formalized in `Compl`).

**Q5 (T). Ambiguous notation in step (g) of Theorem 2 (p.351-352).**  For `F' = (Q P̲P'. R̲R')` the paper writes
"`C' ⊨ ∀d P(d)` and `C' ⊨ ∀d [P(d) ⇒ R(d)]`".  Heim's condition (21) is `∀d [(P∧P')(d) ⇒ R(d)]`, where `P∧P'` is the static
value of the restrictor.  Read literally with `P` the presupposition, "`∀d [P(d)⇒R(d)]`" would be too strong (given
`∀d P(d)` it says `∀d R(d)`).  Formalized correctly in `qdef_both` and in `lemma1_ii` (restrictor = its static value).

**Q6 (T). Circular-looking use of `C[G]` in Lemma 2 (p.349-350).**  The proof of Lemma 2, cases (iii)b, (iv)b, (v)b,
uses `w ∈ C, w ⊨ G ⇒ w ∈ C[G]`, i.e. Theorem 2(ii) for `G`, before Theorem 2 is proved.  It is a true fact about Heim's
dynamic semantics alone (`upd_eq_TS`, proved independently of Transparency), so there is no circularity.

**Q7 (T). Rule (32)d and the update of (32)b,c (p.352).**  (i) The update of (32)d, `C − C[(not G)][F]`, equals
`{w ∈ C : F → G}` for trigger-free `F, G`, not the bivalent content `F ∨ G` of `unless F, G`; it should be
`C − C[(not G)][(not F)]`.  With the printed rule the claim that all four rules "make exactly the same predictions when
F and G contain no presupposition triggers" is false (`unlessD_paper_is_wrong`; corrected rule agrees:
`unless_variants_agree_trigfree`).  (ii) Rules (b), (c) are given the update "as in (a)", which needs `C[(not F)][G] ≠ #`,
not guaranteed by their definedness conditions (`unlessB_update_ill_defined`); the paper itself hints at this.

**Q8 (T). Syntactic Lemma (19b) (p.335-336).**  The proof argues that "each object-language rule would require a left
parenthesis before `c`", which is true only of the compound rules (the atomic pair `p_i p_k` and predicate rules are not
covered); the statement is true and is just prefix-freeness of the bracketed syntax (`ser_append_inj`), for *every*
formula (the restriction "starts with `(s`" is unnecessary).  (19a) as stated ("`α` is the beginning of a constituent in
*any well-formed string that contains `α`*") is imprecise: it holds for strings having `α` as an *initial string*
(`syntactic_lemma_a`).

**Points checked and found correct (no error).**  Statement of Theorem 1 and all of its cases (formalized; only needs `⊤`, `⊥`
in the language); Lemma 1(ii) including both cases of its proof; Lemma 2; Non-Triviality Corollary; the three quantifier
scenarios of §5.1/§6.5 and footnotes 12 and 16; examples (14)-(17); (23); (24); (32)a,(33).

**Remarks (not errors).**  (1) Theorem 2's constancy hypothesis is only needed for clauses whose *nuclear scope* carries a trigger
(Lemma 1(i) needs only NT + constant domain), and NT only for the clauses actually used; the theorem could be sharpened.
(2) On infinite domains with `Q = infinitely many` the exact condition is: Transparency at `w` iff `P^w − R^w` is finite
(`transpInf_iff`), which the paper states only in the "if" direction.

## 3. Fidelity of the formalization (what was simplified)

* **Strings vs contexts.**  The paper defines Transparency on strings with "any sentence completion `β`".  `Core.lean`
  uses one-hole contexts; a completion of the initial string `α` is a context with the same left material, the same
  bracket depth, a free right material, and a free connective (`and`/`or`) where the initial string is a bare `(`.
  `Strings.lean` proves that this coincides with the literal string definition (`strTransp_iff_transp`), on the connective
  structure, treating each clause as one token.
* **Inside quantificational clauses** the completion of `(Q P̲P'` is `. Y)` (any predicate `Y`) and of `(Q P . R̲R'` is `)`
  ("for syntactic reasons", as in the paper); this is encoded directly in `lvar`, not derived from a string grammar
  for clauses.  Replacement `γ` in `(P and γ)` is an atomic predicate (`P_m`), as (18) allows only `(P_i and P_k)`.
* **Language.**  Propositional letters, and tautology/contradiction `p ∨ ¬p`, `p ∧ ¬p` built from a designated letter `i0`.
  In `p̲_a p'_b` the presupposition `a` and assertion `b` are independent letters.  Individual variables and the meta-language
  `∀d`, `⇒`, `⇔` of (18) are Lean's own, not object-language syntax.
* **Semantics.**  Worlds form an arbitrary type; context sets are predicates.  The domain is `{0,…,n−1}` (constant finite
  size built into `QModel`).  A quantifier is given only by its tree of numbers `f : ℕ → ℕ → Bool`; permutation invariance,
  extension and conservativity are thereby built in, and *no* further property of `f` is assumed (NT supplies non-constancy).
  Counting is via `List.range`/`countP` (core Lean).
* **Non-Triviality** is formalized semantically on contexts (`Sys.NT`), matching (28); the two conjuncts
  (`≠ T`, `≠ F`) are required for the *same* completion, as in the paper.
* **Infinite domains** are treated in `Infinite.lean` in a self-contained semantic form (one world, `γ` ranging over all
  sets), not inside the CCP framework of `QModel`.
* **`and*`, `or*`, `unless`** are modeled as definedness/update functions over the propositional CCPs; `unless` is not
  added to the syntax (its Transparency behaviour is obtained via the static-content-equivalent `or`/`if not`).
* **Not formalized:** empirical judgments, Stalnaker's pragmatic account, accommodation, the meta-constraint proposal, linear
  order vs processing order, DRT.  The corrected Theorem 2 is proven for the fragment (18) restricted to clauses
  `(Q P . R)` with predicates `P_i`, `P̲_iP'_k`, `(P_i and P_k)`.