Spatial Trace Bridge: Path Telicity → Fragment Verbs

Connects the spatial dimension theory (Events/SpatialTrace.lean, Events/DimensionBridge.lean) to concrete motion verb entries in Fragments/English/Predicates/Verbal.lean and telicity diagnostics.

What it exercises

• pathShapeToTelicity (PathShape → Telicity)
• LevinClass.pathSpec (verb → path specification)
• LicensingPipeline PathShape (bounded → licensed, unbounded → blocked)
• telicity_boundedness_agree (PathShape telicity ↔ boundedness licensing)

Structure

1. Per-verb path specification — verify levinClass.pathSpec for motion verbs
2. PathShape → Telicity → Licensing pipeline — full chain verification
3. Motion VP telicity data — verb + PP pairs with path shapes
4. Diagnostic bridge — connect path telicity to for/in compatibility

Each motion verb's levinClass and pathSpec annotation is verified by rfl. Changing any annotation breaks exactly one theorem here.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.arrive_levinClass : Fragments.English.Predicates.Verbal.arrive.levinClass = some LevinClass.inherentlyDirectedMotion

"arrive" is inherently directed motion.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.arrive_pathSpec : LevinClass.inherentlyDirectedMotion.pathSpec = some Core.Path.PathShape.bounded

Inherently directed motion → bounded path.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.leave_levinClass : Fragments.English.Predicates.Verbal.leave.levinClass = some LevinClass.leave

"leave" is a leave verb.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.leave_pathSpec : LevinClass.leave.pathSpec = some Core.Path.PathShape.source

Leave verbs → source path.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.run_levinClass : Fragments.English.Predicates.Verbal.run.levinClass = some LevinClass.mannerOfMotion

"run" is manner-of-motion.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.run_pathSpec : LevinClass.mannerOfMotion.pathSpec = none

Manner-of-motion verbs are path-neutral (path from PP).

The full chain from PathShape through Telicity to licensing is verified for all three shapes. The LicensingPipeline instance for PathShape is in DimensionBridge.lean.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.bounded_pipeline : Semantics.Events.SpatialTrace.pathShapeToTelicity Core.Path.PathShape.bounded = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic ∧ Core.Scale.LicensingPipeline.isLicensed Core.Path.PathShape.bounded = true

Bounded path → telic → QUA → closed → licensed.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.source_pipeline : Semantics.Events.SpatialTrace.pathShapeToTelicity Core.Path.PathShape.source = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic ∧ Core.Scale.LicensingPipeline.isLicensed Core.Path.PathShape.source = true

Source path → telic → QUA → closed → licensed.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.unbounded_pipeline : Semantics.Events.SpatialTrace.pathShapeToTelicity Core.Path.PathShape.unbounded = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic ∧ Core.Scale.LicensingPipeline.isLicensed Core.Path.PathShape.unbounded = false

Unbounded path → atelic → CUM → open → blocked.

structure Phenomena.TenseAspect.Studies.SpatialTrace.MotionVPDatum : Type

A motion VP datum: verb + PP + path shape + expected telicity.

• verb : String
• pp : String
• pathShape : Core.Path.PathShape
• expectedTelicity : Semantics.Tense.Aspect.LexicalAspect.Telicity

instance Phenomena.TenseAspect.Studies.SpatialTrace.instReprMotionVPDatum : Repr MotionVPDatum

Equations

• Phenomena.TenseAspect.Studies.SpatialTrace.instReprMotionVPDatum = { reprPrec := Phenomena.TenseAspect.Studies.SpatialTrace.instReprMotionVPDatum.repr }

def Phenomena.TenseAspect.Studies.SpatialTrace.instReprMotionVPDatum.repr : MotionVPDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.SpatialTrace.instDecidableEqMotionVPDatum : DecidableEq MotionVPDatum

Equations

• Phenomena.TenseAspect.Studies.SpatialTrace.instDecidableEqMotionVPDatum = Phenomena.TenseAspect.Studies.SpatialTrace.instDecidableEqMotionVPDatum.decEq

def Phenomena.TenseAspect.Studies.SpatialTrace.instDecidableEqMotionVPDatum.decEq (x✝ x✝¹ : MotionVPDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.TenseAspect.Studies.SpatialTrace.instBEqMotionVPDatum.beq : MotionVPDatum → MotionVPDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Studies.SpatialTrace.instBEqMotionVPDatum.beq x✝¹ x✝ = false

instance Phenomena.TenseAspect.Studies.SpatialTrace.instBEqMotionVPDatum : BEq MotionVPDatum

Equations

• Phenomena.TenseAspect.Studies.SpatialTrace.instBEqMotionVPDatum = { beq := Phenomena.TenseAspect.Studies.SpatialTrace.instBEqMotionVPDatum.beq }

def Phenomena.TenseAspect.Studies.SpatialTrace.arriveAtStore : MotionVPDatum

"arrive at the store" — inherently bounded → telic → "in X" ✓

Equations

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

def Phenomena.TenseAspect.Studies.SpatialTrace.leaveTheHouse : MotionVPDatum

"leave the house" — source → telic → "in X" ✓

Equations

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

def Phenomena.TenseAspect.Studies.SpatialTrace.runToThePark : MotionVPDatum

"run to the park" — manner + bounded PP → telic → "in X" ✓

Equations

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

def Phenomena.TenseAspect.Studies.SpatialTrace.runTowardsThePark : MotionVPDatum

"run towards the park" — manner + unbounded PP → atelic → "for X" ✓

Equations

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

def Phenomena.TenseAspect.Studies.SpatialTrace.motionData : List MotionVPDatum

Equations

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

theorem Phenomena.TenseAspect.Studies.SpatialTrace.all_motion_data_correct : (motionData.all fun (d : MotionVPDatum) => Semantics.Events.SpatialTrace.pathShapeToTelicity d.pathShape == d.expectedTelicity) = true

Path shape determines telicity for all motion data.

Connect path telicity to for/in adverbial compatibility. Since diagnostics are defined on VendlerClass, we bridge through the Vendler classification of motion verbs.

theorem Phenomena.TenseAspect.Studies.SpatialTrace.arrive_inX : Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Diagnostics.DiagnosticResult.accept

"arrive" (achievement, bounded path) licenses "in X".

theorem Phenomena.TenseAspect.Studies.SpatialTrace.leave_inX : Fragments.English.Predicates.Verbal.leave.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Diagnostics.DiagnosticResult.accept

"leave" (achievement, source path) licenses "in X".

theorem Phenomena.TenseAspect.Studies.SpatialTrace.run_forX : Fragments.English.Predicates.Verbal.run.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Diagnostics.DiagnosticResult.accept

"run" (activity, path-neutral) licenses "for X".

theorem Phenomena.TenseAspect.Studies.SpatialTrace.motion_vendler_path_coherence : (Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ LevinClass.inherentlyDirectedMotion.pathSpec = some Core.Path.PathShape.bounded) ∧ (Fragments.English.Predicates.Verbal.leave.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ LevinClass.leave.pathSpec = some Core.Path.PathShape.source) ∧ Fragments.English.Predicates.Verbal.run.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ LevinClass.mannerOfMotion.pathSpec = none

Motion verb Vendler class × path shape coherence: bounded-path motion verbs are achievements, path-neutral ones are activities.