def Semantics.Events.StratifiedReference.SR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (d : α → β) (g : β → Prop) (P : α → Prop) (x : α) : Prop

Stratified Reference: the core unified property from @cite{champollion-2017} eq. (62). SR_{d,g}(P)(x) holds iff x can be decomposed into P-parts whose images under dimension d satisfy granularity g.

• d : α → β — the dimension (e.g., thematic role θ, runtime τ, measure μ)
• g : β → Prop — the granularity (e.g., Atom, properSubinterval, smaller)
• P : α → Prop — the predicate under scrutiny
• x : α — the entity/event being decomposed

SR_{d,g}(P)(x) = *{y : P(y) ∧ g(d(y))}(x)

Equations

• Semantics.Events.StratifiedReference.SR d g P x = Mereology.AlgClosure (fun (y : α) => P y ∧ g (d y)) x

def Semantics.Events.StratifiedReference.SR_univ {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (d : α → β) (g : β → Prop) (P : α → Prop) : Prop

Universal Stratified Reference: every P-entity has SR. eq. (63): SR_{d,g}(P) = ∀x. P(x) → SR_{d,g}(P)(x). When this holds, P is "stratified" along dimension d at granularity g.

Equations

• Semantics.Events.StratifiedReference.SR_univ d g P = ∀ (x : α), P x → Semantics.Events.StratifiedReference.SR d g P x

def Semantics.Events.StratifiedReference.SDR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] (θ : α → β) (P : α → Prop) (x : α) : Prop

Stratified Distributive Reference: dimension is a thematic role θ, granularity is Atom. SDR_{θ}(P)(e) holds iff e can be decomposed into P-parts whose θ-fillers are atoms (individuals). eq. (24)/(59).

SDR captures distributivity: "The boys each saw a movie" distributes over atomic agents.

Equations

• Semantics.Events.StratifiedReference.SDR θ P x = Semantics.Events.StratifiedReference.SR θ Mereology.Atom P x

def Semantics.Events.StratifiedReference.SDR_univ {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] (θ : α → β) (P : α → Prop) : Prop

Universal SDR: every P-entity has SDR along θ.

Equations

• Semantics.Events.StratifiedReference.SDR_univ θ P = ∀ (x : α), P x → Semantics.Events.StratifiedReference.SDR θ P x

def Semantics.Events.StratifiedReference.SSRGranularity {Time : Type u_1} [LinearOrder Time] (outer inner : Ev Time) : Prop

Proper subinterval granularity relative to a fixed outer event e. Used by SSR: the runtime of each part must be a proper subinterval of the runtime of the whole. eq. (38)/(60).

Equations

• Semantics.Events.StratifiedReference.SSRGranularity outer inner = inner.runtime.properSubinterval outer.runtime

def Semantics.Events.StratifiedReference.SSR {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] (P : Ev Time → Prop) (e : Ev Time) : Prop

Stratified Subinterval Reference: dimension is τ (runtime), granularity requires proper subinterval of the outer event's runtime. SSR(P)(e) holds iff e can be built from P-parts with strictly smaller runtimes. eq. (38)/(60).

SSR captures atelicity: predicates compatible with "for"-adverbials have SSR. "John ran for an hour" → run has SSR.

Equations

