Stratified Reference: Distributivity → Fragment Verbs

Connects @cite{champollion-2017}'s Stratified Reference theory (Events/StratifiedReference.lean) to concrete verb entries and empirical distributivity/atelicity data.

What it exercises

• SDR, SDR_univ (stratified distributive reference)
• VerbDistributivity (per-verb distributivity postulates)
• SSR, SSR_univ (stratified subinterval reference)
• forAdverbial_requires_ssr (for-adverbials require SSR)
• qua_incompatible_with_ssr (QUA + SSR → ⊥)
• in_adverbial_incompatible_with_ssr (in-adverbials vs SSR)
• sdr_mono (SDR monotonicity)

Structure

1. Distributivity profiles — per-verb agent/theme distributivity
2. Distributivity data — empirical collective/distributive judgments
3. Profile → data alignment — profiles predict empirical data
4. VerbDistributivity postulate alignment — data matches postulates
5. SSR ↔ atelicity bridge — SSR connects to for/in diagnostics

structure Phenomena.Plurals.Studies.Champollion2017.DistProfile : Type

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

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

instance Phenomena.Plurals.Studies.Champollion2017.instReprDistProfile : Repr DistProfile

Equations

• Phenomena.Plurals.Studies.Champollion2017.instReprDistProfile = { reprPrec := Phenomena.Plurals.Studies.Champollion2017.instReprDistProfile.repr }

def Phenomena.Plurals.Studies.Champollion2017.instReprDistProfile.repr : DistProfile → ℕ → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Champollion2017.instDecidableEqDistProfile : DecidableEq DistProfile

Equations

• Phenomena.Plurals.Studies.Champollion2017.instDecidableEqDistProfile = Phenomena.Plurals.Studies.Champollion2017.instDecidableEqDistProfile.decEq

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

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.instBEqDistProfile.beq : DistProfile → DistProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Plurals.Studies.Champollion2017.instBEqDistProfile.beq x✝¹ x✝ = false

instance Phenomena.Plurals.Studies.Champollion2017.instBEqDistProfile : BEq DistProfile

Equations

• Phenomena.Plurals.Studies.Champollion2017.instBEqDistProfile = { beq := Phenomena.Plurals.Studies.Champollion2017.instBEqDistProfile.beq }

def Phenomena.Plurals.Studies.Champollion2017.seeProfile : DistProfile

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

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.killProfile : DistProfile

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

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.meetProfile : DistProfile

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

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.eatProfile : DistProfile

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

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.distProfiles : List DistProfile

Equations

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

structure Phenomena.Plurals.Studies.Champollion2017.DistDatum : Type

Empirical collective/distributive ambiguity judgments.

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

instance Phenomena.Plurals.Studies.Champollion2017.instReprDistDatum : Repr DistDatum

Equations

• Phenomena.Plurals.Studies.Champollion2017.instReprDistDatum = { reprPrec := Phenomena.Plurals.Studies.Champollion2017.instReprDistDatum.repr }

def Phenomena.Plurals.Studies.Champollion2017.instReprDistDatum.repr : DistDatum → ℕ → Std.Format

Equations

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

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

Equations

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

instance Phenomena.Plurals.Studies.Champollion2017.instDecidableEqDistDatum : DecidableEq DistDatum

Equations

• Phenomena.Plurals.Studies.Champollion2017.instDecidableEqDistDatum = Phenomena.Plurals.Studies.Champollion2017.instDecidableEqDistDatum.decEq

def Phenomena.Plurals.Studies.Champollion2017.instBEqDistDatum.beq : DistDatum → DistDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Plurals.Studies.Champollion2017.instBEqDistDatum.beq x✝¹ x✝ = false

instance Phenomena.Plurals.Studies.Champollion2017.instBEqDistDatum : BEq DistDatum

Equations

• Phenomena.Plurals.Studies.Champollion2017.instBEqDistDatum = { beq := Phenomena.Plurals.Studies.Champollion2017.instBEqDistDatum.beq }

def Phenomena.Plurals.Studies.Champollion2017.seeDistDatum : DistDatum

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.killDistDatum : DistDatum

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.meetDistDatum : DistDatum

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.eatDistDatum : DistDatum

Equations

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

def Phenomena.Plurals.Studies.Champollion2017.distData : List DistDatum

Equations

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

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Champollion2017.all_collective_ok : (distData.all fun (d : DistDatum) => d.collectiveOK) = true

All data consistently shows collective reading is available.

The VerbDistributivity class from Events/StratifiedReference.lean axiomatizes SDR 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 Phenomena.Plurals.Studies.Champollion2017.see_matches_postulates : seeProfile.agentSDR = true ∧ seeProfile.themeSDR = true

See profile matches VerbDistributivity postulates.

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

Kill profile matches VerbDistributivity postulates.

theorem Phenomena.Plurals.Studies.Champollion2017.meet_matches_postulates : meetProfile.agentSDR = false

Meet profile matches VerbDistributivity postulates.

theorem Phenomena.Plurals.Studies.Champollion2017.verb_vendler_for_sdr : Fragments.English.Predicates.Verbal.see.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state ∧ Fragments.English.Predicates.Verbal.kill.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.meet.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ Fragments.English.Predicates.Verbal.eat.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

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

SSR (Stratified Subinterval Reference) connects to atelicity via qua_incompatible_with_ssr and forAdverbial_requires_ssr. QUA(P) + SSR(P)(e) + P(e) → ⊥, so telic predicates can't have SSR. Atelic predicates (states/activities) have SSR → accept "for X".

We verify this through the Vendler classification of fragment verbs. 

def Phenomena.Plurals.Studies.Champollion2017.predictsSSR : Option Semantics.Tense.Aspect.LexicalAspect.VendlerClass → Bool

Per-verb SSR prediction based on Vendler class: state/activity → SSR expected (atelic); achievement/accomplishment → no SSR.

Equations

• Phenomena.Plurals.Studies.Champollion2017.predictsSSR (some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state) = true
• Phenomena.Plurals.Studies.Champollion2017.predictsSSR (some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity) = true
• Phenomena.Plurals.Studies.Champollion2017.predictsSSR (some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement) = false
• Phenomena.Plurals.Studies.Champollion2017.predictsSSR (some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment) = false
• Phenomena.Plurals.Studies.Champollion2017.predictsSSR none = false

theorem Phenomena.Plurals.Studies.Champollion2017.atelic_classes_accept_forX : TenseAspect.Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = TenseAspect.Diagnostics.DiagnosticResult.accept ∧ TenseAspect.Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = TenseAspect.Diagnostics.DiagnosticResult.accept

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

theorem Phenomena.Plurals.Studies.Champollion2017.telic_classes_accept_inX : TenseAspect.Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = TenseAspect.Diagnostics.DiagnosticResult.accept ∧ TenseAspect.Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = TenseAspect.Diagnostics.DiagnosticResult.accept

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

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

"sleep" (state) → SSR expected.

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

"run" (activity) → SSR expected.

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

"arrive" (achievement) → no SSR.

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

"eat" (accomplishment) → no SSR.

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

"see" (state) → SSR expected.