Spatial Path Infrastructure

@cite{gawron-2009} @cite{talmy-2000} @cite{zwarts-2005} @cite{zwarts-winter-2000}

Framework-agnostic types for spatial paths and their boundedness classification. Paths are the spatial analog of temporal intervals (Core.Time.Interval): directed stretches of space between locations.

The key linguistic insight: the boundedness of a directional PP determines whether the VP it creates is telic or atelic. Bounded PPs ("to the store") yield telic VPs; unbounded PPs ("towards the store") yield atelic VPs. This parallels the QUA/CUM mereological classification from Core/Mereology.lean.

Sections

1. Path Type
2. Path Shape (Boundedness Classification)
3. PathShape ↔ Scale Boundedness Bridge

structure Core.Path.Path (Loc : Type u_1) : Type u_1

Spatial path: a directed trajectory between locations. @cite{zwarts-2005}: paths are directed stretches of space with a source (starting point) and goal (endpoint).

Parallels Core.Time.Interval for the temporal domain. Unlike intervals, paths have no valid : source ≤ goal constraint because spatial locations lack a canonical linear ordering.

• source : Loc

  Starting location of the path.

• goal : Loc

  Ending location of the path.

inductive Core.Path.PathShape : Type

Directional PP boundedness classification. @cite{zwarts-2005}: the boundedness of a directional PP determines whether the VP it creates is telic or atelic.

• bounded: goal-oriented ("to the store", "into the room")
• unbounded: direction-oriented ("towards the store", "along the road")
• source: origin-oriented ("from the store", "out of the room")

This classifies the set of paths denoted by a PP, not individual paths. "To X" denotes {p | p.goal = X} — a QUA set (no proper subpath of a to-X path is also to-X). "Towards X" denotes a CUM set (concatenating two towards-X paths gives another).

• bounded : PathShape
• unbounded : PathShape
• source : PathShape

instance Core.Path.instDecidableEqPathShape : DecidableEq PathShape

Equations

• Core.Path.instDecidableEqPathShape x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Path.instBEqPathShape : BEq PathShape

Equations

• Core.Path.instBEqPathShape = { beq := Core.Path.instBEqPathShape.beq }

def Core.Path.instBEqPathShape.beq : PathShape → PathShape → Bool

Equations

• Core.Path.instBEqPathShape.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Path.instReprPathShape : Repr PathShape

Equations

• Core.Path.instReprPathShape = { reprPrec := Core.Path.instReprPathShape.repr }

def Core.Path.instReprPathShape.repr : PathShape → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Path.instReprPathShape.repr Core.Path.PathShape.source prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Path.PathShape.source")).group prec✝

def Core.Path.PathShape.toBoundedness : PathShape → Scale.Boundedness

Path shape to scale boundedness: bounded/source paths correspond to closed scales, unbounded paths to open scales. Parallel to quaBoundedness/cumBoundedness in Core/MereoDim.lean §1.

Equations

• Core.Path.PathShape.bounded.toBoundedness = Core.Scale.Boundedness.closed
• Core.Path.PathShape.source.toBoundedness = Core.Scale.Boundedness.closed
• Core.Path.PathShape.unbounded.toBoundedness = Core.Scale.Boundedness.open_

theorem Core.Path.bounded_path_licensed : PathShape.bounded.toBoundedness.isLicensed = true

Bounded paths are licensed (closed scale → admits degree modification). @cite{zwarts-2005}: "to the store" creates a telic VP because the path set is bounded, corresponding to a closed scale.

theorem Core.Path.source_path_licensed : PathShape.source.toBoundedness.isLicensed = true

Source paths are licensed (closed scale at the origin end).

theorem Core.Path.unbounded_path_blocked : PathShape.unbounded.toBoundedness.isLicensed = false

Unbounded paths are blocked (open scale → no inherent endpoint). @cite{zwarts-2005}: "towards the store" creates an atelic VP because the path set is unbounded, corresponding to an open scale.