Mandarin Cross-Domain Particles @cite{zhao-2025}

Lexical entries for Mandarin le, guo, and mei-you with cross-domain behavior. These particles operate across temporal and degree domains:

Particle	Temporal gloss	Degree gloss	Licensing
了 le	perfective	exceed-threshold	NOT-ATOM-DIST_α
没有 mei-you	neg-perfective	not-exceed	NOT-ATOM-DIST_α
过 guo	experiential	—	(none)

le and mei-you presuppose NOT-ATOM-DIST_α, explaining their incompatibility with statives (temporal domain) and bare comparatives (degree domain). guo has no such presupposition.

Cross-Module Connections

• Core.Time: ATOM-DIST and antiAtomDistLicensed
• Fragments.Mandarin.Particles: existing Mandarin particle pattern

inductive Fragments.Mandarin.AspectComparison.SemanticDomain : Type

Semantic domain for cross-domain particles.

• temporal : SemanticDomain
• degree : SemanticDomain

instance Fragments.Mandarin.AspectComparison.instDecidableEqSemanticDomain : DecidableEq SemanticDomain

Equations

• Fragments.Mandarin.AspectComparison.instDecidableEqSemanticDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mandarin.AspectComparison.instReprSemanticDomain.repr : SemanticDomain → ℕ → Std.Format

Equations

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

instance Fragments.Mandarin.AspectComparison.instReprSemanticDomain : Repr SemanticDomain

Equations

• Fragments.Mandarin.AspectComparison.instReprSemanticDomain = { reprPrec := Fragments.Mandarin.AspectComparison.instReprSemanticDomain.repr }

instance Fragments.Mandarin.AspectComparison.instBEqSemanticDomain : BEq SemanticDomain

Equations

• Fragments.Mandarin.AspectComparison.instBEqSemanticDomain = { beq := Fragments.Mandarin.AspectComparison.instBEqSemanticDomain.beq }

def Fragments.Mandarin.AspectComparison.instBEqSemanticDomain.beq : SemanticDomain → SemanticDomain → Bool

Equations

• Fragments.Mandarin.AspectComparison.instBEqSemanticDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Fragments.Mandarin.AspectComparison.CrossDomainParticle : Type

A cross-domain particle entry. Encodes the particle's surface form, its temporal and degree glosses, and whether it requires NOT-ATOM-DIST_α licensing.

• hanzi : String

  Chinese character(s)

• pinyin : String

  Pinyin romanization

• temporalGloss : String

  Gloss in temporal domain

• degreeGloss : Option String

  Gloss in degree domain (if applicable)

• requiresAntiAtomDist : Bool

  Whether the particle presupposes NOT-ATOM-DIST_α

def Fragments.Mandarin.AspectComparison.instReprCrossDomainParticle.repr : CrossDomainParticle → ℕ → Std.Format

Equations

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

instance Fragments.Mandarin.AspectComparison.instReprCrossDomainParticle : Repr CrossDomainParticle

Equations

• Fragments.Mandarin.AspectComparison.instReprCrossDomainParticle = { reprPrec := Fragments.Mandarin.AspectComparison.instReprCrossDomainParticle.repr }

def Fragments.Mandarin.AspectComparison.le : CrossDomainParticle

了 le — perfective / exceed-threshold. Presupposes NOT-ATOM-DIST_α in both domains.

Equations

• Fragments.Mandarin.AspectComparison.le = { hanzi := "了", pinyin := "le", temporalGloss := "perfective", degreeGloss := some "exceed-threshold", requiresAntiAtomDist := true }

def Fragments.Mandarin.AspectComparison.meiyou : CrossDomainParticle

没有 mei-you — negative perfective / not-exceed. Presupposes NOT-ATOM-DIST_α.

Equations

• Fragments.Mandarin.AspectComparison.meiyou = { hanzi := "没有", pinyin := "méi-yǒu", temporalGloss := "negative perfective", degreeGloss := some "not-exceed", requiresAntiAtomDist := true }

def Fragments.Mandarin.AspectComparison.guo : CrossDomainParticle

过 guo — experiential aspect. No NOT-ATOM-DIST_α presupposition.

Equations

• Fragments.Mandarin.AspectComparison.guo = { hanzi := "过", pinyin := "guò", temporalGloss := "experiential", degreeGloss := none, requiresAntiAtomDist := false }

def Fragments.Mandarin.AspectComparison.isLicensed {Event : Type u_1} {α : Type u_2} [LinearOrder α] (p : CrossDomainParticle) (τ : Event → Core.Time.Interval α) (V : Core.Time.EvQuant Event) : Prop

Is a particle licensed by an event quantifier V (w.r.t. trace τ)? Licensed iff either (a) the particle doesn't require anti-ATOM-DIST, or (b) V fails ATOM-DIST_α.

Equations

• Fragments.Mandarin.AspectComparison.isLicensed p τ V = (p.requiresAntiAtomDist = false ∨ Core.Time.antiAtomDistLicensed τ V)

theorem Fragments.Mandarin.AspectComparison.le_requires_antiAtomDist : le.requiresAntiAtomDist = true

le requires NOT-ATOM-DIST_α.

theorem Fragments.Mandarin.AspectComparison.meiyou_requires_antiAtomDist : meiyou.requiresAntiAtomDist = true

mei-you requires NOT-ATOM-DIST_α.

theorem Fragments.Mandarin.AspectComparison.guo_no_antiAtomDist : guo.requiresAntiAtomDist = false

guo does NOT require NOT-ATOM-DIST_α.

theorem Fragments.Mandarin.AspectComparison.le_licensed_iff {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Core.Time.Interval α) (V : Core.Time.EvQuant Event) : isLicensed le τ V ↔ Core.Time.antiAtomDistLicensed τ V

le is licensed iff NOT-ATOM-DIST_α holds.

theorem Fragments.Mandarin.AspectComparison.meiyou_licensed_iff {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Core.Time.Interval α) (V : Core.Time.EvQuant Event) : isLicensed meiyou τ V ↔ Core.Time.antiAtomDistLicensed τ V

mei-you is licensed iff NOT-ATOM-DIST_α holds.

theorem Fragments.Mandarin.AspectComparison.guo_always_licensed {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Core.Time.Interval α) (V : Core.Time.EvQuant Event) : isLicensed guo τ V

guo is always licensed (no anti-ATOM-DIST requirement).