interpTy .t Bool → Prop: unify Montague type interpretation with Mathlib Prop + Decidable pattern, eliminate IModel

Author: hawkrobe

CHANGELOG.md

@@ -1,5 +1,66 @@
 # Changelog
 
+## [0.229.550] - 2026-04-05
+
+### Changed
+- **`interpTy .t` Bool → Prop migration**: unified Montague type interpretation with Mathlib's Prop + Decidable pattern
+  - Root change: `Model.interpTy .t = Prop` (was `Bool`); eliminates `= true` coercions, `decide` wrapping, and `Bool.eq_iff_iff` idioms throughout
+  - Eliminated redundant `IModel` type (merged into `Model` — it only hardcoded `World := World4`)
+  - Quantifier denotations are now direct Prop: `every_sem m R S = ∀ x, R x → S x`, `some_sem m R S = ∃ x, R x ∧ S x`, etc.
+  - GQ properties: added `P`-prefixed Prop versions (`PConservative`, `PScopeUpwardMono`, etc.) alongside existing Bool `Core.Quantification` library
+  - `evalTree` stays `Option Bool` via `decide` at the `.t` boundary (preserves `native_decide` proofs)
+  - `BProp W := W → Bool` unchanged (modal operators, RSA predicates stay Bool-valued)
+  - `TypeShifting.lean`: `ident`, `BE`, `A`, `lower`, `iota`, `NOM`, `THE` all updated; `BE_unique` fully rewritten for classical Prop reasoning
+  - ~40 downstream files updated (Phenomena studies, Fragments, Composition, Entailment)
+
+## [0.229.549] - 2026-04-05
+
+### Added
+- **Halle & Marantz 1993 — Distributed Morphology and the Pieces of Inflection**: formalized the foundational DM paper
+  - `Phenomena/Morphology/Studies/HalleMarantz1993.lean`: English verb inflection paradigm using `FeatureVI`/`subsetPrinciple` (5 context-free VI entries with competition theorems), conditioned allomorphy via `VocabItem` with root restrictions (Paninian principle: `-t`/`∅` override default `-d`), Tns+Agr fusion using `FusionRule` (all 5 paradigm cells derived from fused features, `fusion_always_spellable` universally quantified), impoverishment → VI syncretism derivation (`deleteFeature` + `pipeline_fusion_impoverishment_vi` threading fusion through impoverishment to VI), Baker 1985 bridge (`tnsAgr_outside_gfRules`: all Tns/Agr features outside all GF-rule categories in Bybee's relevance hierarchy, connecting three papers)
+
+### Changed
+- `references.bib`: `halle-marantz-1993` role upgraded from `cited` to `formalized`
+
+## [0.229.548] - 2026-04-05
+
+### Changed
+- **MSK2025 audit — fix entailment profiles and derivation claims**
+  - `Fragments/French/Predicates.lean`: fixed `sentience := false` (both profiles — anticausative subjects can be non-sentient: *le mur rougit*), `stationary := false` (not applicable to intransitive sole arguments); split into `cosSubjectProfile` (property-change verbs, both control classes) and `motionCosSubjectProfile` (motion verbs: approcher, plier only); durcir/radoucir/refroidir correctly use `cosSubjectProfile` (no movement entailment)
+  - `MartinSchaeferKastner2025.lean`: removed `deriveControlLevel` and `control_level_is_movement` biconditional — ControlLevel is pragmatic/world-knowledge, not derivable from entailments; added `control_level_not_from_entailments` (rougir = refroidir profiles), `movement_sufficient_not_necessary`; added `ResponsibilityGoal` + `predictSePreferenceExt` for G3 (responsibility preference); added `availableForms`/`choice_only_with_plusMinusSe` (choice prerequisite); K-G 2009 syncretism docstring
+
+## [0.229.547] - 2026-04-05
+
+### Added
+- **Martin, Schäfer & Kastner 2025 — lexical pragmatics of reflexive marking**: formalized three generalizations about French ±*se* anticausatives, connecting voice syncretism to Gricean Manner reasoning
+  - `GriceanMaxims.lean`: added `MannerSubmaxim` (M1–M4: avoidObscurity, avoidAmbiguity, beBrief, beOrderly) and `MannerViolation` types, paralleling existing `QuantitySubmaxim`/`QuantityViolation`
+  - `Fragments/French/Predicates.lean`: 10 new change-of-state verb entries with `EntailmentProfile` — 5 limited-control (brunir, noircir, pâlir, rajeunir, rougir) and 5 in-control (approcher, durcir, plier, radoucir, refroidir)
+  - `Phenomena/Causation/Studies/MartinSchaeferKastner2025.lean`: `ControlLevel` derived from `EntailmentProfile.movement`, `SeMarking` morphological class, voice ambiguity formalization via `VoiceFlavor.nonThematic`/`.reflexive` syncretism, three generalization theorems, per-verb control derivation, unaccusativity bridge, anti-causation-claim theorem, experimental data from Tables 2 & 4
+
+## [0.229.546] - 2026-04-05
+
+### Added
+- **Zimmermann 2026 "African Lambdas I"**: formalized core contributions on the nominal domain in African languages
+  - `Theories/Semantics/Lexical/Determiner/ChoiceFunction.lean`: choice function type (`CF`, `SkolemCF`) for indefinite semantics, with correctness conditions and scope-via-binding theorems (@cite{reinhart-1997}, @cite{kratzer-1998})
+  - `Fragments/Hausa/Determiners.lean`: first Hausa fragment — *koo-wane* (distributive UQ = Q_∀[ONE_∅]), *duk(a)* (non-distributive UQ = bare Q_∀), *wani/wata* (∃-quantifier INDEF with flexible scope), bare NP
+  - `Fragments/Akan/Determiners.lean`: first Akan fragment — *nó* (DEF marker with disputed analysis: strong vs weak vs demonstrative), *bí* (choice function INDEF with wide scope under negation), *bi-ara* (flexible universal: ∀/NPI/FC)
+  - `Phenomena/Reference/Studies/Zimmermann2026.lean`: bridge theorems connecting Hausa *koo*/*duk* to Q_∀ + ONE decomposition, CF-based scope contrast between Akan *bí* and Hausa *wani*, extended typological sample (13 languages)
+  - 11 new bibliography entries (zimmermann-2026, zimmermann-2008, zimmermann-2014, bombi-2018, owusu-2022, philipp-2022, reinhart-1997, winter-1997, mirrazi-2024, matthewson-1999, schwarzschild-2002)
+
+### Fixed
+- `Definite.lean:99`: Akan *nó* was uncritically labeled as Schwarz's strong article — now notes the Bombi/Owusu dispute
+- `Core/Definiteness.lean:129`: `bareNominal` comment oversimplified Akan bare NPs — now notes context-dependent readings
+
+## [0.229.545] - 2026-04-05
+
+### Changed
+- **Glass 2025 deepening**: migrated causal model infrastructure, eliminated ad-hoc types, added postsupposition field, and connected to neg-raising
+  - `Doxastic.lean`: replaced ad-hoc `CausalVar`/`CausalEdge`/`CausalModel` (~130 lines) with `Core.StructuralEquationModel` — `beliefFormationDynamics` uses `CausalDynamics` with `CausalLaw.simple`, `satisfiesPLC` uses `causallySufficient`, PLC theorems via `normalDevelopment` propagation instead of BFS graph reachability
+  - `VerbEntry.lean`: added `PostsupType` enum (`.weakContrafactive`/`.strongContrafactive`) and `postsupType` field to `VerbCore` — postsuppositions are now structural, not flagged by string matching
+  - `Mandarin/Predicates.lean`: yǐwéi now carries `postsupType := some .weakContrafactive` directly; deleted `hasExceptionalPostsupposition` string-matching function
+  - `Glass2025.lean`: updated to use `postsupType` field (`yiwei_has_postsupposition`), added §8 NegRaising bridge (`veridicality_determines_both` connecting PLC gap to neg-raising gap via shared veridicality source)
+  - `Postsupposition.lean`: added `strong_entails_weak` (CG ⊨ ¬p → CG ◇ ¬p for nonempty contexts) and `weak_not_entails_strong` (counterexample: `[true, false]`)
+
 ## [0.229.544] - 2026-04-05
 
 ### Changed

Linglib.lean

@@ -43,6 +43,7 @@ import Linglib.Core.Conjectures
 import Linglib.Core.Semantics.CommonGround
 import Linglib.Core.Parse
 import Linglib.Core.Semantics.Presupposition
+import Linglib.Core.Semantics.Postsupposition
 import Linglib.Core.Semantics.ContentLayer
 import Linglib.Core.Agent.ProductOfExperts
 import Linglib.Core.Partition
@@ -156,8 +157,11 @@ import Linglib.Core.Divergence
 import Linglib.Core.ChannelCapacity
 import Linglib.Core.Inheritance
 import Linglib.Core.Morphology.MorphProfile
+import Linglib.Core.Morphology.Wordhood
+import Linglib.Core.Morphology.FormMeaningMapping
 import Linglib.Theories.Morphology.Core.Circumfix
 import Linglib.Theories.Morphology.Core.Exponence
+import Linglib.Theories.Morphology.Core.MirrorPrinciple
 import Linglib.Theories.Morphology.Core.Monotonicity
 import Linglib.Theories.Morphology.Core.ScaleFromParadigm
 import Linglib.Theories.Morphology.Core.WordStructure
@@ -440,6 +444,8 @@ import Linglib.Fragments.German.Negation
 import Linglib.Fragments.German.AdjAgreement
 import Linglib.Fragments.German.V2
 import Linglib.Fragments.German.Distributives
+import Linglib.Fragments.Hausa.Determiners
+import Linglib.Fragments.Akan.Determiners
 import Linglib.Fragments.SwissGerman.Case
 import Linglib.Fragments.Georgian.Coordination
 import Linglib.Fragments.Georgian.Morph
@@ -506,6 +512,7 @@ import Linglib.Fragments.Latin.Coordination
 import Linglib.Fragments.Latvian.IndeterminatePronouns
 import Linglib.Fragments.Japanese.Case
 import Linglib.Fragments.Japanese.Comparison
+import Linglib.Fragments.Japanese.Coordination
 import Linglib.Fragments.Japanese.Determiners
 import Linglib.Fragments.Japanese.Classifiers
 import Linglib.Fragments.Japanese.Nouns
@@ -821,6 +828,7 @@ import Linglib.Phenomena.Constructions.Resultatives.Studies.Tay2024
 import Linglib.Phenomena.Causation.Studies.BeaversEtAl2021
 import Linglib.Phenomena.Causation.Typology
 import Linglib.Phenomena.Causation.Studies.MartinRoseNichols2025
+import Linglib.Phenomena.Causation.Studies.MartinSchaeferKastner2025
 import Linglib.Phenomena.Causation.Studies.NadathurLauer2020
 import Linglib.Phenomena.Causation.Studies.MunozPerez2026
 import Linglib.Phenomena.Causation.Studies.Coon2019
@@ -1018,6 +1026,9 @@ import Linglib.Phenomena.Negation.FlexibleNegation
 import Linglib.Phenomena.Morphology.CompositionBridge
 import Linglib.Phenomena.Morphology.Studies.Bybee1985
 import Linglib.Phenomena.Morphology.Studies.ZwickyPullum1983
+import Linglib.Phenomena.Morphology.Studies.KalinBjorkmanEtAl2026
+import Linglib.Phenomena.Morphology.Studies.Baker1985
+import Linglib.Phenomena.Morphology.Studies.HalleMarantz1993
 import Linglib.Phenomena.Morphology.Typology
 import Linglib.Phenomena.Morphology.Studies.AckermanMalouf2013
 import Linglib.Phenomena.Morphology.CategoryChanging
@@ -1039,6 +1050,7 @@ import Linglib.Phenomena.Plurals.Basic
 import Linglib.Phenomena.Plurals.Homogeneity
 import Linglib.Phenomena.Plurals.NonMaximality
 import Linglib.Phenomena.Plurals.Studies.HaslingerEtAl2025
+import Linglib.Phenomena.Plurals.Studies.HaslingerHienEtAl2025
 import Linglib.Phenomena.Questions.Studies.QingEtAl2025
 import Linglib.Phenomena.Plurals.Compare
 import Linglib.Phenomena.Plurals.Studies.Champollion2017
@@ -1104,6 +1116,7 @@ import Linglib.Phenomena.Presupposition.Studies.Grove2022
 import Linglib.Phenomena.Presupposition.Studies.Beaver2001
 import Linglib.Phenomena.Presupposition.Studies.Blutner2000
 import Linglib.Phenomena.Presupposition.Studies.Karttunen1973
+import Linglib.Phenomena.Presupposition.Studies.Glass2025
 import Linglib.Phenomena.Modality.OutlookMarkers
 import Linglib.Phenomena.Classifiers.Typology
 import Linglib.Phenomena.Classifiers.Studies.Chierchia1998
@@ -1228,6 +1241,7 @@ import Linglib.Phenomena.Phonotactics.Studies.HayesWilson2008
 import Linglib.Phenomena.Tone.Studies.Hyman2006
 import Linglib.Phenomena.Tone.Studies.Lionnet2025
 import Linglib.Phenomena.Tone.Studies.AkinboFwangwar2026
+import Linglib.Phenomena.CompensatoryLengthening.Studies.Hayes1989
 -- Theories: CCG
 import Linglib.Theories.Syntax.CCG.Core.Basic
 import Linglib.Theories.Syntax.CCG.Core.Combinators
@@ -1499,9 +1513,13 @@ import Linglib.Theories.Morphology.DM.NominalStructure
 import Linglib.Theories.Morphology.DM.RichExponent
 import Linglib.Theories.Morphology.DM.Allosemy
 import Linglib.Theories.Morphology.DM.Impoverishment
+import Linglib.Theories.Morphology.DM.PostSyntacticOps
 import Linglib.Theories.Morphology.Core.CliticVsAffix
 import Linglib.Theories.Morphology.Core.ICP
+import Linglib.Theories.Morphology.Core.WordhoodBridge
+import Linglib.Theories.Morphology.Nanosyntax.Core
 import Linglib.Theories.Morphology.WP.LCEC
+import Linglib.Theories.Morphology.PFM.Core
 import Linglib.Phenomena.ArgumentStructure.Studies.Pylkkanen2008
 import Linglib.Phenomena.ArgumentStructure.Studies.Larson1988
 import Linglib.Phenomena.ArgumentStructure.Studies.Bruening2021
@@ -1578,6 +1596,9 @@ import Linglib.Theories.Semantics.Lexical.Determiner.PolarizedIndividuals
 import Linglib.Theories.Semantics.Lexical.Determiner.Quantifier
 import Linglib.Theories.Semantics.Lexical.Determiner.Exceptive
 import Linglib.Theories.Semantics.Lexical.Determiner.Possessive
+import Linglib.Theories.Semantics.Lexical.Determiner.UnifiedUniversal
+import Linglib.Theories.Semantics.Lexical.Determiner.ONEModifiers
+import Linglib.Theories.Semantics.Lexical.Determiner.ChoiceFunction
 import Linglib.Theories.Semantics.Lexical.Expressives.Basic
 import Linglib.Theories.Semantics.Lexical.Expressives.OutlookMarker
 import Linglib.Theories.Semantics.Probabilistic.Scenarios.Basic
@@ -1672,6 +1693,7 @@ import Linglib.Theories.Semantics.Lexical.Verb.EventStructure
 import Linglib.Theories.Semantics.Lexical.Verb.ArgDerivation
 import Linglib.Theories.Morphology.RootTypology
 import Linglib.Theories.Morphology.ReversalRestitution
+import Linglib.Theories.Morphology.TheorySpace
 import Linglib.Theories.Semantics.Events.SpatialTrace
 import Linglib.Theories.Semantics.Events.DimensionBridge
 import Linglib.Theories.Semantics.Events.TemporalDecomposition
@@ -1681,7 +1703,6 @@ import Linglib.Theories.Semantics.Attitudes.CDistributivity
 import Linglib.Theories.Semantics.Attitudes.EmbeddingConstraints
 import Linglib.Theories.Semantics.Attitudes.ContentComposition
 import Linglib.Theories.Semantics.Attitudes.ContextQuantification
-import Linglib.Theories.Semantics.Attitudes.ContrafactiveGap
 import Linglib.Theories.Semantics.Attitudes.Doxastic
 import Linglib.Theories.Semantics.Attitudes.Intensional
 import Linglib.Theories.Semantics.Attitudes.Parasitic
@@ -1900,6 +1921,7 @@ import Linglib.Phenomena.Gradability.Studies.WaldonEtAl2023
 import Linglib.Phenomena.Reference.Studies.WaldonDegen2021
 import Linglib.Phenomena.Reference.Studies.Elbourne2013
 import Linglib.Phenomena.Reference.Studies.Longobardi2005
+import Linglib.Phenomena.Reference.Studies.Zimmermann2026
 import Linglib.Phenomena.Binominals.Studies.TenWolde2023
 import Linglib.Theories.Pragmatics.RSA.ScalarImplicatures.Basic
 import Linglib.Theories.Pragmatics.RSA.ScalarImplicatures.Embedded.Attitudes
@@ -1931,6 +1953,8 @@ import Linglib.Theories.Phonology.Harmony.OT
 import Linglib.Theories.Phonology.Syllable.Defs
 import Linglib.Theories.Phonology.Syllable.Foot
 import Linglib.Theories.Phonology.Syllable.NaturalClass
+import Linglib.Theories.Phonology.Moraic.Defs
+import Linglib.Theories.Phonology.Moraic.CompensatoryLengthening
 import Linglib.Theories.Phonology.RuleBased.Defs
 import Linglib.Theories.Phonology.HarmonicGrammar.Basic
 import Linglib.Theories.Phonology.HarmonicGrammar.MaxEnt

Linglib/Core/Definiteness.lean

@@ -126,7 +126,11 @@ def bridgingPresupType : BridgingSubtype → DefPresupType
 - How many overt article forms? (0, 1, or 2)
 - What expresses weak-article definites? (bare nominal, overt article, etc.) -/
 inductive WeakArticleStrategy where
-  | bareNominal    -- No overt form; bare noun = weak definite (Akan, Mauritian Creole)
+  | bareNominal    -- No overt form; bare noun = weak definite (Mauritian Creole).
+                   -- Akan also uses this strategy, though Akan bare NPs have
+                   -- context-dependent readings: definite for globally unique
+                   -- referents (*ewia* 'sun'), indefinite/∃ otherwise.
+                   -- See @cite{owusu-2022}, @cite{philipp-2022}.
   | overtArticle   -- Distinct overt weak article (German contracted, Fering A-form)
   | sameAsStrong   -- Single form for both (Haitian Creole `la`)
   deriving DecidableEq, Repr

Linglib/Core/Mereology.lean

@@ -267,6 +267,15 @@ theorem IsSumHom.cum_preimage {α β : Type*}
 def Overlap {γ : Type*} [PartialOrder γ] (x y : γ) : Prop :=
   ∃ z, z ≤ x ∧ z ≤ y
 
+/-- Overlap is reflexive: every element overlaps itself (via x ≤ x). -/
+theorem Overlap.refl {γ : Type*} [PartialOrder γ] (x : γ) : Overlap x x :=
+  ⟨x, le_refl x, le_refl x⟩
+
+/-- Overlap is symmetric. -/
+theorem Overlap.symm {γ : Type*} [PartialOrder γ] {x y : γ}
+    (h : Overlap x y) : Overlap y x :=
+  let ⟨z, hzx, hzy⟩ := h; ⟨z, hzy, hzx⟩
+
 /-- Extensive measure function: additive over non-overlapping entities.
     @cite{krifka-1998} §2.2, eq. (7): μ(x ⊕ y) = μ(x) + μ(y) when ¬O(x,y).
     Examples: weight, volume, number (cardinality). -/

Linglib/Core/Morphology/FormMeaningMapping.lean

@@ -0,0 +1,47 @@
+/-!
+# Form-Meaning Mapping Phenomena
+@cite{kalin-bjorkman-etal-2026}
+
+§4 of @cite{kalin-bjorkman-etal-2026} identifies seven descriptive types
+of form-meaning mapping — the relationships between phonological exponents
+and morphosyntactic features/functions.
+
+These seven types are theory-neutral descriptive categories: any theory
+of morphology must account for them (whether by generating them directly,
+reanalyzing them, or invoking extra mechanisms).
+-/
+
+namespace Core.Morphology.FormMeaningMapping
+
+/-- The seven descriptive types of form-meaning mapping.
+    @cite{kalin-bjorkman-etal-2026} §4. -/
+inductive MappingType where
+  /-- One meaning/function ↔ one exponent, invariant.
+      Example: root *cat* is always `\/kæt\/`. -/
+  | oneToOne
+  /-- One meaning/function → multiple *competing* exponents
+      (context-sensitive selection).
+      Example: English plural *-z, -s, -ɪz, -ən, ∅*. §4.1. -/
+  | allomorphy
+  /-- One meaning/function → multiple *co-occurring* exponents
+      (non-competing, simultaneous expression).
+      Example: Amharic *k'al-at-otʃtʃ* 'words' (two plural markers). §4.2. -/
+  | multipleExponence
+  /-- Multiple related meanings/functions → one exponent
+      (non-co-occurring contexts share a form).
+      Example: English *-ed* for past tense and past participle. §4.3. -/
+  | syncretism
+  /-- Multiple co-occurring meanings/functions → one exponent
+      (bundled into a single form).
+      Example: French *du* = *de* + *le*. §4.4. -/
+  | portmanteau
+  /-- A meaning/function has no corresponding form — the paradigm
+      cell is empty.
+      Example: English *stride* lacks a standard past participle. §4.5.1. -/
+  | morphologicalGap
+  /-- A form has no corresponding meaning/function.
+      Example: Romance theme vowels, compound linkers. §4.5.2. -/
+  | emptyMorph
+  deriving DecidableEq, Repr
+
+end Core.Morphology.FormMeaningMapping