Root content

What a root says about the action, its result, and the patient, the fine, within-class half of a root's meaning; the coarse half, which templatic components it entails, is Root.Kinds. Each dimension is a region of a finite scale rather than a point, since a verb is compatible with a range of force levels, patient materials, or result geometries. [spalek-mcnally-2026] separate English tear from Spanish rasgar, two roots of one kind, by patient robustness, force direction, and compatibility with careful action; [majid-boster-bowerman-2008] sort cutting and breaking events by instrument, object dimensionality, and the geometry of the result. Root.Content bundles one region per dimension, univ where a root says nothing.

Main declarations

• Root.Content.ForceLevel, ForceDirection, InstrumentType, AgentControl — dimensions of the action; ResultGeometry of the result; Robustness, ObjectDimensionality of the patient
• Root.Content — a region per dimension
• Root.Content.Overlaps — the regions meet on every dimension

References

• [spalek-mcnally-2026]: The anatomy of a verb.
• [majid-boster-bowerman-2008]: The cross-linguistic categorization of everyday events.
• [talmy-1988]: Force dynamics in language and cognition.
• [levin-1993]: English Verb Classes and Alternations.

Dimensions

inductive Semantics.Root.Content.ForceLevel : Type

Magnitude of the force involved ([talmy-1988]).

• zero : ForceLevel

  No force component, as in states.

• low : ForceLevel
• moderate : ForceLevel
• high : ForceLevel

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqForceLevel : DecidableEq ForceLevel

Equations

• Semantics.Root.Content.instDecidableEqForceLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeForceLevel : Fintype ForceLevel

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprForceLevel : Repr ForceLevel

Equations

• Semantics.Root.Content.instReprForceLevel = { reprPrec := Semantics.Root.Content.instReprForceLevel.repr }

def Semantics.Root.Content.instReprForceLevel.repr : ForceLevel → ℕ → Std.Format

Equations

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

inductive Semantics.Root.Content.ForceDirection : Type

Spatial pattern of the force applied ([Tal00]), contrary directions for tear and a single direction for rasgar ([spalek-mcnally-2026]).

• undirected : ForceDirection
• unidirectional : ForceDirection
• bidirectional : ForceDirection
• omnidirectional : ForceDirection

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqForceDirection : DecidableEq ForceDirection

Equations

• Semantics.Root.Content.instDecidableEqForceDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeForceDirection : Fintype ForceDirection

Equations

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

def Semantics.Root.Content.instReprForceDirection.repr : ForceDirection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprForceDirection : Repr ForceDirection

Equations

• Semantics.Root.Content.instReprForceDirection = { reprPrec := Semantics.Root.Content.instReprForceDirection.repr }

inductive Semantics.Root.Content.Robustness : Type

Material substantiality of the patient, on which rasgar is restricted to flimsy patients and tear is not ([spalek-mcnally-2026]).

• insubstantial : Robustness
• flimsy : Robustness
• moderate : Robustness
• robust : Robustness

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqRobustness : DecidableEq Robustness

Equations

• Semantics.Root.Content.instDecidableEqRobustness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeRobustness : Fintype Robustness

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprRobustness : Repr Robustness

Equations

• Semantics.Root.Content.instReprRobustness = { reprPrec := Semantics.Root.Content.instReprRobustness.repr }

def Semantics.Root.Content.instReprRobustness.repr : Robustness → ℕ → Std.Format

Equations

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

inductive Semantics.Root.Content.ResultGeometry : Type

The physical change produced, after the class descriptions of [levin-1993] (§45.1 break, §45.2 bend, §44 destroy, §21.1 cut) and [HK87]'s separation in material integrity.

• separation : ResultGeometry

  Loss of integrity by pulling apart (tear).

• surfaceBreach : ResultGeometry

  Damage to a surface (rasgar, cut).

• fracture : ResultGeometry

  Breakage along stress lines (crack, break).

• fragmentation : ResultGeometry

  Complete structural failure (shatter, smash).

• deformation : ResultGeometry

  Change of shape with integrity preserved (bend, fold).

• totalDestruction : ResultGeometry

  The entity ceases to exist as such (destroy).

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqResultGeometry : DecidableEq ResultGeometry

