Root Quality Dimensions

Within-class root content profiles: ranges over quality dimensions — force, robustness, instrument, dimensionality, agent properties. A multi-paper synthesis ([Tal88], [Tal00], [Dow91], [MBB08], [SMcN26]); no single paper carries this profile. Structural entailments (state, manner, result, cause) are the separate Root.Kinds (Roots/Signature.lean).

Main declarations

• Root.Profile.Range — within-class variation along a dimension
• the dimension enums (ForceLevel, Robustness, InstrumentType, …)
• Root.Profile — the bundled profile

Range mechanism

@[reducible, inline]

abbrev Verb.Root.Profile.Range (α : Type u_1) : Type u_1

Acceptable values along a quality dimension.

• none: the root is unconstrained on this dimension (says nothing)
• some [v₁, v₂, …]: the root is compatible with exactly these values

Roots are regions, not points: a verb like tear is compatible with a range of force levels, not a single one.

Equations

• Verb.Root.Profile.Range α = Option (List α)

def Verb.Root.Profile.Range.unconstrained {α : Type u_1} : Range α

Equations

• Verb.Root.Profile.Range.unconstrained = none

def Verb.Root.Profile.Range.only {α : Type u_1} (vs : List α) : Range α

Equations

• Verb.Root.Profile.Range.only vs = some vs

def Verb.Root.Profile.Range.isCompatible {α : Type u_1} [BEq α] : Range α → α → Bool

Equations

• Verb.Root.Profile.Range.isCompatible none x✝ = true
• Verb.Root.Profile.Range.isCompatible (some vs) x✝ = vs.contains x✝

def Verb.Root.Profile.Range.isConstrained {α : Type u_1} : Range α → Bool

Equations

• Verb.Root.Profile.Range.isConstrained none = false
• Verb.Root.Profile.Range.isConstrained (some val) = true

def Verb.Root.Profile.Range.overlaps {α : Type u_1} [BEq α] : Range α → Range α → Bool

Two ranges overlap if they share at least one value.

Equations

• Verb.Root.Profile.Range.overlaps none x✝ = true
• x✝.overlaps none = true
• Verb.Root.Profile.Range.overlaps (some vs₁) (some vs₂) = vs₁.any fun (x : α) => vs₂.contains x

Quality dimensions

inductive Verb.ForceLevel : Type

Magnitude of force involved in the event.

[Tal88] identifies force magnitude as a core parameter of force-dynamic schemas. [SMcN26]: tear implies considerable force; rasgar implies less (enough to damage something flimsy).

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

@[implicit_reducible]

instance Verb.instDecidableEqForceLevel : DecidableEq ForceLevel

Equations

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

@[implicit_reducible]

instance Verb.instReprForceLevel : Repr ForceLevel

Equations

• Verb.instReprForceLevel = { reprPrec := Verb.instReprForceLevel.repr }

def Verb.instReprForceLevel.repr : ForceLevel → ℕ → Std.Format

Equations

• Verb.instReprForceLevel.repr Verb.ForceLevel.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ForceLevel.none")).group prec✝
• Verb.instReprForceLevel.repr Verb.ForceLevel.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ForceLevel.low")).group prec✝
• Verb.instReprForceLevel.repr Verb.ForceLevel.moderate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ForceLevel.moderate")).group prec✝
• Verb.instReprForceLevel.repr Verb.ForceLevel.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ForceLevel.high")).group prec✝

inductive Verb.ForceDirection : Type

Spatial pattern of force application.

[Tal00]: force vectors have directional parameters. [SMcN26]: tear implies contrary-direction force (pulling apart); rasgar implies unidirectional force (gash-like).

• none : ForceDirection
• unidirectional : ForceDirection
• bidirectional : ForceDirection
• omnidirectional : ForceDirection

@[implicit_reducible]

instance Verb.instDecidableEqForceDirection : DecidableEq ForceDirection

Equations

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

def Verb.instReprForceDirection.repr : ForceDirection → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprForceDirection.repr Verb.ForceDirection.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ForceDirection.none")).group prec✝

@[implicit_reducible]

instance Verb.instReprForceDirection : Repr ForceDirection

Equations

• Verb.instReprForceDirection = { reprPrec := Verb.instReprForceDirection.repr }

inductive Verb.Robustness : Type

Material substantiality of the affected entity (patient).

[SMcN26]: the primary dimension distinguishing tear (unrestricted) from rasgar (flimsy patients only).

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

