Root Quality Dimensions and Structural Entailments

@cite{talmy-1988} @cite{talmy-2000} @cite{dowty-1991} @cite{beavers-koontz-garboden-2020} @cite{majid-boster-bowerman-2008}

Per-root content typology: ranges over root quality dimensions, the @cite{beavers-koontz-garboden-2020} (B&KG) binary entailment tetrad, and Marantz-style root structural position.

Provenance

Moved from Core/Lexical/RootFeatures.lean in the cleanup that dissolved Core/Lexical/. The file's original docstring claimed "framework-agnostic infrastructure" but its load-bearing content (B&KG's binary [state, manner, result, cause] tetrad in §3, Marantz's complement-vs-adjunct merge position in §4) is framework-specific: B&KG's tetrad is the thesis of @cite{beavers-koontz-garboden-2020}, explicitly opposed to Rappaport Hovav & Levin's template-based account (@cite{rappaport-hovav-levin-2010}) and to Embick's contextual-allosemy framework. Promoting these features to a named Theories file (sibling of Roots/Basic.lean, Roots/Typology.lean, Roots/Template.lean) makes the framework commitment legible.

Sibling slots intentionally unfilled. Theories/Semantics/Lexical/Roots/RappaportHovavLevin.lean is the natural home for the template-based competitor account (@cite{rappaport-hovav-levin-2010}, @cite{rappaport-hovav-levin-2024}). @cite{rappaport-hovav-levin-2010} reject the very feature setup encoded here; their position is that manner/result are event-structural templates, not root features. The slot is empty in this restructure; future work formalizing RH&L's framework should land there as a sibling, with refutation theorems showing where B&KG and RH&L disagree on attested verbs.

Sections

• §1 Range mechanism — Range α := Option (List α) for within-class variation
• §2 Quality dimensions — force, robustness, instrument, dimensionality, agent properties
• §3 B&KG root structural entailments — state/manner/result/cause + collocational constraints
• §4 Marantz root structural position — complement vs adjunct of v
• §5 Derived properties on RootProfile

Citation hygiene notes

• B&KG page references (e.g., "Table 12, p. 228", "p. 229") are flagged UNVERIFIED: per CLAUDE.md ("Never cite specific page ranges from memory"). Verify against the published @cite{beavers-koontz-garboden-2020} monograph before treating as authoritative.
• Inline Marantz (2009a;b, 2013) references in the original file lacked bib entries. The substantive claim — that roots merge as complement or adjunct of v — is uncontroversially attributed to Marantz across the DM literature, but the specific publication citations need verification before adding to references.bib.

@[reducible, inline]

abbrev Semantics.Lexical.Roots.Range (α : Type) : Type

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

• Semantics.Lexical.Roots.Range α = Option (List α)

def Semantics.Lexical.Roots.Range.unconstrained {α : Type} : Range α

Equations

• Semantics.Lexical.Roots.Range.unconstrained = none

def Semantics.Lexical.Roots.Range.only {α : Type} (vs : List α) : Range α

Equations

• Semantics.Lexical.Roots.Range.only vs = some vs

def Semantics.Lexical.Roots.Range.isCompatible {α : Type} [BEq α] : Range α → α → Bool

Equations

• Semantics.Lexical.Roots.Range.isCompatible none x✝ = true
• Semantics.Lexical.Roots.Range.isCompatible (some vs) x✝ = vs.contains x✝

def Semantics.Lexical.Roots.Range.isConstrained {α : Type} : Range α → Bool

Equations

• Semantics.Lexical.Roots.Range.isConstrained none = false
• Semantics.Lexical.Roots.Range.isConstrained (some val) = true

def Semantics.Lexical.Roots.Range.overlaps {α : Type} [BEq α] : Range α → Range α → Bool

Two ranges overlap if they share at least one value.

Equations

