Cross-Dimension Bridge (Theory-Specific)

@cite{kennedy-2007} @cite{krifka-1989} @cite{krifka-1998} @cite{rouillard-2026} @cite{zwarts-2005}

Theory-specific commutativity squares, LicensingPipeline instances, concrete dimension chain instantiations, and end-to-end licensing theorems. Builds on the theory-neutral infrastructure in Core/MereoDim.lean, Core/Time.lean, Core/Path.lean, and Core/Scale.lean.

Three Levels of Unification

1. LicensingPipeline instances: Telicity, VendlerClass, PathShape join Boundedness, MereoTag, BoundaryType as pipeline sources.

2. Full commutativity diamond: All six classification paths converge at Boundedness. Proved pairwise: VendlerClass → Telicity → Boundedness = VendlerClass → scaleBoundedness, and likewise for PathShape.

3. Concrete dimension chains: Temporal (τ, dur), spatial (σ, dist), and object (θ, μ) chains instantiate DimensionChain, with end-to-end QUA transfer theorems.

4. Dimension irrelevance: The licensing prediction depends only on the mereological tag (QUA/CUM), not on which dimension (temporal/spatial/object) the chain traverses. This is the "all the same theorem" claim.

@[reducible, inline]

abbrev Semantics.Events.DimensionBridge.telicityToBoundedness (t : Tense.Aspect.LexicalAspect.Telicity) : Core.Scale.Boundedness

Telicity maps to scale boundedness via MereoTag: telic → QUA → closed, atelic → CUM → open. Derived through the compositional chain Telicity →.toMereoTag MereoTag →.toBoundedness Boundedness. This is the shared core of all four licensing frameworks: @cite{kennedy-2007}, @cite{rouillard-2026}, @cite{krifka-1989}, @cite{zwarts-2005}.

Equations

• Semantics.Events.DimensionBridge.telicityToBoundedness t = t.toMereoTag.toBoundedness

theorem Semantics.Events.DimensionBridge.telic_is_closed : telicityToBoundedness Tense.Aspect.LexicalAspect.Telicity.telic = Core.Scale.Boundedness.closed

theorem Semantics.Events.DimensionBridge.atelic_is_open : telicityToBoundedness Tense.Aspect.LexicalAspect.Telicity.atelic = Core.Scale.Boundedness.open_

instance Semantics.Events.DimensionBridge.instLicensingPipelineTelicity : Core.Scale.LicensingPipeline Tense.Aspect.LexicalAspect.Telicity

Equations

• Semantics.Events.DimensionBridge.instLicensingPipelineTelicity = { toBoundedness := Semantics.Events.DimensionBridge.telicityToBoundedness }

instance Semantics.Events.DimensionBridge.instLicensingPipelineVendlerClass : Core.Scale.LicensingPipeline Tense.Aspect.LexicalAspect.VendlerClass

Equations

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

instance Semantics.Events.DimensionBridge.instLicensingPipelinePathShape : Core.Scale.LicensingPipeline Core.Path.PathShape

Equations

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

theorem Semantics.Events.DimensionBridge.vendler_comm (c : Tense.Aspect.LexicalAspect.VendlerClass) : telicityToBoundedness c.telicity = Montague.Sentence.MaximalInformativity.scaleBoundedness c

VendlerClass → Telicity → Boundedness = VendlerClass → Boundedness. Both paths route through the same compositional chain (VendlerClass →.telicity Telicity →.toMereoTag MereoTag →.toBoundedness Boundedness), so agreement is definitional.

theorem Semantics.Events.DimensionBridge.pathShape_comm (s : Core.Path.PathShape) : telicityToBoundedness (SpatialTrace.pathShapeToTelicity s) = s.toBoundedness

PathShape → Telicity → Boundedness = PathShape → Boundedness. The compositional chain (PathShape → Telicity → MereoTag → Boundedness) agrees with the direct PathShape.toBoundedness from Core/Path.lean. This is a genuine commutativity proof: the Core-level direct classification and the Theories-level compositional derivation yield the same result.

theorem Semantics.Events.DimensionBridge.mereoTag_boundedness_qua : Core.Scale.MereoTag.qua.toBoundedness = Core.Scale.Boundedness.closed

MereoTag.qua = Boundedness.closed.

theorem Semantics.Events.DimensionBridge.mereoTag_boundedness_cum : Core.Scale.MereoTag.cum.toBoundedness = Core.Scale.Boundedness.open_

MereoTag.cum = Boundedness.open_.

theorem Semantics.Events.DimensionBridge.boundaryType_closed : Core.Time.Interval.BoundaryType.closed.toBoundedness = Core.Scale.Boundedness.closed

BoundaryType.closed = Boundedness.closed.

theorem Semantics.Events.DimensionBridge.boundaryType_open : Core.Time.Interval.BoundaryType.open_.toBoundedness = Core.Scale.Boundedness.open_

BoundaryType.open_ = Boundedness.open_.