@[implicit_reducible]

instance Verb.instDecidableEqRobustness : DecidableEq Robustness

Equations

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

@[implicit_reducible]

instance Verb.instReprRobustness : Repr Robustness

Equations

• Verb.instReprRobustness = { reprPrec := Verb.instReprRobustness.repr }

def Verb.instReprRobustness.repr : Robustness → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprRobustness.repr Verb.Robustness.flimsy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Robustness.flimsy")).group prec✝
• Verb.instReprRobustness.repr Verb.Robustness.moderate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Robustness.moderate")).group prec✝
• Verb.instReprRobustness.repr Verb.Robustness.robust prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Robustness.robust")).group prec✝

inductive Verb.ResultType : Type

Nature of the physical change produced by the event.

Grounded in [Lev93]'s class descriptions and [HK87] notion of "separation in material integrity":

• 45.1 Break: loss of material integrity (break, crack, shatter, tear)
• 45.2 Bend: change in shape without loss of integrity
• 44 Destroy: total destruction (no specific resulting state)
• 21 Cut: separation via instrument contact Refined by [BKG20] on CoS root types. UNVERIFIED: Levin chapter numbers cited from memory.

• separation : ResultType
• surfaceBreach : ResultType
• fracture : ResultType
• fragmentation : ResultType
• deformation : ResultType
• totalDestruction : ResultType

@[implicit_reducible]

instance Verb.instDecidableEqResultType : DecidableEq ResultType

Equations

• Verb.instDecidableEqResultType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Verb.instReprResultType : Repr ResultType

Equations

• Verb.instReprResultType = { reprPrec := Verb.instReprResultType.repr }

def Verb.instReprResultType.repr : ResultType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprResultType.repr Verb.ResultType.separation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ResultType.separation")).group prec✝
• Verb.instReprResultType.repr Verb.ResultType.fracture prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ResultType.fracture")).group prec✝
• Verb.instReprResultType.repr Verb.ResultType.deformation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.ResultType.deformation")).group prec✝

inductive Verb.InstrumentType : Type

Type of instrument used in the event.

[MBB08]: instrument type interacts with object properties to determine the predictability of separation locus (their Dimension 1). Sharp instruments yield predictable separations; blunt instruments and hands yield unpredictable separations.

[Lev93]: cut verbs specify their instrument (instrumentSpec = true); break verbs do not. UNVERIFIED: Levin chapter (§21 vs §45.1) cited from memory.

• sharpBlade : InstrumentType
• bluntImpact : InstrumentType
• hands : InstrumentType
• none : InstrumentType

@[implicit_reducible]

instance Verb.instDecidableEqInstrumentType : DecidableEq InstrumentType

Equations

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

@[implicit_reducible]

instance Verb.instReprInstrumentType : Repr InstrumentType

Equations

• Verb.instReprInstrumentType = { reprPrec := Verb.instReprInstrumentType.repr }

def Verb.instReprInstrumentType.repr : InstrumentType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprInstrumentType.repr Verb.InstrumentType.hands prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.InstrumentType.hands")).group prec✝
• Verb.instReprInstrumentType.repr Verb.InstrumentType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.InstrumentType.none")).group prec✝

inductive Verb.ObjectDimensionality : Type

Dimensionality of the affected object (patient).

[MBB08]: object dimensionality interacts with instrument type and manner of action to determine event categorization cross-linguistically. 1D objects (rope, stick) can be snapped; 2D objects (cloth, paper) can be torn; 3D objects (melon, pot) can be smashed.

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

@[implicit_reducible]

instance Verb.instDecidableEqObjectDimensionality : DecidableEq ObjectDimensionality

Equations

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

def Verb.instReprObjectDimensionality.repr : ObjectDimensionality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Verb.instReprObjectDimensionality : Repr ObjectDimensionality

Equations

• Verb.instReprObjectDimensionality = { reprPrec := Verb.instReprObjectDimensionality.repr }

inductive Verb.Volitionality : Type

Whether the agent acts with volitional intent.

[Dow91]: Proto-Agent entailment P1 = "volitional involvement in the event or state." [AYS21]: killing verb roots impose specific intentionality requirements on the agent (murder requires intentional agent; kill does not). [Lev93]: some break verbs "allow unintentional, action interpretations with body-part objects."

• nonvolitional : Volitionality
• neutral : Volitionality
• volitional : Volitionality

