@cite{champollion-2017}: Distributivity as a bridge between aspect and measurement

Paper-anchored study for Parts of a Whole. The book unifies four ostensibly disjoint phenomena — predicative distributivity (Ch 4), atelicity (Ch 5–6), and pseudopartitive measurement (Ch 7) — under one higher-order property, stratified reference (SR, Ch 4 §4.6). A distributive construction with Share S, Map M, granularity g describing entity x is acceptable iff SR_{M,g}(S)(x) (Distributivity Constraint, Ch 4 §4.6).

Substrate types SR, SDR, SSR, SMR and the construction abbreviations live in Theories/Semantics/Events/Aspect/Stratified.lean. This file consumes them against English Fragment verbs and stages the empirical data the book argues over.

Main definitions

• DistProfile — per-verb agent/theme distributivity tag bundle; Fragment-level metadata indexed against the substrate VerbDistributivity postulate class.
• DistDatum — empirical collective/distributive judgment record.
• predictsSSR — typological convenience function predicting SSR from a Vendler class. Not Champollion's own diagnostic — see Caveats.

Caveats

• Vendler classes are not Champollion primitives. Champollion Ch 6 explicitly disclaims Vendler classes ("Vendler classes do not appear as primitives in this book"). predictsSSR is a convenience bridge from linglib's Fragment Vendler tags to expected SSR behaviour; the underlying Champollion prediction is the cover/granularity- theoretic SR test.
• Lexical cumulativity is assumed throughout. Per @cite{champollion-2017} §2.7.2, every verb's denotation is cumulative (*[[V]] = [[V]]). This is why SSR_univ → CUM does not hold and the Krifka-CUM contrast cannot be recast as an SR-vs-CUM contrast — see Aspect/Stratified.lean module docstring "Relation to Krifka's CUM/QUA".

TODO

• Push carts contrast (Ch 6 §6.4) — the book's headline empirical case where SR predicts acceptable and Krifka 1998 predicts presupposition failure: John pushed carts all the way to the store for fifty minutes (Champollion's BACK-AND-FORTH scenario, Ch 6 §6.4.1). Sketch ~80 LOC: scenario record, acceptability data, SSR-derived prediction, Krifka-divisive-reference-derived prediction (requires a divisiveReference substrate stub in or referenceable from Studies/Krifka1998.lean), divergence theorem.

• Spatial SR / SR_σ (Ch 6) — Champollion treats SR_σ (dimension = location trace) symmetrically with SR_τ; for fifty meters uses SR_σ. Substrate currently exposes only SSR (temporal). Add SR_σ in Aspect/Stratified.lean (~30 LOC), then exercise here on the road meanders for a mile / the road ends in a mile (~30 LOC).

• SMR consumers (Ch 7 §7.4) — substrate SMR_univ has no consumer. Stage Champollion's Ch 7 measurement-substance contrasts: predicted-acceptable thirty liters of water, five feet of snow, two degrees Celsius of global warming, cool for five degrees; and predicted-failures thirty degrees Celsius of water, five pounds of book. ~60 LOC. The book rejection is via at-issue-meaning + count-noun quantization, not SR — make the distinction explicit.

• Distributivity Constraint as unification (Ch 4 §4.6) — headline theorem: eachConstr, forConstr, pseudopartConstr all reduce to DistConstr. Substrate already supports this; state the three reductions (~5 LOC rfl per construction) plus a packaging corollary. ~25 LOC.

• Lexical cumulativity assumption (§2.7.2) — express as a class LexicallyCumulativeFragment carrying verbIsCumulative : ∀ V ∈ verbs, AlgClosure V = V, with English Fragment supplying the instance. Required for soundness of any theorem that imports the book's for-adverbial entry. ~20 LOC.

• Granularity rescue of waltz (Ch 5 §5.4) — concrete meaning postulate showing waltz has SR_{τ, λt[seconds(t)≤3]}, the only place in the book Champollion uses a numerical threshold. Couple with linglib Time.seconds measure. ~20 LOC.

• Cover / SR equivalence (Ch 5 §5.4) — substrate-bridge theorem *λy[C(y)] x ↔ ∃C' ⊆ C [Cov(C', x)]. Connects Champollion's SR to @cite{schwarzschild-1996} cover semantics. Lives in Aspect/Stratified.lean as a property of AlgClosure; consumed here only if needed for Ch 6 push-carts proof. Substrate ~40 LOC.

• regular predicate in for-adverbial entry (Ch 4) — Champollion's lexical entry includes ... ∧ regular(M(e)) — a condition currently invisible in linglib's forAdverbialMeaning. Either define regular : Interval Time → Prop (~10 LOC substrate) or document why linglib drops it.