• Semantics.Events.StratifiedReference.SSR P e = Mereology.AlgClosure (fun (e' : Semantics.Events.Ev Time) => P e' ∧ Semantics.Events.StratifiedReference.SSRGranularity e e') e

def Semantics.Events.StratifiedReference.SSR_univ {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] (P : Ev Time → Prop) : Prop

Universal SSR: every P-event has SSR.

Equations

• Semantics.Events.StratifiedReference.SSR_univ P = ∀ (e : Semantics.Events.Ev Time), P e → Semantics.Events.StratifiedReference.SSR P e

def Semantics.Events.StratifiedReference.SMR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [Preorder β] (μ : α → β) (P : α → Prop) (x : α) : Prop

Stratified Measurement Reference: dimension is a measure function μ, granularity requires strictly smaller measure value. SMR_{μ}(P)(x) holds iff x can be decomposed into P-parts with strictly smaller μ-values. eq. (53)/(61).

SMR captures measurement: "three pounds of apples" has SMR along the weight measure.

Equations

• Semantics.Events.StratifiedReference.SMR μ P x = Mereology.AlgClosure (fun (y : α) => P y ∧ μ y < μ x) x

def Semantics.Events.StratifiedReference.SMR_univ {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [Preorder β] (μ : α → β) (P : α → Prop) : Prop

Universal SMR: every P-entity has SMR along μ.

Equations

• Semantics.Events.StratifiedReference.SMR_univ μ P = ∀ (x : α), P x → Semantics.Events.StratifiedReference.SMR μ P x

@[reducible, inline]

abbrev Semantics.Events.StratifiedReference.DistConstr {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (Map : α → β) (gran : β → Prop) (Share : α → Prop) (x : α) : Prop

Champollion's unified distributivity constraint (eq. 68): DistConstr_{Map, gran}(Share)(x) = SR_{Map, gran}(Share)(x). The three parameters—Map, granularity, and Share—are instantiated differently by each construction (each, for-adverbials, etc.).

Equations

• Semantics.Events.StratifiedReference.DistConstr Map gran Share x = Semantics.Events.StratifiedReference.SR Map gran Share x

@[reducible, inline]

abbrev Semantics.Events.StratifiedReference.eachConstr {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] (θ : α → β) (Share : α → Prop) (x : α) : Prop

"each" distributes over atomic θ-fillers. Map = θ (thematic role), granularity = Atom. §6.4.

Equations

• Semantics.Events.StratifiedReference.eachConstr θ Share x = Semantics.Events.StratifiedReference.SDR θ Share x

@[reducible, inline]

abbrev Semantics.Events.StratifiedReference.forConstr {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] (Share : Ev Time → Prop) (e : Ev Time) : Prop

"for"-adverbials require SSR: the predicate must have stratified subinterval reference (atelicity). Map = τ, granularity = proper subinterval. §5.3.

Equations

• Semantics.Events.StratifiedReference.forConstr Share e = Semantics.Events.StratifiedReference.SSR Share e

theorem Semantics.Events.StratifiedReference.sr_univ_entails_restricted {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {d : α → β} {g : β → Prop} {P : α → Prop} (h : SR_univ d g P) {x : α} (hx : P x) : SR d g P x

SR_univ entails SR for any specific element (instantiation). eq. (32): universal → restricted.

theorem Semantics.Events.StratifiedReference.cum_implies_sr_trivial_gran {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {d : α → β} {P : α → Prop} (hCum : Mereology.CUM P) : SR_univ d (fun (x : β) => True) P

CUM predicates have SR for trivial granularity (everything passes). If P is CUM and g is always true, then SR_{d,g}(P) holds universally.

theorem Semantics.Events.StratifiedReference.sdr_mono {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] {θ : α → β} {P Q : α → Prop} (h : ∀ (x : α), P x → Q x) (x : α) : SDR θ P x → SDR θ Q x

SDR is monotone in the predicate: P ⊆ Q implies SDR θ P ⊆ SDR θ Q.

class Semantics.Events.StratifiedReference.VerbDistributivity (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] [SemilatticeSup (Ev Time)] [PartialOrder Entity] (agentOf themeOf : Ev Time → Entity) (see kill meet : Ev Time → Prop) : Prop

Meaning postulates for verb distributivity (§6.2–6.3). These encode which verbs have SDR along which roles.

• see is distributive on both agent and theme: "The boys saw the girls" entails each boy saw each girl (distributive reading).
• kill is distributive on theme only: "The boys killed the chicken" entails the chicken was killed (by the group).
• meet is NOT distributive on agent: "The boys met" does NOT entail each boy met (collective only).

These are axiomatized following the CLAUDE.md convention: prefer sorry over weakening, since the proofs require model-theoretic content.

• see_agent_sdr : SDR_univ agentOf see

  "see" has SDR along the agent role.

• see_theme_sdr : SDR_univ themeOf see

  "see" has SDR along the theme role.

• kill_theme_sdr : SDR_univ themeOf kill

  "kill" has SDR along the theme role.

• kill_agent_not_sdr : ¬SDR_univ agentOf kill

  "kill" does NOT have SDR along the agent role (collective causation). §6.3: group agents can collectively cause death.

• meet_agent_not_sdr : ¬SDR_univ agentOf meet

  "meet" does NOT have SDR along the agent role (inherently collective). §6.3: meeting requires multiple participants.

theorem Semantics.Events.StratifiedReference.forAdverbial_requires_ssr {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] {P : Ev Time → Prop} (h_for_ok : SSR_univ P) (e : Ev Time) : P e → SSR P e

for-adverbials require SSR (§5.3, eq. 39/66). "John ran for an hour" is felicitous because "run" has SSR. "* John arrived for an hour" is infelicitous because "arrive" lacks SSR.

theorem Semantics.Events.StratifiedReference.qua_incompatible_with_ssr {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] {P : Ev Time → Prop} (hQua : Mereology.QUA P) {e : Ev Time} (he : P e) (hSSR : SSR P e) : False

QUA and SSR are directly incompatible: if P(e) and SSR(P)(e) hold, then P cannot be quantized. The AlgClosure decomposition yields a base element a with P(a) and a.runtime ⊂ e.runtime. Since a ≤ e (from the join structure) and a ≠ e (properSubinterval is irreflexive), we get a < e, contradicting QUA.

This is strictly stronger than the route through CUM (§4.4), which would require additional mereological axioms (SSR_univ → CUM is false in general: P = "events with runtime length ≤ 1" has SSR_univ but not CUM over dense time).

def Semantics.Events.StratifiedReference.forAdverbialMeaning {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] (V : Ev Time → Prop) (duration : Core.Time.Interval Time) (e : Ev Time) : Prop

The "for"-adverbial adds a duration constraint on the event runtime and requires the predicate to have SSR (eq. 39). "V for δ" = λe. V(e) ∧ τ(e) = δ ∧ SSR(V)(e).

Equations

• Semantics.Events.StratifiedReference.forAdverbialMeaning V duration e = (V e ∧ e.runtime = duration ∧ Semantics.Events.StratifiedReference.SSR V e)

theorem Semantics.Events.StratifiedReference.in_adverbial_incompatible_with_ssr {Time : Type u_1} [LinearOrder Time] [SemilatticeSup (Ev Time)] {P : Ev Time → Prop} (hQua : Mereology.QUA P) {e₁ e₂ : Ev Time} (he₁ : P e₁) (_he₂ : P e₂) (_hne : e₁ ≠ e₂) : ¬SSR_univ P

"in"-adverbials are incompatible with SSR (they require telicity). §5.4: "V in δ" requires QUA, which is incompatible with SSR. Any P-event with SSR has a strict P-part, contradicting QUA.