[Cha17]: Distributivity as a bridge between aspect and measurement

Paper-anchored study for Parts of a Whole, which unifies predicative distributivity (Ch 4), atelicity (Ch 5–6), and pseudopartitive measurement (Ch 7) under one property, stratified reference (Stratified.Reference, Ch 4 §4.6). This file consumes that substrate against English Fragment verbs.

Main definitions

• materializationOfSumHom / LexicallyCumulative / lexicallyCumulative_imp_cum — the §2.5 (thematic roles are sum homomorphisms) and §2.7.2 (lexical cumulativity ⟹ Krifka CUM) algebraic substrate.
• ChampollionPostulates — Champollion's per-verb distributivity meaning postulates (§6.2–6.3), over the Fragment verbs' denotations via Verb.StratifiesOver.
• subintervalReference_iff_cover — atelicity as a Schwarzschild cover ([Cha17] §5.4, his Theorem 14 at the runtime dimension); the genuine consumer of Semantics/Plurality/Cover.lean.

Caveats

• Vendler classes are not Champollion primitives (Ch 6 disclaims them explicitly). The Vendler↔atelicity theorems are a convenience bridge from Fragment Vendler tags to for/in-adverbial acceptability, not Champollion's own diagnostic (the subinterval-reference test).
• Lexical cumulativity is assumed throughout (§2.7.2), which is why SubintervalReferenceUniv → CUM does not hold — see Aspect/Stratified.

§2.5/§2.7.2 algebraic substrate

def Champollion2017.materializationOfSumHom {E : Type u_1} {I : Type u_2} [SemilatticeSup E] [SemilatticeSup I] (f : E → I) [hf : Mereology.IsSumHom f] : Semantics.Plurality.Algebra.Materialization E I

Champollion §2.5: any sum-homomorphism f : Event → α (thematic role or τ runtime) packages into a Materialization (= SupHom E I) via IsSumHom.toSupHom.

Equations

• Champollion2017.materializationOfSumHom f = hf.toSupHom

@[simp]

theorem Champollion2017.materializationOfSumHom_apply {E : Type u_1} {I : Type u_2} [SemilatticeSup E] [SemilatticeSup I] (f : E → I) [Mereology.IsSumHom f] (x : E) : (materializationOfSumHom f) x = f x

def Champollion2017.LexicallyCumulative {α : Type u_3} [SemilatticeSup α] (P : α → Prop) : Prop

Champollion §2.7.2: lexical cumulativity of a predicate — AlgClosure P = P extensionally (P a fixed point of the *-operator).

Equations

• Champollion2017.LexicallyCumulative P = ∀ (x : α), Mereology.AlgClosure P x ↔ P x

theorem Champollion2017.lexicallyCumulative_imp_cum {α : Type u_3} [SemilatticeSup α] {P : α → Prop} (h : LexicallyCumulative P) : Mereology.CUM P

Lexical cumulativity entails Krifka's CUM (closure under binary join).

Distributivity: meaning postulates over Verb.denote (§6.2–6.3)

Champollion's per-verb distributivity facts are lexical meaning postulates, stated over the Fragment verbs' denotations via Verb.StratifiesOver — the Verb-API distributivity property (relational stratified distributive reference of Verb.denote), the substrate-grounded successor to the retired Bool distributivity tags.

structure Champollion2017.ChampollionPostulates {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] [PartialOrder Entity] [SemilatticeSup (Event Time)] (M : Verb.CosModel Entity State Time) (agentRole themeRole : Entity → Event Time → Prop) : Prop

[Cha17]'s verb-distributivity meaning postulates (§6.2–6.3, (19)–(23)), over the Fragment verbs' CosModel denotations and the model's agent/theme role relations: see distributes on both roles, kill on theme only (collective causation blocks the agent), meet on neither (inherently collective). Postulates, not theorems — Champollion stipulates them lexically.

• see_distributes_agent : English.Predicates.Verbal.see.StratifiesOver M agentRole
• see_distributes_theme : English.Predicates.Verbal.see.StratifiesOver M themeRole
• kill_distributes_theme : English.Predicates.Verbal.kill.StratifiesOver M themeRole
• kill_not_distributes_agent : ¬English.Predicates.Verbal.kill.StratifiesOver M agentRole
• meet_not_distributes_agent : ¬English.Predicates.Verbal.meet.StratifiesOver M agentRole

Atelicity as a Schwarzschild cover (§5.4)

theorem Champollion2017.subintervalReference_iff_cover {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Event Time)] [DecidableEq (Event Time)] {P : Event Time → Prop} {e : Event Time} : Semantics.Aspect.Stratified.SubintervalReference P e ↔ ∃ (parts : Finset (Event Time)) (hne : parts.Nonempty), Semantics.Plurality.Cover.IsFinCover parts hne e ∧ ∀ p ∈ parts, P p ∧ p.runtime < e.runtime

[Cha17] §5.4: a predicate P has stratified subinterval reference at e iff e has a finite Schwarzschild cover into proper-subinterval P-parts. The for-adverbial atelicity diagnostic is the existence of such a cover — his Theorem 14 (Cover.algClosure_iff_exists_finCover) at the runtime dimension. The genuine consumer of Semantics/Plurality/Cover.lean.

Vendler ↔ atelicity (convenience bridge, not Champollion's diagnostic)

Champollion Ch 6 disclaims Vendler classes as primitives. These read a Fragment verb's Vendler tag and the textbook for-adverbial / in-adverbial prediction — a convenience for the atelic/telic split, distinct from the subinterval-reference test above.

theorem Champollion2017.fragment_verb_vendler_classes : English.Predicates.Verbal.see.vendlerClass = some Features.VendlerClass.state ∧ English.Predicates.Verbal.kill.vendlerClass = some Features.VendlerClass.accomplishment ∧ English.Predicates.Verbal.meet.vendlerClass = some Features.VendlerClass.achievement ∧ English.Predicates.Verbal.eat.vendlerClass = some Features.VendlerClass.accomplishment

theorem Champollion2017.atelic_classes_accept_forX : Features.forXPrediction Features.VendlerClass.state = Features.DiagnosticResult.accept ∧ Features.forXPrediction Features.VendlerClass.activity = Features.DiagnosticResult.accept

Atelic Vendler classes (states/activities) accept for X.

theorem Champollion2017.telic_classes_accept_inX : Features.inXPrediction Features.VendlerClass.achievement = Features.DiagnosticResult.accept ∧ Features.inXPrediction Features.VendlerClass.accomplishment = Features.DiagnosticResult.accept

Telic Vendler classes (achievements/accomplishments) accept in X.