• Semantics.Lexical.Roots.Range.overlaps none x✝ = true
• x✝.overlaps none = true
• Semantics.Lexical.Roots.Range.overlaps (some vs₁) (some vs₂) = vs₁.any fun (x : α) => vs₂.contains x

inductive Semantics.Lexical.Roots.ForceLevel : Type

Magnitude of force involved in the event.

@cite{talmy-1988} identifies force magnitude as a core parameter of force-dynamic schemas. @cite{spalek-mcnally-2026}: tear implies considerable force; rasgar implies less (enough to damage something flimsy).

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqForceLevel : DecidableEq ForceLevel

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprForceLevel : Repr ForceLevel

Equations

• Semantics.Lexical.Roots.instReprForceLevel = { reprPrec := Semantics.Lexical.Roots.instReprForceLevel.repr }

def Semantics.Lexical.Roots.instReprForceLevel.repr : ForceLevel → Nat → Std.Format

Equations

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

inductive Semantics.Lexical.Roots.ForceDirection : Type

Spatial pattern of force application.

@cite{talmy-2000}: force vectors have directional parameters. @cite{spalek-mcnally-2026}: tear implies contrary-direction force (pulling apart); rasgar implies unidirectional force (gash-like).

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqForceDirection : DecidableEq ForceDirection

Equations

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

def Semantics.Lexical.Roots.instReprForceDirection.repr : ForceDirection → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprForceDirection : Repr ForceDirection

Equations

• Semantics.Lexical.Roots.instReprForceDirection = { reprPrec := Semantics.Lexical.Roots.instReprForceDirection.repr }

inductive Semantics.Lexical.Roots.Robustness : Type

Material substantiality of the affected entity (patient).

@cite{spalek-mcnally-2026}: the primary dimension distinguishing tear (unrestricted) from rasgar (flimsy patients only).

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqRobustness : DecidableEq Robustness

Equations

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

def Semantics.Lexical.Roots.instReprRobustness.repr : Robustness → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprRobustness : Repr Robustness

Equations

• Semantics.Lexical.Roots.instReprRobustness = { reprPrec := Semantics.Lexical.Roots.instReprRobustness.repr }

inductive Semantics.Lexical.Roots.ResultType : Type

Nature of the physical change produced by the event.

Grounded in @cite{levin-1993}'s class descriptions and @cite{hale-keyser-1987} 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 @cite{beavers-koontz-garboden-2020} 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 Semantics.Lexical.Roots.instDecidableEqResultType : DecidableEq ResultType

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprResultType : Repr ResultType

Equations

• Semantics.Lexical.Roots.instReprResultType = { reprPrec := Semantics.Lexical.Roots.instReprResultType.repr }

def Semantics.Lexical.Roots.instReprResultType.repr : ResultType → Nat → Std.Format

Equations

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

inductive Semantics.Lexical.Roots.InstrumentType : Type

Type of instrument used in the event.

@cite{majid-boster-bowerman-2008}: 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.

@cite{levin-1993}: 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 Semantics.Lexical.Roots.instDecidableEqInstrumentType : DecidableEq InstrumentType

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprInstrumentType : Repr InstrumentType

Equations

• Semantics.Lexical.Roots.instReprInstrumentType = { reprPrec := Semantics.Lexical.Roots.instReprInstrumentType.repr }

def Semantics.Lexical.Roots.instReprInstrumentType.repr : InstrumentType → Nat → Std.Format

Equations

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

inductive Semantics.Lexical.Roots.ObjectDimensionality : Type

Dimensionality of the affected object (patient).

@cite{majid-boster-bowerman-2008}: 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 Semantics.Lexical.Roots.instDecidableEqObjectDimensionality : DecidableEq ObjectDimensionality

Equations

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

def Semantics.Lexical.Roots.instReprObjectDimensionality.repr : ObjectDimensionality → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprObjectDimensionality : Repr ObjectDimensionality

Equations