theorem Semantics.Events.DimensionBridge.commutativity_diamond : (∀ (c : Tense.Aspect.LexicalAspect.VendlerClass), Core.Scale.LicensingPipeline.isLicensed c.telicity = Core.Scale.LicensingPipeline.isLicensed c) ∧ (∀ (s : Core.Path.PathShape), Core.Scale.LicensingPipeline.isLicensed (SpatialTrace.pathShapeToTelicity s) = Core.Scale.LicensingPipeline.isLicensed s) ∧ Core.Scale.LicensingPipeline.isLicensed Core.Scale.MereoTag.qua = Core.Scale.LicensingPipeline.isLicensed Core.Scale.Boundedness.closed ∧ Core.Scale.LicensingPipeline.isLicensed Core.Scale.MereoTag.cum = Core.Scale.LicensingPipeline.isLicensed Core.Scale.Boundedness.open_

The full commutativity diamond: every path through the classification diagram produces the same licensing prediction. With compositional chains, the VendlerClass and PathShape arms are definitional (both sides route through the same chain).

noncomputable def Semantics.Events.DimensionBridge.temporalChain {Time : Type u_1} [LinearOrder Time] [cem : Mereology.EventCEM Time] {dur : Core.Time.Interval Time → ℚ} [hDur : Mereology.ExtMeasure (Core.Time.Interval Time) dur] (hInj : Function.Injective fun (e : Ev Time) => e.runtime) : Mereology.DimensionChain (fun (e : Ev Time) => e.runtime) dur

Temporal dimension chain: Events →τ Intervals →dur ℚ.

Equations

• ⋯ = ⋯

theorem Semantics.Events.DimensionBridge.temporal_qua_licensed {Time : Type u_1} [LinearOrder Time] [cem : Mereology.EventCEM Time] {dur : Core.Time.Interval Time → ℚ} [hDur : Mereology.ExtMeasure (Core.Time.Interval Time) dur] (hInj : Function.Injective fun (e : Ev Time) => e.runtime) {P : ℚ → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ dur ∘ fun (e : Ev Time) => e.runtime)

Temporal end-to-end: QUA on ℚ → QUA on Events through τ then dur.

noncomputable def Semantics.Events.DimensionBridge.spatialChain {Time : Type u_1} [LinearOrder Time] [cem : Mereology.EventCEM Time] {Loc : Type u_2} [SemilatticeSup (Core.Path.Path Loc)] [st : SpatialTrace Loc Time] {dist : Core.Path.Path Loc → ℚ} [hDist : Mereology.ExtMeasure (Core.Path.Path Loc) dist] (hInj : Function.Injective SpatialTrace.σ) : Mereology.DimensionChain SpatialTrace.σ dist

Spatial dimension chain: Events →σ Paths →dist ℚ.

Equations

• ⋯ = ⋯

theorem Semantics.Events.DimensionBridge.spatial_qua_licensed {Time : Type u_1} [LinearOrder Time] [cem : Mereology.EventCEM Time] {Loc : Type u_2} [SemilatticeSup (Core.Path.Path Loc)] [st : SpatialTrace Loc Time] {dist : Core.Path.Path Loc → ℚ} [hDist : Mereology.ExtMeasure (Core.Path.Path Loc) dist] (hInj : Function.Injective SpatialTrace.σ) {P : ℚ → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ dist ∘ SpatialTrace.σ)

Spatial end-to-end: QUA on ℚ → QUA on Events through σ then dist.

noncomputable def Semantics.Events.DimensionBridge.objectChain {Time : Type u_1} [LinearOrder Time] [cem : Mereology.EventCEM Time] {Entity : Type u_3} [SemilatticeSup Entity] [rh : Mereology.RoleHom Entity Time] {μ : Entity → ℚ} [hμ : Mereology.ExtMeasure Entity μ] (hInj : Function.Injective Mereology.RoleHom.themeOf) : Mereology.DimensionChain Mereology.RoleHom.themeOf μ

Object dimension chain: Events →θ Entities →μ ℚ.

Equations

• ⋯ = ⋯

theorem Semantics.Events.DimensionBridge.object_qua_licensed {Time : Type u_1} [LinearOrder Time] [cem : Mereology.EventCEM Time] {Entity : Type u_3} [SemilatticeSup Entity] [rh : Mereology.RoleHom Entity Time] {μ : Entity → ℚ} [hμ : Mereology.ExtMeasure Entity μ] (hInj : Function.Injective Mereology.RoleHom.themeOf) {P : ℚ → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ μ ∘ Mereology.RoleHom.themeOf)

Object end-to-end: QUA on ℚ → QUA on Events through θ then μ.

theorem Semantics.Events.DimensionBridge.dimension_irrelevance : Mereology.quaBoundedness.isLicensed = true ∧ Mereology.cumBoundedness.isLicensed = false

The three chains produce the same licensing from the same mereological source. This is "all the same theorem": regardless of which dimension (temporal, spatial, object), QUA → telic → closed → licensed and CUM → atelic → open → blocked. The dimension is irrelevant.