Root outcomes — event-relative machinery

The heavy, event-relative half of the outcome substrate: the boundary operators res/pre and the outcome-bearing carrier VerbOutcomes. The light cardinality invariant (OutcomeCardinality) lives in Semantics/Verb/Root/OutcomeCardinality.lean so that Root can carry the outcome axis without depending on Event/EventRel.

A verb root lexically encodes the set of outcomes its object can be in after the action — the dimension [Bha24] adds to root semantics, orthogonal to the manner/result/cause kinds of [BKG20]'s Root.Kinds (bend and break share a signature, differ in outcomes).

Main definitions

• resState / preState — an object's state at the right / left boundary of an event ([Bha24], eqs. 64–65)
• VerbOutcomes — an outcome-bearing predicate: base predicate, outcome set, threshold set; VerbOutcomes.cardinality reads off its OutcomeCardinality

References

• [Bha24] (roots encode outcome sets)

Event boundaries (eqs. 64–65)

res and pre read an object's lexically-relevant state (the paper's state k : t ↦ l(x), abstracted here as State) at the right and left boundaries of an event's temporal trace τ. They are equivalence operators, not temporal ones — they yield states, not times.

@[reducible, inline]

abbrev Semantics.Lexical.StateFunction (Entity : Type u_1) (State : Type u_2) (Time : Type u_3) : Type (max (max u_1 u_2) u_3)

A state function tracks an object's state at each time point.

Equations

• Semantics.Lexical.StateFunction Entity State Time = (Time → Entity → State)

def Semantics.Lexical.resState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : StateFunction Entity State Time) (e : Event Time) (x : Entity) : State

res(e)(x) (eq. 64): the object's state at the right boundary of e.

Equations

• Semantics.Lexical.resState k e x = k e.τ.toProd.2 x

def Semantics.Lexical.preState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : StateFunction Entity State Time) (e : Event Time) (x : Entity) : State

pre(e)(x) (eq. 65): the object's state at the left boundary of e.

Equations

• Semantics.Lexical.preState k e x = k e.τ.toProd.1 x

The outcome-bearing verb root (the heavy witness)

An outcome-bearing predicate bundles the base predicate P (event-first, the ⟨v,⟨e,t⟩⟩ meaning affixes modify) with the lexical outcome set O and the contextual threshold set T.

structure Semantics.Lexical.VerbOutcomes (Entity : Type u_4) (State : Type u_5) (Time : Type u_6) [LinearOrder Time] : Type (max (max u_4 u_5) u_6)

A verb root carrying an outcome set, the carrier result-state modifiers act on ([Bha24], eqs. 56, 60).

• verb : ArgumentStructure.EventRel Time Entity

  The base predicate P(e)(x) (⟨v,⟨e,t⟩⟩).

• outcomes : Set State

  The lexically-encoded outcome set O (states at the right boundary).

• thresholds : Set State

  The contextual threshold set T (states at the left boundary).

noncomputable def Semantics.Lexical.VerbOutcomes.cardinality {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (vro : VerbOutcomes Entity State Time) : Verb.OutcomeCardinality

The cardinality tier of a root's outcome set.

Equations

• vro.cardinality = Verb.OutcomeCardinality.ofSet vro.outcomes