• Semantics.Lexical.Roots.instReprObjectDimensionality = { reprPrec := Semantics.Lexical.Roots.instReprObjectDimensionality.repr }

inductive Semantics.Lexical.Roots.Volitionality : Type

Whether the agent acts with volitional intent.

@cite{dowty-1991}: Proto-Agent entailment P1 = "volitional involvement in the event or state." @cite{ausensi-yu-smith-2021}: killing verb roots impose specific intentionality requirements on the agent (murder requires intentional agent; kill does not). @cite{levin-1993}: some break verbs "allow unintentional, action interpretations with body-part objects."

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqVolitionality : DecidableEq Volitionality

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprVolitionality : Repr Volitionality

Equations

• Semantics.Lexical.Roots.instReprVolitionality = { reprPrec := Semantics.Lexical.Roots.instReprVolitionality.repr }

def Semantics.Lexical.Roots.instReprVolitionality.repr : Volitionality → Nat → Std.Format

Equations

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

inductive Semantics.Lexical.Roots.AgentControl : Type

Whether the action can be performed with care and control.

@cite{dowty-1991}: Proto-Agent entailment P2 = "sentience (and/or perception)," enabling controlled action. @cite{spalek-mcnally-2026}: 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 Semantics.Lexical.Roots.instDecidableEqAgentControl : DecidableEq AgentControl

Equations

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

def Semantics.Lexical.Roots.instReprAgentControl.repr : AgentControl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprAgentControl : Repr AgentControl

Equations

• Semantics.Lexical.Roots.instReprAgentControl = { reprPrec := Semantics.Lexical.Roots.instReprAgentControl.repr }

structure Semantics.Lexical.Roots.RootProfile : Type

Within-class root content profile.

Captures quality dimensions of root content — force, robustness, agent properties — as opposed to RootEntailments (§ 3), 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).

Together with MeaningComponents (which defines the class), LevinClass (which identifies the class), and RootEntailments (which captures structural entailments), this gives a four-level characterization of a verb's semantic content:

1. Class-defining meaning components (binary, from alternations)
2. Class membership (Levin taxonomy)
3. Root structural entailments (@cite{beavers-koontz-garboden-2020})
4. Root-specific quality features (ranges, from detailed lexical analysis)

• forceMag : Range ForceLevel

  Force magnitude: @cite{talmy-1988}.

• forceDir : Range ForceDirection

  Force directionality: @cite{talmy-2000}, @cite{spalek-mcnally-2026}.

• patientRob : Range Robustness

  Patient material robustness: @cite{spalek-mcnally-2026}.

• resultType : Range ResultType

  Type of physical change: @cite{levin-1993}, @cite{beavers-koontz-garboden-2020}.

• agentVolition : Range Volitionality

  Agent volitionality: @cite{dowty-1991} P1, @cite{ausensi-yu-smith-2021}.

• agentControl : Range AgentControl

  Agent control: @cite{dowty-1991} P2, @cite{spalek-mcnally-2026}.

• instrumentType : Range InstrumentType

  Instrument type the root selects for: @cite{majid-boster-bowerman-2008}. cut selects for sharp blades; break is unspecified.

• patientDim : Range ObjectDimensionality

  Patient dimensionality: @cite{majid-boster-bowerman-2008}. tear selects for 2D objects (cloth, paper); snap for 1D (stick, twig).

def Semantics.Lexical.Roots.instBEqRootProfile.beq : RootProfile → RootProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Roots.instBEqRootProfile.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Semantics.Lexical.Roots.instBEqRootProfile : BEq RootProfile

Equations

• Semantics.Lexical.Roots.instBEqRootProfile = { beq := Semantics.Lexical.Roots.instBEqRootProfile.beq }

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprRootProfile : Repr RootProfile

Equations

• Semantics.Lexical.Roots.instReprRootProfile = { reprPrec := Semantics.Lexical.Roots.instReprRootProfile.repr }

