Cross-Domain Bridge: VendlerClass ↔ Mandarin Particles

@cite{zhao-2025}

Bridges VendlerClass ATOM-DIST predictions (from Theories/) to the Mandarin cross-domain particle entries (from Fragments/).

The core classification (predictsAtomDist, predictsAtomDist_iff_stative, etc.) lives in Theories/Semantics/Lexical/Verb/Aspect.lean alongside the other VendlerClass feature functions. This file connects those predictions to the Fragment-level particle licensing.

theorem Phenomena.TenseAspect.CrossDomainBridge.le_temporal_licensed_iff_dynamic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : c.predictsAtomDist = false ↔ Fragments.Mandarin.AspectComparison.le.requiresAntiAtomDist = true ∧ c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

le is temporally licensed for a VendlerClass iff the class is dynamic: states predict ATOM-DIST_t → le NOT licensed; dynamic classes predict ¬ATOM-DIST_t → le licensed.

Connects VendlerClass.predictsAtomDist (Theories/) to CrossDomainParticle.requiresAntiAtomDist (Fragments/).

theorem Phenomena.TenseAspect.CrossDomainBridge.meiyou_temporal_licensed_iff_dynamic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : c.predictsAtomDist = false ↔ Fragments.Mandarin.AspectComparison.meiyou.requiresAntiAtomDist = true ∧ c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

meiyou has the same licensing pattern as le.

theorem Phenomena.TenseAspect.CrossDomainBridge.guo_compatible_with_all : Fragments.Mandarin.AspectComparison.guo.requiresAntiAtomDist = false

guo imposes no ATOM-DIST restriction, so it is compatible with all VendlerClasses including states.