Atomic distributivity

@cite{champollion-2015} @cite{zhao-2025}

AtomDist is the event-quantifier-level form of @cite{zhao-2025}'s ATOM-DIST_t (Def. 5.36, p. 165): an event quantifier V satisfies ATOM-DIST with respect to a trace τ iff whenever it applies to an event property fixing the trace as i, it also applies to the property fixing the trace as any subinterval i' of i.

Per the strata-theory unification (@cite{champollion-2017}), this is the quantifier-level form of stratified reference at point-interval granularity along the time dimension — a sibling of the Bennett-Partee 1972 strict subinterval property (HasSubintervalProp in Theories/Semantics/Tense/Aspect/SubintervalProperty.lean). The bridge EvQuant.ofPred below lifts an event predicate to an event quantifier; the witness-universal and quantifier-restriction formulations live at the same parameter-space point but differ in quantification structure and are not directly interderivable without explicit witness-existence assumptions.

The antiAtomDistLicensed predicate is the licensing condition for Mandarin perfective particles in @cite{zhao-2025} (le, méi-yǒu).

@[reducible, inline]

abbrev Core.Time.EvQuant (Event : Type u_1) : Type u_1

An event quantifier: a predicate on event predicates. V(P) holds iff "there is an event satisfying P" according to V's quantificational force. The Champollion 2015 typed shape.

Equations

• Core.Time.EvQuant Event = ((Event → Prop) → Prop)

def Core.Time.AtomDist {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Interval α) (V : EvQuant Event) : Prop

ATOM-DIST_α (@cite{zhao-2025} Def. 5.36, p. 165): an event quantifier V satisfies ATOM-DIST with respect to trace function τ iff for every event predicate P and subinterval i' of τ(e), V also holds for the restriction of P to events whose trace is i'.

Formally: V(P) → ∀ e, P(e) → ∀ i', subinterval(i', τ(e)) → V(λ e'. P(e') ∧ τ(e') = i')

This captures the subinterval property parameterized over any linearly ordered dimension α (Zhao §5.5 extends to space; the cross-domain hypothesis is that the same definition applies to any [LinearOrder α]).

Equations

• Core.Time.AtomDist τ V = ∀ (P : Event → Prop), V P → ∀ (e : Event), P e → ∀ (i' : Core.Time.Interval α), i'.subinterval (τ e) → V fun (e' : Event) => P e' ∧ τ e' = i'

def Core.Time.antiAtomDistLicensed {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Interval α) (V : EvQuant Event) : Prop

NOT-ATOM-DIST_α licensing condition: A particle is licensed by an event quantifier V (w.r.t. trace τ) iff V does NOT satisfy ATOM-DIST_α. This is the presupposition of Mandarin le and méi-yǒu (@cite{zhao-2025} eq. 5.42).

Equations

• Core.Time.antiAtomDistLicensed τ V = ¬Core.Time.AtomDist τ V

def Core.Time.EvQuant.ofPred {Event : Type u_1} (P : Event → Prop) : EvQuant Event

Existential lift of an event predicate to an event quantifier: λf. ∃e, P e ∧ f e. The standard way (per @cite{champollion-2015}) to view a verb's predicate denotation as an event quantifier; used to bridge the predicate-level strata theory (SR_univ etc.) to the quantifier-level AtomDist.

Equations

• Core.Time.EvQuant.ofPred P f = ∃ (e : Event), P e ∧ f e

@[simp]

theorem Core.Time.EvQuant.ofPred_apply {Event : Type u_1} (P f : Event → Prop) : ofPred P f ↔ ∃ (e : Event), P e ∧ f e