def Semantics.Lexical.Roots.instReprRootProfile.repr : RootProfile → Nat → Std.Format

Equations

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

def Semantics.Lexical.Roots.instInhabitedRootProfile.default : RootProfile

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instInhabitedRootProfile : Inhabited RootProfile

Equations

• Semantics.Lexical.Roots.instInhabitedRootProfile = { default := Semantics.Lexical.Roots.instInhabitedRootProfile.default }

structure Semantics.Lexical.Roots.RootEntailments : Type

Root-level structural entailments from @cite{beavers-koontz-garboden-2020}.

B&KG argue against Bifurcation (roots only contribute idiosyncratic content) and Manner/Result Complementarity (no root encodes both). Roots CAN entail states, change, and causation — notions traditionally reserved for templates (CAUSE, BECOME).

The four features define a root typology:

• state: root describes a state (√FLAT, √CRACK, √DRY)
• manner: root describes an action/manner (√JOG, √RUN, √HIT)
• result: root entails change — passes restitutive again test
• cause: root entails causation

Constraints: result → state and cause → result (see WellFormed).

@cite{rappaport-hovav-levin-2010} reject this entailment-feature framing; for them manner/result are event-structural template properties, not root features. The competitor analysis would live in Theories/Semantics/Lexical/Roots/RappaportHovavLevin.lean (planned).

UNVERIFIED: B&KG Table 12 reference cited from memory.

• state : Bool
• manner : Bool
• result : Bool
• cause : Bool

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqRootEntailments : DecidableEq RootEntailments

Equations

• Semantics.Lexical.Roots.instDecidableEqRootEntailments = Semantics.Lexical.Roots.instDecidableEqRootEntailments.decEq

def Semantics.Lexical.Roots.instDecidableEqRootEntailments.decEq (x✝ x✝¹ : RootEntailments) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Lexical.Roots.instReprRootEntailments.repr : RootEntailments → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprRootEntailments : Repr RootEntailments

Equations

• Semantics.Lexical.Roots.instReprRootEntailments = { reprPrec := Semantics.Lexical.Roots.instReprRootEntailments.repr }

def Semantics.Lexical.Roots.RootEntailments.ResultImpliesState (r : RootEntailments) : Prop

If a root entails change (result), it entails a state that changes. @cite{beavers-koontz-garboden-2020}: result entailments presuppose state entailments.

Equations

• r.ResultImpliesState = (r.result = true → r.state = true)

@[implicit_reducible]

instance Semantics.Lexical.Roots.RootEntailments.instDecidableResultImpliesState (r : RootEntailments) : Decidable r.ResultImpliesState

Equations

• r.instDecidableResultImpliesState = id inferInstance

def Semantics.Lexical.Roots.RootEntailments.CauseImpliesResult (r : RootEntailments) : Prop

If a root entails causation, it entails what is caused (a result). @cite{beavers-koontz-garboden-2020}: cause entailments presuppose result entailments.

Equations

• r.CauseImpliesResult = (r.cause = true → r.result = true)

@[implicit_reducible]

instance Semantics.Lexical.Roots.RootEntailments.instDecidableCauseImpliesResult (r : RootEntailments) : Decidable r.CauseImpliesResult

Equations

• r.instDecidableCauseImpliesResult = id inferInstance

def Semantics.Lexical.Roots.RootEntailments.WellFormed (r : RootEntailments) : Prop

Well-formedness: both collocational constraints hold.

Equations

• r.WellFormed = (r.ResultImpliesState ∧ r.CauseImpliesResult)

@[implicit_reducible]

instance Semantics.Lexical.Roots.RootEntailments.instDecidableWellFormed (r : RootEntailments) : Decidable r.WellFormed

Equations

• r.instDecidableWellFormed = id inferInstance

Canonical root types

UNVERIFIED: Specific row references to @cite{beavers-koontz-garboden-2020} Table 12 are cited from memory. The 7 canonical types below cover B&KG's typology; verify row numbers against the published monograph before treating as definitive.

