Dimension Coherence Bridge

Connects the dimension coherence theorems from Events/DimensionCoherence.lean and Events/DimensionBridge.lean to concrete VP data and licensing predictions.

What it exercises

• dimension_coherence (cross-chain QUA pullback)
• any_chain_qua_transfer (falsifiable prediction for future dimensions)
• dimension_irrelevance (QUA/CUM ↔ licensed/blocked)
• two_step_agrees_with_composite (composition coherence)
• licensing_factors_through_boundedness (licensing invariance)

Structure

1. Dimension irrelevance — all dimension chains produce same licensing
2. Licensing pipeline convergence — all classification systems converge
3. Per-VP convergence — concrete VPs with all systems agreeing
4. Falsifiability exercise — any_chain_qua_transfer as scientific prediction
5. Diagnostic bridge — licensing → for/in compatibility

All three dimension chains (temporal, spatial, object) produce the same licensing prediction from the same mereological source.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.dimension_irrelevance_verified : Mereology.quaBoundedness.isLicensed = true ∧ Mereology.cumBoundedness.isLicensed = false

QUA → licensed, CUM → blocked, regardless of dimension.

All six classification systems converge at the same licensing prediction for each concrete VP.

structure Phenomena.TenseAspect.Studies.DimensionCoherence.VPLicensingDatum : Type

A VP licensing datum with predictions from all classification paths.

• vp : String
• vendlerClass : Semantics.Tense.Aspect.LexicalAspect.VendlerClass
• telicity : Semantics.Tense.Aspect.LexicalAspect.Telicity
• mereoTag : Core.Scale.MereoTag
• boundedness : Core.Scale.Boundedness
• expectedLicensed : Bool

def Phenomena.TenseAspect.Studies.DimensionCoherence.instReprVPLicensingDatum.repr : VPLicensingDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.DimensionCoherence.instReprVPLicensingDatum : Repr VPLicensingDatum

Equations

• Phenomena.TenseAspect.Studies.DimensionCoherence.instReprVPLicensingDatum = { reprPrec := Phenomena.TenseAspect.Studies.DimensionCoherence.instReprVPLicensingDatum.repr }

instance Phenomena.TenseAspect.Studies.DimensionCoherence.instDecidableEqVPLicensingDatum : DecidableEq VPLicensingDatum

Equations

• Phenomena.TenseAspect.Studies.DimensionCoherence.instDecidableEqVPLicensingDatum = Phenomena.TenseAspect.Studies.DimensionCoherence.instDecidableEqVPLicensingDatum.decEq

def Phenomena.TenseAspect.Studies.DimensionCoherence.instDecidableEqVPLicensingDatum.decEq (x✝ x✝¹ : VPLicensingDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Studies.DimensionCoherence.instBEqVPLicensingDatum : BEq VPLicensingDatum

Equations

• Phenomena.TenseAspect.Studies.DimensionCoherence.instBEqVPLicensingDatum = { beq := Phenomena.TenseAspect.Studies.DimensionCoherence.instBEqVPLicensingDatum.beq }

def Phenomena.TenseAspect.Studies.DimensionCoherence.instBEqVPLicensingDatum.beq : VPLicensingDatum → VPLicensingDatum → Bool

Equations

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

def Phenomena.TenseAspect.Studies.DimensionCoherence.eatTwoApples : VPLicensingDatum

"eat two apples": accomplishment → telic → QUA → closed → licensed.

Equations

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

def Phenomena.TenseAspect.Studies.DimensionCoherence.eatApples : VPLicensingDatum

"eat apples": activity → atelic → CUM → open → blocked.

Equations

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

def Phenomena.TenseAspect.Studies.DimensionCoherence.arriveVP : VPLicensingDatum

"arrive": achievement → telic → QUA → closed → licensed.

Equations

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

def Phenomena.TenseAspect.Studies.DimensionCoherence.sleepVP : VPLicensingDatum

"sleep": state → atelic → CUM → open → blocked.

Equations

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

def Phenomena.TenseAspect.Studies.DimensionCoherence.vpData : List VPLicensingDatum

Equations

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

Verify that the hardcoded VendlerClass values in VP data match the fragment verb entries. Without these, changing a fragment annotation would leave the convergence theorems below silently green.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.eatTwoApples_grounded : Fragments.English.Predicates.Verbal.eat.vendlerClass = some eatTwoApples.vendlerClass

"eat two apples" vendlerClass matches fragment.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.eatApples_grounded : Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity = eatApples.telicity

"eat apples" VP-level activity comes from sinc + CUM NP composition.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.arriveVP_grounded : Fragments.English.Predicates.Verbal.arrive.vendlerClass = some arriveVP.vendlerClass

"arrive" vendlerClass matches fragment.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.sleepVP_grounded : Fragments.English.Predicates.Verbal.sleep.vendlerClass = some sleepVP.vendlerClass

"sleep" vendlerClass matches fragment.

Verify that all classification paths converge for each VP.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.eat_two_apples_convergence : Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic ∧ Semantics.Tense.Aspect.LexicalAspect.Telicity.telic.toMereoTag = Core.Scale.MereoTag.qua ∧ Core.Scale.MereoTag.qua.toBoundedness = Core.Scale.Boundedness.closed ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = true ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.Telicity.telic = true ∧ Core.Scale.LicensingPipeline.isLicensed Core.Scale.MereoTag.qua = true ∧ Core.Scale.LicensingPipeline.isLicensed Core.Scale.Boundedness.closed = true

All paths converge for "eat two apples".

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.eat_apples_convergence : Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic ∧ Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic.toMereoTag = Core.Scale.MereoTag.cum ∧ Core.Scale.MereoTag.cum.toBoundedness = Core.Scale.Boundedness.open_ ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = false ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic = false ∧ Core.Scale.LicensingPipeline.isLicensed Core.Scale.MereoTag.cum = false ∧ Core.Scale.LicensingPipeline.isLicensed Core.Scale.Boundedness.open_ = false

All paths converge for "eat apples".

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.arrive_convergence : Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = true

All paths converge for "arrive".

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.sleep_convergence : Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = false

All paths converge for "sleep".

any_chain_qua_transfer from DimensionCoherence.lean says that any DimensionChain — including ones not yet defined — must satisfy QUA transfer. This is a falsifiable scientific prediction: if someone found a mereological dimension where QUA doesn't transfer, the MereoDim axiom for that dimension would be falsified.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.classification_diamond : (∀ (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass), Core.Scale.LicensingPipeline.isLicensed c.telicity = Core.Scale.LicensingPipeline.isLicensed c) ∧ ∀ (s : Core.Path.PathShape), Core.Scale.LicensingPipeline.isLicensed (Semantics.Events.SpatialTrace.pathShapeToTelicity s) = Core.Scale.LicensingPipeline.isLicensed s

The commutativity diamond holds: all paths through the classification diagram converge at Boundedness.

All classification paths produce the same diagnostic predictions.

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.licensed_accepts_inX : Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Diagnostics.DiagnosticResult.accept ∧ Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Diagnostics.DiagnosticResult.accept

Licensed VPs (telic/QUA/closed) accept "in X".

theorem Phenomena.TenseAspect.Studies.DimensionCoherence.blocked_accepts_forX : Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Diagnostics.DiagnosticResult.accept ∧ Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Diagnostics.DiagnosticResult.accept

Blocked VPs (atelic/CUM/open) accept "for X".