• Theorem subjects via substrate predicates — per CLAUDE.md theory-hub denotation discipline: replace seeProfile.agentSDR = true (Bool tag) with statements about SDR_univ agentOf seePred where seePred : Event Time → Prop is derived from Fragment see.semantics. Requires Fragment verbs to expose an Event Time → Prop denotation.

• Convert Bool fields to Prop + [Decidable] per CLAUDE.md "no Bool for predicate-shape data" — affects DistProfile, DistDatum, predictsSSR. ~15 LOC mechanical.

What this file is NOT

• Not a re-statement of substrate primitives. SR, SDR, SSR, SMR live in Aspect/Stratified.lean; this file only consumes them.
• Not a Krifka 1998 vs SR proof harness. The empirical contrast lives in Studies/Krifka1998.lean (sister); the push-carts §6 will live there or be split across both.
• Not a Vendler-class theory anchor. Ch 6 explicitly disclaims Vendler classes; predictsSSR is a Fragment-tagging convenience.

References

• @cite{champollion-2017} (primary; SR machinery + Ch 4–7 empirical cases + §2.7.2 lexical cumulativity stance + Ch 6 vs-Krifka argument)
• @cite{krifka-1998} (the divisive-reference target Champollion argues against in Ch 6; sister: Studies/Krifka1998.lean)
• @cite{schwarzschild-2006} (the monotonic-measure-function predicate Champollion's SMR translates and weakens, Ch 7 §7.3)
• @cite{link-1983} (the algebraic-closure * operator SR builds on)
• @cite{dowty-1979} (the subinterval property SR generalizes, Ch 5)

Distributivity Profiles

structure Champollion2017.DistProfile : Type

Per-verb distributivity profile: whether the verb distributes over atomic agents and/or themes. Mirrors the postulates in VerbDistributivity from Events/Aspect/Stratified.lean.

• verb : String
• agentSDR : Bool
• themeSDR : Bool

def Champollion2017.instReprDistProfile.repr : DistProfile → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Champollion2017.instReprDistProfile : Repr DistProfile

Equations

• Champollion2017.instReprDistProfile = { reprPrec := Champollion2017.instReprDistProfile.repr }

def Champollion2017.instDecidableEqDistProfile.decEq (x✝ x✝¹ : DistProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Champollion2017.instDecidableEqDistProfile : DecidableEq DistProfile

Equations

• Champollion2017.instDecidableEqDistProfile = Champollion2017.instDecidableEqDistProfile.decEq

def Champollion2017.seeProfile : DistProfile

"see" distributes on both agent and theme. "The boys saw the movies" → each boy saw each movie.

Equations

• Champollion2017.seeProfile = { verb := "see", agentSDR := true, themeSDR := true }

def Champollion2017.killProfile : DistProfile

"kill" distributes on theme only. "The boys killed the chicken" → the chicken was killed (by the group).

Equations

• Champollion2017.killProfile = { verb := "kill", agentSDR := false, themeSDR := true }

def Champollion2017.meetProfile : DistProfile

"meet" does NOT distribute on agent (inherently collective). "The boys met" does NOT entail each boy met.

Equations

• Champollion2017.meetProfile = { verb := "meet", agentSDR := false, themeSDR := false }

def Champollion2017.eatProfile : DistProfile

"eat" distributes on agent (each ate something). "The boys ate the pizza" → each boy ate (some) the pizza.

Equations

• Champollion2017.eatProfile = { verb := "eat", agentSDR := true, themeSDR := true }

def Champollion2017.distProfiles : List DistProfile

Equations

• Champollion2017.distProfiles = [Champollion2017.seeProfile, Champollion2017.killProfile, Champollion2017.meetProfile, Champollion2017.eatProfile]

Distributivity Data

structure Champollion2017.DistDatum : Type

Empirical collective/distributive ambiguity judgments.

• sentence : String
• distributiveOK : Bool
• collectiveOK : Bool

def Champollion2017.instReprDistDatum.repr : DistDatum → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Champollion2017.instReprDistDatum : Repr DistDatum

Equations

• Champollion2017.instReprDistDatum = { reprPrec := Champollion2017.instReprDistDatum.repr }

@[implicit_reducible]

instance Champollion2017.instDecidableEqDistDatum : DecidableEq DistDatum

Equations

• Champollion2017.instDecidableEqDistDatum = Champollion2017.instDecidableEqDistDatum.decEq

def Champollion2017.instDecidableEqDistDatum.decEq (x✝ x✝¹ : DistDatum) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Champollion2017.seeDistDatum : DistDatum

Equations

• Champollion2017.seeDistDatum = { sentence := "The boys saw the movie", distributiveOK := true, collectiveOK := true }

def Champollion2017.killDistDatum : DistDatum

Equations

• Champollion2017.killDistDatum = { sentence := "The boys killed the chicken", distributiveOK := false, collectiveOK := true }

def Champollion2017.meetDistDatum : DistDatum

Equations

• Champollion2017.meetDistDatum = { sentence := "The boys met", distributiveOK := false, collectiveOK := true }

def Champollion2017.eatDistDatum : DistDatum

Equations

• Champollion2017.eatDistDatum = { sentence := "The boys ate the pizza", distributiveOK := true, collectiveOK := true }

def Champollion2017.distData : List DistDatum

Equations

• Champollion2017.distData = [Champollion2017.seeDistDatum, Champollion2017.killDistDatum, Champollion2017.meetDistDatum, Champollion2017.eatDistDatum]

Profile → Data Alignment

Verify that the distributivity profiles predict the empirical data: agentSDR = true ↔ distributive reading available.

theorem Champollion2017.profiles_predict_data : seeProfile.agentSDR = seeDistDatum.distributiveOK ∧ killProfile.agentSDR = killDistDatum.distributiveOK ∧ meetProfile.agentSDR = meetDistDatum.distributiveOK ∧ eatProfile.agentSDR = eatDistDatum.distributiveOK

Agent SDR predicts distributive reading availability.

theorem Champollion2017.all_collective_ok : (distData.all fun (d : DistDatum) => d.collectiveOK) = true

All data consistently shows collective reading is available.

VerbDistributivity Postulate Alignment

The VerbDistributivity class from Events/Aspect/Stratified.lean axiomatizes SDR_univ for specific verbs. Verify our profiles match: - see_agent_sdr, see_theme_sdr ↔ seeProfile = (true, true) - kill_theme_sdr, kill_agent_not_sdr ↔ killProfile = (false, true) - meet_agent_not_sdr ↔ meetProfile.agentSDR = false

theorem Champollion2017.see_matches_postulates : seeProfile.agentSDR = true ∧ seeProfile.themeSDR = true

See profile matches VerbDistributivity postulates.

theorem Champollion2017.kill_matches_postulates : killProfile.agentSDR = false ∧ killProfile.themeSDR = true

Kill profile matches VerbDistributivity postulates.

theorem Champollion2017.meet_matches_postulates : meetProfile.agentSDR = false

Meet profile matches VerbDistributivity postulates.

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

Fragment verb entries have the right Vendler class for SDR alignment.

SSR_univ ↔ Vendler Bridge

SSR_univ connects to Vendlerian atelicity via qua_incompatible_with_ssr and forAdverbial_requires_ssr: QUA(P) + SSR_univ P → ⊥ at any P-event, so telic predicates can't have SSR_univ. The atelic Vendler classes (states/activities) are expected to have SSR_univ and to accept for X; the telic classes (achievements/accomplishments) are not and accept in X.

We verify this through the Vendler classification of fragment verbs.
The Bool-valued `predictsSSR` below is the per-class typology
prediction; bridging to the substrate-side `SSR_univ` predicate on
a verb's denotation requires a verb-side `Event Time → Prop` denotation
(theory-hub denotation discipline; follow-up work). 

def Champollion2017.predictsSSR : Option Features.VendlerClass → Bool

Per-verb prediction of SSR_univ based on Vendler class: state / activity → atelic; achievement / accomplishment / semelfactive → not atelic.

Equations

• Champollion2017.predictsSSR (some Features.VendlerClass.state) = true
• Champollion2017.predictsSSR (some Features.VendlerClass.activity) = true
• Champollion2017.predictsSSR (some Features.VendlerClass.achievement) = false
• Champollion2017.predictsSSR (some Features.VendlerClass.accomplishment) = false
• Champollion2017.predictsSSR (some Features.VendlerClass.semelfactive) = false
• Champollion2017.predictsSSR none = false

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

States and activities are atelic → predict SSR → accept "for X".

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

Achievements and accomplishments are telic → no SSR → accept "in X".

theorem Champollion2017.sleep_ssr : predictsSSR Fragments.English.Predicates.Verbal.sleep.vendlerClass = true

"sleep" (state) → SSR expected.

theorem Champollion2017.run_ssr : predictsSSR Fragments.English.Predicates.Verbal.run.vendlerClass = true

"run" (activity) → SSR expected.

theorem Champollion2017.arrive_no_ssr : predictsSSR Fragments.English.Predicates.Verbal.arrive.vendlerClass = false

"arrive" (achievement) → no SSR.

theorem Champollion2017.eat_no_ssr : predictsSSR Fragments.English.Predicates.Verbal.eat.vendlerClass = false

"eat" (accomplishment) → no SSR.

theorem Champollion2017.see_ssr : predictsSSR Fragments.English.Predicates.Verbal.see.vendlerClass = true

"see" (state) → SSR expected.