def Semantics.Lexical.Roots.RootEntailments.propertyConcept : RootEntailments

+S −M −R −C: property concept roots (√FLAT, √DRY). Deadjectival COS verbs — the root names the result state. Complement position.

Equations

• Semantics.Lexical.Roots.RootEntailments.propertyConcept = { state := true, manner := false, result := false, cause := false }

def Semantics.Lexical.Roots.RootEntailments.pureResult : RootEntailments

+S −M +R −C: internally caused result roots (√BLOSSOM, √RUST). Root entails both a state and a change to that state, but not external causation. Complement position.

Equations

• Semantics.Lexical.Roots.RootEntailments.pureResult = { state := true, manner := false, result := true, cause := false }

def Semantics.Lexical.Roots.RootEntailments.causativeResult : RootEntailments

+S −M +R +C: externally caused result roots (√CRACK, √BREAK). Root entails a state, change, AND causation — the root inherently implies an external cause. Complement position. @cite{beavers-koontz-garboden-2020}: these "lexicalize crosslinguistically as basic causatives" unlike √BLOSSOM-type roots.

Equations

• Semantics.Lexical.Roots.RootEntailments.causativeResult = { state := true, manner := false, result := true, cause := true }

def Semantics.Lexical.Roots.RootEntailments.pureManner : RootEntailments

−S +M −R −C: pure manner roots (√JOG, √RUN, √SWIM). Root specifies action manner without entailing any state. Adjoined position.

Equations

• Semantics.Lexical.Roots.RootEntailments.pureManner = { state := false, manner := true, result := false, cause := false }

def Semantics.Lexical.Roots.RootEntailments.mannerResult : RootEntailments

+S +M +R −C: manner + result without cause. Well-formed per the constraints but UNATTESTED in B&KG's typology. Such roots "would essentially derive syntactically unergative verbs with pure change-of-state meanings." Defined for completeness.

Equations

• Semantics.Lexical.Roots.RootEntailments.mannerResult = { state := true, manner := true, result := true, cause := false }

def Semantics.Lexical.Roots.RootEntailments.fullSpec : RootEntailments

+S +M +R +C: fully specified roots (√HAND, √DROWN, √CUT). @cite{beavers-koontz-garboden-2020} Ch. 3–4: manner + caused change. These are the attested MRC violators. √HAND sits in adjoined position, √DROWN in complement position; this structural difference is not captured here.

Equations

• Semantics.Lexical.Roots.RootEntailments.fullSpec = { state := true, manner := true, result := true, cause := true }

def Semantics.Lexical.Roots.RootEntailments.minimal : RootEntailments

−S −M −R −C: minimal roots — no structural entailments. Conservative default for classes not yet studied under B&KG's framework. Not a row in B&KG's typology (which only lists roots with at least one positive feature).

Equations

• Semantics.Lexical.Roots.RootEntailments.minimal = { state := false, manner := false, result := false, cause := false }

Canonical type well-formedness

theorem Semantics.Lexical.Roots.RootEntailments.propertyConcept_wf : propertyConcept.WellFormed

theorem Semantics.Lexical.Roots.RootEntailments.pureResult_wf : pureResult.WellFormed

theorem Semantics.Lexical.Roots.RootEntailments.causativeResult_wf : causativeResult.WellFormed

theorem Semantics.Lexical.Roots.RootEntailments.pureManner_wf : pureManner.WellFormed

theorem Semantics.Lexical.Roots.RootEntailments.mannerResult_wf : mannerResult.WellFormed

theorem Semantics.Lexical.Roots.RootEntailments.fullSpec_wf : fullSpec.WellFormed

theorem Semantics.Lexical.Roots.RootEntailments.minimal_wf : minimal.WellFormed

MRC violation detection

def Semantics.Lexical.Roots.RootEntailments.ViolatesMRC (r : RootEntailments) : Prop

