Cross-Domain Licensing Agreement Bridge #

@cite{champollion-2017} @cite{kennedy-2007} @cite{krifka-1989} @cite{krifka-1998} @cite{rouillard-2026} @cite{zwarts-2005} @cite{vendler-1957}

The showcase theorem: six independent classification systems from different linguistic subfields all agree on licensing predictions, because they all route through LicensingPipeline.isLicensed → Boundedness.isLicensed.

Compositional Chain Architecture #

MereoTag (QUA/CUM) serves as the canonical bottleneck — all binary domain classifications route through it, and MereoTag.toBoundedness is the single point where the licensing prediction is made:

VendlerClass ─.telicity─→ Telicity ─.toMereoTag─→ MereoTag ─.toBoundedness─→ Boundedness
PathShape ─pathShapeToTelicity─→ Telicity ─.toMereoTag─→ MereoTag ─.toBoundedness─→ Boundedness
SituationBoundedness ─.toMereoTag─→ MereoTag ─.toBoundedness─→ Boundedness
BoundaryType ─.toBoundedness─→ Boundedness (direct — concepts are identical)
EpistemicTag ─.toBoundedness─→ Boundedness (direct — weak mereological link)

Each arrow encodes an independently motivated theoretical insight:

.telicity: Vendler classes determine telicity
pathShapeToTelicity: bounded paths create telic VPs
.toMereoTag: telic = quantized
.toBoundedness: quantized = closed scale

The Six Sources #

Source	Type	Closed variant	Module
Scale boundedness	`Boundedness`	`.closed`	Core/Scale
Mereological tag	`MereoTag`	`.qua`	Core/Scale
Telicity	`Telicity`	`.telic`	Events/Aspect
Vendler class	`VendlerClass`	`.accomplishment`	Events/Aspect
Interval boundary	`BoundaryType`	`.closed`	Core/Time
Situation boundedness	`SituationBoundedness`	`.bounded`	Core/Time

All six have LicensingPipeline instances mapping their closed/open variants to Boundedness.closed/.open_, yielding identical licensing predictions.

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.kennedy_rouillard_agree {max : ℕ} {W₁ : Type u_1} {W₂ : Type u_2} (μ₁ : W₁ → Core.Scale.Degree max) (μ₂ : W₂ → ℕ) :

(Semantics.Lexical.Adjective.adjMeasure μ₁ Fragments.English.Predicates.Adjectival.full).licensed = (Core.Scale.DirectedMeasure.rouillardETIA μ₂ Core.Scale.Boundedness.closed).licensed

Kennedy adjective (closed) and Rouillard E-TIA (closed) agree.

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.full_and_accomplishment_same_reason :

Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.full.scaleType = Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Adjective licensing and VP licensing use the same reason: both derive from Boundedness.closed.isLicensed.

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.tall_and_state_same_reason :

Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.tall.scaleType = Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state

Open adjective ("tall") blocks for the same reason as atelic VP.

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.achievement_eq_accomplishment :

Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Achievement = accomplishment (both telic → closed → licensed).

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.activity_eq_state :

Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state

Activity = state (both atelic → open → blocked).

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.bounded_eq_closedBoundary :

Core.Scale.LicensingPipeline.isLicensed Core.Time.SituationBoundedness.bounded = Core.Scale.LicensingPipeline.isLicensed Core.Time.Interval.BoundaryType.closed

SituationBoundedness.bounded = BoundaryType.closed (both → Boundedness.closed → licensed).

The epistemic probability scale is closed [0,1] (@cite{kennedy-2007}), so epistemic adjectives like "certain" license degree modification ("completely certain") for the same structural reason that "full" does — closed-scale boundedness routes through Boundedness.closed → isLicensed = true.

This connects the seventh licensing source (epistemic modality) to the existing six, demonstrating that the LicensingPipeline unification extends beyond the adjectival and verbal domains into epistemic modal semantics.

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.epistemic_agrees_with_adj_closed :

Core.Scale.LicensingPipeline.isLicensed Semantics.Attitudes.EpistemicThreshold.epistemicBoundedness = Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.full.scaleType

Epistemic probability licensing agrees with Kennedy adjective licensing: both are Boundedness.closed → isLicensed = true. "completely certain" is licensed for the same reason as "completely full".

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.epistemic_agrees_with_telic :

Core.Scale.LicensingPipeline.isLicensed Semantics.Attitudes.EpistemicThreshold.epistemicBoundedness = Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

Epistemic licensing agrees with telic VP licensing: "completely certain" licensed for the same reason as "in an hour" with accomplishments (both closed).

source

theorem Phenomena.Gradability.CrossDomainLicensingBridge.epistemic_agrees_with_qua :

Core.Scale.LicensingPipeline.isLicensed Semantics.Attitudes.EpistemicThreshold.epistemicBoundedness = Core.Scale.LicensingPipeline.isLicensed Core.Scale.MereoTag.qua

Epistemic licensing agrees with QUA mereological licensing.

Documentation

Linglib.Phenomena.Gradability.Studies.Rouillard2026

Cross-Domain Licensing Agreement Bridge #

Compositional Chain Architecture #

The Six Sources #