@cite{filip-2012}: "Lexical Aspect"

Filip's handbook chapter (Binnick ed., OUP) identifies a three-way classification of verb predicates beyond K89/K98's binary CUM/QUA:

1. Telic / quantized (QUA): recover, arrive
2. Atelic / cumulative (CUM): run, push
3. Neither (¬CUM ∧ ¬QUA): build, eat, write — verbs whose telicity is underspecified at the verb level and determined compositionally by the object NP

The third class's compositional behavior:

• QUA object → QUA VP: "eat two apples" (telic)
• CUM object → CUM VP: "eat apples" (atelic)
• ¬CUM ∧ ¬QUA object → ¬CUM ∧ ¬QUA VP: "drink margarita" (Moon's case)

Main definitions

• three_way_exhaustive — Filip's distinctive observation: every predicate is CUM, QUA, or ¬CUM ∧ ¬QUA
• not_cum_vp_of_witnesses — ¬CUM lifts to VP under [IsSincVerb θ]
• middle_ground_stable — ¬CUM ∧ ¬QUA lifts to VP under [IsSincVerb θ] (the propagation-gap stability result; canonical typeclass-form public API consumed by Studies/Moon2026.lean)

TODO

• The propagation-gap substrate (§ 2 below) was inlined from former Theories/Semantics/Events/PropagationGap.lean in 0.231.55 as single-consumer substrate. If a second paper-anchored Studies file consumes middle_ground_stable, lift back to substrate per CLAUDE.md Theories/ ≥ 2 consumers rule.

References

• @cite{filip-2012} (primary)
• @cite{krifka-1998} §3.3 (CUM/QUA propagation machinery the gap rests on)
• @cite{krifka-1989} (the binary CUM/QUA antecedent Filip critiques)
• @cite{moon-2026} (canonical instance: mixed-drink nouns as concrete witness of the topological-source ¬CUM ∧ ¬QUA middle ground)

Three-way exhaustiveness (Filip's distinctive observation)

theorem Filip2012.three_way_exhaustive {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : Mereology.CUM P ∨ Mereology.QUA P ∨ ¬Mereology.CUM P ∧ ¬Mereology.QUA P

The three classes are exhaustive: every predicate falls into exactly one of CUM, QUA, or ¬CUM ∧ ¬QUA. Conceptually important: the middle ground is a genuine third category, not a gap in our analysis.

Propagation gap substrate (inlined)

When OBJ is neither CUM nor QUA, neither cum_propagation nor qua_propagation fires. Under SINC + UP + CumTheta verbs the middle ground is stable — it lifts from OBJ to VP. The concrete witness instance is @cite{moon-2026}'s mixed drink nouns.

theorem Filip2012.not_cum_vp_of_witnesses {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} [Semantics.Aspect.Incremental.IsSincVerb θ] {OBJ : α → Prop} {x y : α} {e₁ e₂ : β} (hx : OBJ x) (hy : OBJ y) (hθ₁ : θ x e₁) (hθ₂ : θ y e₂) (hSum : ¬OBJ (x ⊔ y)) : ¬Mereology.CUM (Semantics.Aspect.Cumulativity.VP θ OBJ)

¬CUM lifts to VP (canonical typeclass form). [IsSincVerb θ] bundles CumTheta (via IsCumThetaVerb parent class) and UP.

theorem Filip2012.middle_ground_stable {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} [Semantics.Aspect.Incremental.IsSincVerb θ] {OBJ : α → Prop} {a b : α} {e_a e_b : β} (ha : OBJ a) (hb : OBJ b) (hθ_a : θ a e_a) (hθ_b : θ b e_b) (hSum : ¬OBJ (a ⊔ b)) {x y : α} {e_x : β} (hx : OBJ x) (hy : OBJ y) (hlt : y < x) (hθ_x : θ x e_x) : ¬Mereology.CUM (Semantics.Aspect.Cumulativity.VP θ OBJ) ∧ ¬Mereology.QUA (Semantics.Aspect.Cumulativity.VP θ OBJ)

Middle-ground gap lifts (canonical typeclass form). [IsSincVerb θ] bundles SINC + UP + CumTheta directly. The recommended public API for the @cite{filip-2012} propositional gap-propagation result.