Does this root violate Manner/Result Complementarity? @cite{beavers-koontz-garboden-2020} Ch. 4: some roots encode both manner and result. @cite{rappaport-hovav-levin-2010} dispute this; the framing "violates MRC" presupposes MRC as a baseline norm — itself a framework commitment.

Equations

• r.ViolatesMRC = (r.manner = true ∧ r.result = true)

@[implicit_reducible]

instance Semantics.Lexical.Roots.RootEntailments.instDecidableViolatesMRC (r : RootEntailments) : Decidable r.ViolatesMRC

Equations

• r.instDecidableViolatesMRC = id inferInstance

theorem Semantics.Lexical.Roots.RootEntailments.fullSpec_violates_MRC : fullSpec.ViolatesMRC

theorem Semantics.Lexical.Roots.RootEntailments.mannerResult_violates_MRC : mannerResult.ViolatesMRC

theorem Semantics.Lexical.Roots.RootEntailments.pureResult_respects_MRC : ¬pureResult.ViolatesMRC

theorem Semantics.Lexical.Roots.RootEntailments.pureManner_respects_MRC : ¬pureManner.ViolatesMRC

theorem Semantics.Lexical.Roots.RootEntailments.causativeResult_respects_MRC : ¬causativeResult.ViolatesMRC

inductive Semantics.Lexical.Roots.RootPosition : Type

Structural attachment position of a verb root. Following the Distributed-Morphology tradition (Marantz; systematized by @cite{beavers-koontz-garboden-2020}):

• Complement: root merges as complement of v (inside VP). Fills the result-state slot. Change-of-state roots: √FLAT, √CRACK, √BLOSSOM, √DROWN.
• Adjoined: root merges as adjunct to v (outside VP). Modifies the causing event. Manner/activity roots: √JOG, √TOSS, √HAND.

This distinction is structurally significant beyond root typology: it determines vVPE eligibility (@cite{kalyakin-2026}), scope of result-state modifiers, and the restitutive/repetitive again ambiguity (@cite{beavers-koontz-garboden-2020}, @cite{merchant-2013}).

UNVERIFIED: The Marantz publications usually cited in this context (DM "Phases and words" handout, "No Escape from Syntax", "Verbal argument structure" chapter) have not been added to references.bib. The substantive claim is uncontroversially attributed to Marantz across DM, but specific publication references should be verified before citing.

Note: this is the canonical RootPosition for the Roots/ subdirectory; Template.lean will be updated in the same restructure commit to drop its local duplicate def and import from here.

• complement : RootPosition
• adjoined : RootPosition

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqRootPosition : DecidableEq RootPosition

Equations

• Semantics.Lexical.Roots.instDecidableEqRootPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Roots.instReprRootPosition.repr : RootPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprRootPosition : Repr RootPosition

Equations

• Semantics.Lexical.Roots.instReprRootPosition = { reprPrec := Semantics.Lexical.Roots.instReprRootPosition.repr }

def Semantics.Lexical.Roots.RootProfile.constrainsPatient (rp : RootProfile) : Prop

Does a root profile constrain patient properties?

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableConstrainsPatient (rp : RootProfile) : Decidable rp.constrainsPatient

Equations

• Semantics.Lexical.Roots.instDecidableConstrainsPatient rp = Semantics.Lexical.Roots.instDecidableConstrainsPatient._aux_1 rp

def Semantics.Lexical.Roots.RootProfile.overlaps (rp₁ rp₂ : RootProfile) : 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 Semantics.Lexical.Roots.instDecidableOverlaps (rp₁ rp₂ : RootProfile) : Decidable (rp₁.overlaps rp₂)

Equations

• Semantics.Lexical.Roots.instDecidableOverlaps rp₁ rp₂ = Semantics.Lexical.Roots.instDecidableOverlaps._aux_1 rp₁ rp₂