|
1 | 1 | # Changelog |
2 | 2 |
|
| 3 | +The release clock (`v4.29.1`, ...) tracks Lean/mathlib compatibility and is what Reservoir consumers pull. The dev clock (`0.230.x`) tracks day-to-day commits and is the unit used in commit messages and memory. A release header is a banner over the dev entries that ship in it; the dev entries are not demoted under it. |
| 4 | + |
| 5 | +## [Unreleased] |
| 6 | + |
| 7 | +## [0.230.61] - 2026-04-20 |
| 8 | + |
| 9 | +### Changed |
| 10 | +- **Wave 1 exhaustification API reorganization** (mathlib-style): |
| 11 | + `Theories/Semantics/Exhaustification/InnocentInclusion.lean` deleted. |
| 12 | + Its abstract API (`II`, `isInnocentlyIncludable`, `exhIEII`) had already |
| 13 | + been promoted to `Operators.lean` in earlier waves; the file's remaining |
| 14 | + content was the worked `FCWorld` example (5-world toy + IE/II |
| 15 | + computations + `free_choice`) and the `DisjWorld` simple-disjunction |
| 16 | + contrast. Both moved to the proper layer: |
| 17 | + - `Phenomena/Modality/Studies/BarLevFox2020.lean` now contains the |
| 18 | + `FCWorld` toy, `fcALT`/`fcPrejacent`, the IE non-excludability lemmas |
| 19 | + (`permAorB_not_ie`/`permA_not_ie`/`permB_not_ie`/`permAandB_is_ie`), |
| 20 | + `separatelyAB_in_cell` (cell witness), the one-line `free_choice` |
| 21 | + proof via `mem_II_of_cell_witness`, and the `DisjWorld` contrast |
| 22 | + (`simple_has_conjunction`). |
| 23 | + - `Theories/Semantics/Exhaustification/PresuppositionalExhaustification.lean` |
| 24 | + slimmed to abstract pex theory only: `homogeneous`/`pexIEII`/ |
| 25 | + `pexIEII_full`/basic projection lemmas/`negative_fc_entailment`/ |
| 26 | + `pex_basic_scalar`. All `FCWorld`-specific content (`pexFC`, |
| 27 | + `pex_fc`, `negPexFC`, `pex_double_prohibition`, `notReqA/B/AandB/AorB` |
| 28 | + duality abbrevs, `pex_negative_fc`, `pex_neg_necessity_double_req`, |
| 29 | + `exhIEII_fc`, `pexIEII_fc`) moved to the study file |
| 30 | + `Phenomena/Modality/Studies/DelPinalBassiSauerland2024.lean` — |
| 31 | + preserves the `Theories/` → `Phenomena/` dependency direction |
| 32 | + (Theories may not import from Phenomena). |
| 33 | + - `Phenomena/Modality/FreeChoiceCompare.lean` updated: imports |
| 34 | + `BarLevFox2020` + `DelPinalBassiSauerland2024` instead of |
| 35 | + `InnocentInclusion`; `Exhaustification.FreeChoice.permA/permB/free_choice` |
| 36 | + references stripped to bare names via the new opens. |
| 37 | + - Stale doc references in `Phenomena/Plurals/Studies/BarLev2021.lean` |
| 38 | + and `Theories/Semantics/Plurality/ExistentialPL.lean` rewritten to |
| 39 | + point at the new homes. |
| 40 | + - Dropped the old `simple_exclusive_or` theorem (broken statement — |
| 41 | + its third disjunct collapsed the conclusion into `propAorB`, and |
| 42 | + proving its strengthened form would require an unproved |
| 43 | + `propAandB_is_ie_simple` lemma; the abstract `cell` API in |
| 44 | + `Operators.lean` already captures the simple-disjunction contrast |
| 45 | + via cell-emptiness when ALT is closed under conjunction). |
| 46 | + - `pex_fc` now a 1-line corollary of `mem_II_of_cell_witness` + |
| 47 | + `separatelyAB_in_cell` (instead of two ~10-line `target_in_II` |
| 48 | + invocations); the new `permAandB_is_ie` lemma plugs the gap that |
| 49 | + the old `extend_II_with_target` sidestepped via `by_cases` on the |
| 50 | + target. |
| 51 | + |
| 52 | +## [0.230.60] - 2026-04-20 |
| 53 | + |
| 54 | +### Changed |
| 55 | +- **Phase 0 mathlib hygiene on `Phenomena/Polarity/`**: snake_case → |
| 56 | + camelCase across `LicensingContext` (9 constructors: |
| 57 | + `conditional_ant → conditionalAntecedent`, `before_clause → beforeClause`, |
| 58 | + `without_clause → withoutClause`, `only_focus → onlyFocus`, |
| 59 | + `too_to → tooTo`, `modal_possibility → modalPossibility`, |
| 60 | + `modal_necessity → modalNecessity`, `since_temporal → sinceTemporal`, |
| 61 | + `free_relative → freeRelative`) and `PolarityType.npi_fci → npiFci`, |
| 62 | + propagated across 30 files via word-boundary perl. `native_decide` |
| 63 | + → `decide` across all `Phenomena/Polarity/` (~160 sites). Hand-rolled |
| 64 | + `Decidable` instances on `isLicensedIn`/`isNPI`/`isFCI`/`isPPI`/ |
| 65 | + `canonicityConsistent` dropped — converted to `abbrev` so the underlying |
| 66 | + `∈`/`∨`/`=` instances are inferred. Bare `simp` in |
| 67 | + `NaturalLogic.de_signature_licenses_weak_npi` / |
| 68 | + `strong_npi_requires_antiadditive` tightened to `cases σ <;> decide`. |
| 69 | + Stray `set_option autoImplicit false` dropped from `KadmonLandman1993.lean`. |
| 70 | + Four data-sanity theorems deleted (`Typology.ch46_total`, |
| 71 | + `interrogative_most_common`, `interrogative_majority`, |
| 72 | + `Lahiri1998.all_share_bhii`) — descriptive statistics over external |
| 73 | + datasets, not load-bearing, now docstring prose. |
| 74 | +- **Phase 1 ContextProperties single classifier**: new |
| 75 | + `Core.Lexical.PolarityItem.LicensingMechanism` enum + |
| 76 | + `ContextProperties` structure (`signature`, `mechanism`, `prototype`, |
| 77 | + `citations`) + `contextProperties : LicensingContext → ContextProperties` |
| 78 | + canonical map for all 22 licensing contexts. The three previously parallel |
| 79 | + classifications now derive from a single source of truth: |
| 80 | + `KadmonLandman1993.contextEntailmentSig` is `(contextProperties c).signature`, |
| 81 | + `KadmonLandman1993.klExplanation` is `(contextProperties c).mechanism`, |
| 82 | + `Ladusaw1979.licensingStrength` is the Ladusaw coarsening of |
| 83 | + `(contextProperties c).signature.toDEStrength`. `KLExplanation` is now an |
| 84 | + `abbrev` for the Core enum. The three consistency theorems |
| 85 | + (`strengthening_implies_de`, `ladusaw_de_is_kl_strengthening`, |
| 86 | + `fc_iff_generic`) close by `cases ctx <;> decide` since both sides |
| 87 | + project from the same map. |
| 88 | + |
| 89 | +## [0.230.59] - 2026-04-20 |
| 90 | + |
| 91 | +### Added |
| 92 | +- **`Paradigms/WugTest.lean`**: NEW. Contract layer for the wug paradigm |
| 93 | + (@cite{berko-1958} + @cite{albright-hayes-2003}). `Attestation` enum |
| 94 | + (`attested`/`novel`); `HasAttestation` and `HasFrequency` typeclasses |
| 95 | + with full lens laws (`get_set`, `set_get`, `set_set`); polymorphic |
| 96 | + `Rate Cell R` observable. Two paradigm-level predicates: |
| 97 | + `NovelShowsFreqGradient` (the indexed-constraint / scaled-weight |
| 98 | + prediction: novel forms inherit a frequency gradient from analogous |
| 99 | + lexical items) and `NovelInvariantInFrequency` (the UseListed |
| 100 | + prediction: novel forms have no entry, so no entry-keyed frequency |
| 101 | + effect). `novelGradient_inconsistent_with_invariance` proves the two |
| 102 | + are mutually exclusive on any cell with two distinct frequencies — |
| 103 | + the structural source of the wug paradigm's role as a UseListed-vs- |
| 104 | + grammar discriminator. |
| 105 | +- **`Theories/Phonology/ParadigmUniformity/LexicalConservatism.lean`**: |
| 106 | + NEW. Sibling of `OptimalParadigms.lean` for the |
| 107 | + @cite{steriade-2000} Lexical Conservatism account. Reuses |
| 108 | + `liftPairwise` from `Defs.lean`; the LC channel is paradigm |
| 109 | + *membership* rather than a different lift — `lcParadigm candidate |
| 110 | + none = [candidate]`, `lcParadigm candidate (some a) = [candidate, a]`. |
| 111 | + `lc_unanchored_zero` is the structural derivation that an unanchored |
| 112 | + paradigm has zero LC-FAITH violations (the diagonal is the only |
| 113 | + pair, and `mismatch f f = 0`); this is the source of the LC |
| 114 | + prediction that bound stems impose no LC pressure, derived from |
| 115 | + paradigm construction rather than stipulated as a side condition. |
| 116 | +- **`blog/data/references.bib`**: `berko-1958` and `albright-hayes-2003` |
| 117 | + entries with verified DOIs (10.1080/00437956.1958.11659661 and |
| 118 | + 10.1016/S0010-0277(03)00146-X). Both anchor the new |
| 119 | + `Paradigms/WugTest.lean` file. |
| 120 | + |
| 121 | +### Changed |
| 122 | +- **`Linglib.lean`**: imports for `Paradigms.WugTest` and |
| 123 | + `Theories.Phonology.ParadigmUniformity.LexicalConservatism`. |
| 124 | + |
| 125 | +## [0.230.58] - 2026-04-20 |
| 126 | + |
| 127 | +### Added |
| 128 | +- **`Phenomena/Phonology/Studies/BreissKatsudaKawahara2026.lean`**: NEW. @cite{breiss-katsuda-kawahara-2026} ("Token frequency modulates optional paradigm uniformity in Japanese voiced velar nasalization", *Phonology* accepted, lingbuzz/009507). Architecture-only formalization: Fragment-typed bound vs. free-N2 schematic compounds (`cpd_bound`, `cpd_freeLow`, `cpd_freeHigh`), the bound→categorical / free→optional split via `JCompound.nasalisationObligatory`, and the abstract `puPressure` channel (zero-floored when N2 is bound, monotone in N2 token log-frequency when N2 is free). Three theorems: `bound_puPressure_zero` (PU pressure zero in the bound case for any strength function), `free_puPressure_eq_strength` (free case reduces to the strength function), `free_puPressure_monotone` (signed-monotonicity claim). Closing `architectural_constraint_zero_when_bound` packages the architectural punchline that any account of these data must produce a signed, frequency-modulated PU pressure that switches off in the bound case — naming `LexicalFrequency.UseListed` and `LexicalFrequency.IndexedConstraints` as ruled out, and `ScaledWeights` + `RepresentationStrength` as ruled in. No numerical fits, no specific corpus statistics, no MaxEnt fitting routine — those belong in the modelling companion (lingbuzz/009508). |
| 129 | +- **`Theories/Phonology/LexicalFrequency/Separation.lean`**: NEW. Abstract framework-separation theorems for the four lexical-frequency theories. Toy `ToyItem` carrier + `baseOne` constant constraint isolate the modulation channel. Five separations with concrete witnesses: `sep_indexed_vs_scaled` (within-stratum equal vs. continuous-monotone), `sep_uselisted_novel_invariant` (novel item dispatches to grammar), `sep_uselisted_vs_scaled_on_novel_pair` (UseListed flat across two novel items, ScaledWeights gradient), `sep_repstrength_vs_scaled_compositional` (compound activation inherited from constituents under min-combine vs. compound-only frequency), `sep_indexed_vs_uselisted_routing` (compute-through-grammar vs. skip-grammar at the same threshold). All proofs constructive (`norm_num` / `simp` after explicit hypothesis discharge). The file does not commit to any empirical case study; the Breiss-Katsuda-Kawahara compounds are one *application* of these separations, formalized in the sibling Phenomena file. |
| 130 | +- **`blog/data/references.bib`**: `breiss-katsuda-kawahara-2026` entry — `@article` accepted at *Phonology*, lingbuzz URL recorded, no DOI fabricated (omitted per CLAUDE.md). Sources field points at the new study + the four `LexicalFrequency/` theory files that anchor on the paper as a discriminating test case. |
| 131 | +- **`Linglib.lean`**: imports for `Belth2026` (previously orphaned in the moved-but-unlisted state from 0.230.55-ish), `BreissKatsudaKawahara2026`, and `LexicalFrequency.Separation`. LexicalFrequency import block re-sorted alphabetically. |
| 132 | + |
| 133 | +### Changed |
| 134 | +- **Toolchain bump v4.29.0 → v4.29.1.** `lean-toolchain` updated; `lakefile.lean` `mathlib` pin moved to `v4.29.1` and package `version` bumped to `v!"4.29.1"` (release-clock alignment per the two-clock CHANGELOG scheme introduced in this release). `lake-manifest.json` regenerated. README badges updated. No source changes required for the bump itself. |
| 135 | +- **CHANGELOG preamble** now describes the two-clock scheme (release clock = Lean compatibility, dev clock = `0.MAJOR.MINOR` per-commit). `## [Unreleased]` and `## [v4.29.1]` headers added above the existing dev entries (no demotion of `0.230.x` headers — the release header is a banner, not a wrapper). |
| 136 | + |
| 137 | +### Known issue (concurrent-session pollution) |
| 138 | +- Stale `.lake/build/lib/lean/Linglib/Phenomena/Polarity/{Stress,DisjunctionIgnorance,Exceptives}.{trace,ilean.hash,olean.hash}` artifacts left over from a concurrent session that deleted source files without `lake clean`. Causes spurious "no such file or directory" failures in full `lake build`; standalone module builds (including all new files in this entry) succeed cleanly. Removing the trace files would resolve, but is left for the owning session to handle. |
| 139 | + |
| 140 | +## [v4.29.1] - 2026-04-20 |
| 141 | + |
| 142 | +First Reservoir-published release. Tracks Lean 4.29.1 / mathlib v4.29.1. |
| 143 | + |
| 144 | +Library scope at first release: ~76 phenomenon categories across syntax, semantics, pragmatics, morphology, phonology, and processing; ~100 languages with parameterized Fragment lexica; competing frameworks formalized side-by-side (RSA vs. exhaustification; Minimalism vs. HPSG vs. CCG vs. DG vs. Construction Grammar; Kratzer vs. Kripke modality; OT vs. subregular phonology; etc.). Aggregated from ~230 dev iterations (0.1 → 0.230.57); see the dev log below for granular history. |
| 145 | + |
| 146 | +--- |
| 147 | + |
3 | 148 | ## [0.230.57] - 2026-04-20 |
4 | 149 |
|
5 | 150 | ### Changed |
|
11 | 156 | ### Added |
12 | 157 | - **`Core/Inheritance/Prototype.lean`**: NEW. Hosts the `Prototype α` structure (graded category membership, `category : α` + `typicality : α → ℚ`) plus `atLeastAsTypical`, `moreTypical`, `atLeastAsTypical_refl`, `atLeastAsTypical_trans`. Moved out of `Basic.lean` to keep the network module orthogonal to rationals/linarith — consumers that only need the isA backbone no longer pay for `Mathlib.Data.Rat.Defs`. Single consumer `WesterbeekKoolenMaes2015.lean` switched over. |
13 | 158 |
|
| 159 | +## [0.230.56] - 2026-04-20 |
| 160 | + |
| 161 | +### Added |
| 162 | +- **`Theories/Phonology/Subregular/Agree.lean`**: NEW. AGREE specialization of the generic forbidden-pair TSL_2 constructor — the (· ≠ ·) dual of the OCP's (· = ·) specialization. Mirrors `OCP.lean`: `agreeForbidden`, `TSLGrammar.agree p := TSLGrammar.ofForbiddenPairs (· ≠ ·) p`, `AgreeCleanPair`, `agreeCleanPair_some_some` (uses `not_not` to flip), `AgreeCleanPair.isBoundaryVacuous`, plus two bridge theorems `mkAgreeOnTier_zero_iff_isChain` and `mkAgreeOnTier_zero_iff_in_agree_lang` showing the OT-side AGREE constraint and the subregular-side TSL_2 language are co-extensive by construction. Carries the same `α : Type` (not `Type*`) limitation as `OCP.lean` due to monomorphism in `Phonology.Constraints` / `Core.Constraint.eval`. Module docstring frames the OCP/AGREE structural duality (no two same → dissimilation; no two different → assimilation/harmony) and notes that asymmetric harmonies (e.g. Kikongo nasal harmony) instantiate the generic constructor directly rather than factoring through either specialization. |
| 163 | +- **`Theories/Phonology/OptimalityTheory/Constraints.lean`**: `mkAgreeOnTier` and `mkAgreeOnTier_is_markedness` — the OT-side `NamedConstraint` constructor for AGREE-style markedness, defined as `mkForbidPairsOnTier` with `R := (· ≠ ·)`. Parallel to existing `mkOCPOnTier`. |
| 164 | + |
| 165 | +### Changed |
| 166 | +- **`Phenomena/Phonology/Studies/Hansson2010.lean`**: refactored to use the AGREE specialization. Navajo sibilant harmony is *symmetric* dissimilation-of-disagreement, so `navajoSibilantHarmony := TSLGrammar.agree NSeg.onTier` (down from `TSLGrammar.ofForbiddenPairs NSeg.forbidDisagreement NSeg.onTier`) and `NSeg.forbidDisagreement` is deleted entirely. OT-side `navajoAgreeAntCC` → `navajoAgree` via `mkAgreeOnTier`. The four accept/reject theorems use `unfold navajoSibilantHarmony TSLGrammar.agree; decide` (typeclass inference doesn't see through the specialization wrapper even with `@[reducible]`). Mathlib hygiene: `match`-style `DecidablePred NSeg.onTier` instance, `@[reducible]` on grammar/data defs, `open Core Core.Computability.Subregular Phonology.Subregular` discipline at top of namespace. |
| 167 | +- **`Phenomena/Phonology/Studies/RoseWalker2004.lean`**: stays on the generic `TSLGrammar.ofForbiddenPairs` constructor — Kikongo nasal harmony is *asymmetric* (forbidden pair is `(nasal, voiced-stop)`, not the reverse) and so factors through neither OCP nor AGREE. Docstring updated to explicitly call out this distinction. Mathlib hygiene: `match`-style `DecidablePred KSeg.onTier` and `DecidableRel KSeg.forbidNasalStop` instances, `@[reducible]` on grammar/data defs, `kikongoAgreeNasalCC` → `kikongoAgree`, `open Core` discipline at top of namespace. |
| 168 | +- **`Linglib.lean`**: import line for `Theories.Phonology.Subregular.Agree` added under the OCP import. |
| 169 | + |
14 | 170 | ## [0.230.55] - 2026-04-20 |
15 | 171 |
|
16 | 172 | ### Added |
|
0 commit comments