@[implicit_reducible]

instance Verb.instDecidableEqVolitionality : DecidableEq Volitionality

Equations

• Verb.instDecidableEqVolitionality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Verb.instReprVolitionality : Repr Volitionality

Equations

• Verb.instReprVolitionality = { reprPrec := Verb.instReprVolitionality.repr }

def Verb.instReprVolitionality.repr : Volitionality → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprVolitionality.repr Verb.Volitionality.neutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Volitionality.neutral")).group prec✝

inductive Verb.AgentControl : Type

Whether the action can be performed with care and control.

[Dow91]: Proto-Agent entailment P2 = "sentience (and/or perception)," enabling controlled action. [SMcN26]: tear is compatible with careful action ("carefully tore the tin foil"); rasgar is not ("??rasgaron con cuidado el papel").

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

@[implicit_reducible]

instance Verb.instDecidableEqAgentControl : DecidableEq AgentControl

Equations

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

@[implicit_reducible]

instance Verb.instReprAgentControl : Repr AgentControl

Equations

• Verb.instReprAgentControl = { reprPrec := Verb.instReprAgentControl.repr }

def Verb.instReprAgentControl.repr : AgentControl → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprAgentControl.repr Verb.AgentControl.neutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.AgentControl.neutral")).group prec✝

structure Verb.Root.Profile : Type

Within-class root content profile.

Captures quality dimensions of root content — force, robustness, agent properties — as opposed to Root.Kinds, which captures structural entailments (state, manner, result, cause).

Each dimension is a Range of acceptable values; none means the root says nothing about that dimension (unconstrained).

• forceMag : Range ForceLevel

  Force magnitude: [Tal88].

• forceDir : Range ForceDirection

  Force directionality: [Tal00], [SMcN26].

• patientRob : Range Robustness

  Patient material robustness: [SMcN26].

• resultType : Range ResultType

  Type of physical change: [Lev93], [BKG20].

• agentVolition : Range Volitionality

  Agent volitionality: [Dow91] P1, [AYS21].

• agentControl : Range AgentControl

  Agent control: [Dow91] P2, [SMcN26].

• instrumentType : Range InstrumentType

  Instrument type the root selects for: [MBB08]. cut selects for sharp blades; break is unspecified.

• patientDim : Range ObjectDimensionality

  Patient dimensionality: [MBB08]. tear selects for 2D objects (cloth, paper); snap for 1D (stick, twig).

@[implicit_reducible]

instance Verb.Root.instDecidableEqProfile : DecidableEq Profile

Equations

• Verb.Root.instDecidableEqProfile = Verb.Root.instDecidableEqProfile.decEq

def Verb.Root.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) : Decidable (x✝ = x✝¹)

Equations

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

def Verb.Root.instBEqProfile.beq : Profile → Profile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Verb.Root.instBEqProfile.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Verb.Root.instBEqProfile : BEq Profile

Equations

• Verb.Root.instBEqProfile = { beq := Verb.Root.instBEqProfile.beq }

@[implicit_reducible]

instance Verb.Root.instReprProfile : Repr Profile

Equations

• Verb.Root.instReprProfile = { reprPrec := Verb.Root.instReprProfile.repr }

def Verb.Root.instReprProfile.repr : Profile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Verb.Root.instInhabitedProfile : Inhabited Profile

Equations

• Verb.Root.instInhabitedProfile = { default := Verb.Root.instInhabitedProfile.default }

def Verb.Root.Profile.constrainsPatient (rp : Profile) : Prop

Does a root profile constrain patient properties?

Equations

• rp.constrainsPatient = (rp.patientRob.isConstrained = true)

@[implicit_reducible]

instance Verb.Root.Profile.instDecidableConstrainsPatient (rp : Profile) : Decidable rp.constrainsPatient

Equations

• rp.instDecidableConstrainsPatient = Verb.Root.Profile.instDecidableConstrainsPatient._aux_1 rp

def Verb.Root.Profile.overlaps (rp₁ rp₂ : Profile) : Prop

Do two root profiles overlap (share at least one compatible event)?

Equations

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

@[implicit_reducible]

instance Verb.Root.Profile.instDecidableOverlaps (rp₁ rp₂ : Profile) : Decidable (rp₁.overlaps rp₂)

Equations

• rp₁.instDecidableOverlaps rp₂ = Verb.Root.Profile.instDecidableOverlaps._aux_1 rp₁ rp₂