Equations

• Semantics.Root.Content.instDecidableEqResultGeometry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeResultGeometry : Fintype ResultGeometry

Equations

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

def Semantics.Root.Content.instReprResultGeometry.repr : ResultGeometry → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprResultGeometry : Repr ResultGeometry

Equations

• Semantics.Root.Content.instReprResultGeometry = { reprPrec := Semantics.Root.Content.instReprResultGeometry.repr }

inductive Semantics.Root.Content.InstrumentType : Type

The instrument effecting a separation, which together with the object's properties fixes how predictable the locus of separation is ([majid-boster-bowerman-2008]).

• sharpBlade : InstrumentType
• bluntImpact : InstrumentType
• hands : InstrumentType
• other : InstrumentType

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqInstrumentType : DecidableEq InstrumentType

Equations

• Semantics.Root.Content.instDecidableEqInstrumentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeInstrumentType : Fintype InstrumentType

Equations

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

def Semantics.Root.Content.instReprInstrumentType.repr : InstrumentType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprInstrumentType : Repr InstrumentType

Equations

• Semantics.Root.Content.instReprInstrumentType = { reprPrec := Semantics.Root.Content.instReprInstrumentType.repr }

inductive Semantics.Root.Content.ObjectDimensionality : Type

Dimensionality of the patient, the rope that snaps, the cloth that tears, or the pot that smashes ([majid-boster-bowerman-2008]).

• oneD : ObjectDimensionality
• twoD : ObjectDimensionality
• threeD : ObjectDimensionality

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqObjectDimensionality : DecidableEq ObjectDimensionality

Equations

• Semantics.Root.Content.instDecidableEqObjectDimensionality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeObjectDimensionality : Fintype ObjectDimensionality

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprObjectDimensionality : Repr ObjectDimensionality

Equations

• Semantics.Root.Content.instReprObjectDimensionality = { reprPrec := Semantics.Root.Content.instReprObjectDimensionality.repr }

def Semantics.Root.Content.instReprObjectDimensionality.repr : ObjectDimensionality → ℕ → Std.Format

Equations

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

inductive Semantics.Root.Content.AgentControl : Type

Compatibility with careful, controlled action, which tear has and rasgar lacks ([spalek-mcnally-2026]).

• incompatible : AgentControl
• neutral : AgentControl
• compatible : AgentControl

@[instance_reducible]

instance Semantics.Root.Content.instDecidableEqAgentControl : DecidableEq AgentControl

Equations

• Semantics.Root.Content.instDecidableEqAgentControl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Root.Content.instFintypeAgentControl : Fintype AgentControl

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instReprAgentControl : Repr AgentControl

Equations

• Semantics.Root.Content.instReprAgentControl = { reprPrec := Semantics.Root.Content.instReprAgentControl.repr }

def Semantics.Root.Content.instReprAgentControl.repr : AgentControl → ℕ → Std.Format

Equations

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

structure Semantics.Root.Content : Type

A root's content, a region of each dimension, univ where the root says nothing.

• force : Finset ForceLevel

  Magnitude of the force applied.

• direction : Finset ForceDirection

  Direction of the force applied.

• instrument : Finset InstrumentType

  The instrument selected for.

• agentControl : Finset AgentControl

  Compatibility with careful action.

• resultGeometry : Finset ResultGeometry

  The physical change produced.

• patientRobustness : Finset Robustness

  Robustness of the patient.

• patientDimensionality : Finset ObjectDimensionality

  Dimensionality of the patient.

def Semantics.Root.instDecidableEqContent.decEq (x✝ x✝¹ : Content) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Semantics.Root.instDecidableEqContent : DecidableEq Content

Equations

• Semantics.Root.instDecidableEqContent = Semantics.Root.instDecidableEqContent.decEq

def Semantics.Root.Content.Overlaps (p q : Content) : Prop

Two contents overlap when their regions meet on every dimension.

Equations

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

@[instance_reducible]

instance Semantics.Root.Content.instDecidableOverlaps (p q : Content) : Decidable (p.Overlaps q)

Equations

• p.instDecidableOverlaps q = id inferInstance