[Bea10] The Structure of Lexical Meaning: Why Semantics Really Matters

Argument realization in direct/oblique alternations is governed not by event structure but by strength of truth conditions. Direct realization encodes monotonically stronger truth conditions than oblique realization. This is captured by:

1. An affectedness hierarchy — four degrees of change, each an existential weakening of the last: quantized ⊃ nonquantized ⊃ potential ⊃ unspecified.

2. L-thematic roles — sets of implicationally related entailments. The three affectedness entailments produce a structured subset hierarchy with exactly 4 semantically non-vacuous roles (of 8 possible).

3. The Morphosyntactic Alignment Principle (MAP) — when an argument alternates between direct and oblique realization, the direct variant bears L-thematic role R and the oblique bears Q ⊆_M R (minimal weakening).

Deepest theorem

MAP_holds_all_alternations: for every attested object/oblique alternation in the data, the oblique role is the next-weakest (minimal, ⊆_M) weakening of the direct role. The subset form (direct degree ≥ oblique degree) is the derived corollary MAP_subset / MapHolds.oblique_le, via the substrate's AffectednessDegree order.

structure Beavers2010.PatientLRole : Type

An L-thematic role for patienthood: a set of the three affectedness entailments ([Bea10]'s reduction of Dowty's 5 P-Patient entailments).

• quantized : Bool
• nonquantized : Bool
• potential : Bool

@[implicit_reducible]

instance Beavers2010.instDecidableEqPatientLRole : DecidableEq PatientLRole

Equations

• Beavers2010.instDecidableEqPatientLRole = Beavers2010.instDecidableEqPatientLRole.decEq

def Beavers2010.instDecidableEqPatientLRole.decEq (x✝ x✝¹ : PatientLRole) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Beavers2010.instReprPatientLRole : Repr PatientLRole

Equations

• Beavers2010.instReprPatientLRole = { reprPrec := Beavers2010.instReprPatientLRole.repr }

def Beavers2010.instReprPatientLRole.repr : PatientLRole → ℕ → Std.Format

Equations

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

def Beavers2010.PatientLRole.valid (r : PatientLRole) : Bool

An L-role is valid iff it respects the implicational chain quantized → nonquantized → potential.

Equations

• r.valid = ((!r.quantized || r.nonquantized) && (!r.nonquantized || r.potential))

def Beavers2010.PatientLRole.quantizedRole : PatientLRole

The four valid L-thematic roles.

Equations

• Beavers2010.PatientLRole.quantizedRole = { quantized := true, nonquantized := true, potential := true }

def Beavers2010.PatientLRole.nonquantizedRole : PatientLRole

Equations

• Beavers2010.PatientLRole.nonquantizedRole = { quantized := false, nonquantized := true, potential := true }

def Beavers2010.PatientLRole.potentialRole : PatientLRole

Equations

• Beavers2010.PatientLRole.potentialRole = { quantized := false, nonquantized := false, potential := true }

def Beavers2010.PatientLRole.unspecifiedRole : PatientLRole

Equations

• Beavers2010.PatientLRole.unspecifiedRole = { quantized := false, nonquantized := false, potential := false }

theorem Beavers2010.PatientLRole.exactly_four_valid_roles (r : PatientLRole) : r.valid = true ↔ r = quantizedRole ∨ r = nonquantizedRole ∨ r = potentialRole ∨ r = unspecifiedRole

Exactly 4 of the 8 combinations are valid: the implicational chain prunes the role space to the four semantically contentful L-roles.

def Beavers2010.PatientLRole.subset (r₁ r₂ : PatientLRole) : Bool

Subset ordering on L-thematic roles: R₁ ⊆ R₂ iff every entailment in R₁ is also in R₂.

Equations

• r₁.subset r₂ = ((!r₁.quantized || r₂.quantized) && (!r₁.nonquantized || r₂.nonquantized) && (!r₁.potential || r₂.potential))

def Beavers2010.PatientLRole.strictSubset (r₁ r₂ : PatientLRole) : Bool

Strict subset: ⊂

Equations

• r₁.strictSubset r₂ = (r₁.subset r₂ && !r₂.subset r₁)

theorem Beavers2010.PatientLRole.valid_roles_form_chain : unspecifiedRole.strictSubset potentialRole = true ∧ potentialRole.strictSubset nonquantizedRole = true ∧ nonquantizedRole.strictSubset quantizedRole = true

The four valid roles form a linear chain under ⊂: {} ⊂ {p} ⊂ {nq,p} ⊂ {q,nq,p}

theorem Beavers2010.PatientLRole.no_incomparable_valid_pairs : unspecifiedRole.subset potentialRole = true ∧ unspecifiedRole.subset nonquantizedRole = true ∧ unspecifiedRole.subset quantizedRole = true ∧ potentialRole.subset nonquantizedRole = true ∧ potentialRole.subset quantizedRole = true ∧ nonquantizedRole.subset quantizedRole = true

The hierarchy is linear: no incomparable pairs among valid roles.

def Beavers2010.PatientLRole.minimalContrast (q r : PatientLRole) : Bool

Minimal contrast: Q ⊆_M R iff Q = R or Q ⊂ R with no valid role strictly between them.

Equations

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

theorem Beavers2010.PatientLRole.minimal_contrasts_are_adjacent : unspecifiedRole.minimalContrast potentialRole = true ∧ potentialRole.minimalContrast nonquantizedRole = true ∧ nonquantizedRole.minimalContrast quantizedRole = true

The attested minimal contrasts are exactly the adjacent pairs.

theorem Beavers2010.PatientLRole.skip_not_minimal : unspecifiedRole.minimalContrast nonquantizedRole = false ∧ unspecifiedRole.minimalContrast quantizedRole = false ∧ potentialRole.minimalContrast quantizedRole = false

Skipping a level is NOT a minimal contrast.

def Beavers2010.PatientLRole.toDegree (r : PatientLRole) : ArgumentStructure.Affectedness.AffectednessDegree

The affectedness degree corresponding to a valid L-thematic role.

Equations

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

def Beavers2010.PatientLRole.ofDegree : ArgumentStructure.Affectedness.AffectednessDegree → PatientLRole

The valid L-thematic role realizing a degree (section of toDegree).

Equations

• Beavers2010.PatientLRole.ofDegree ArgumentStructure.Affectedness.AffectednessDegree.quantized = Beavers2010.PatientLRole.quantizedRole
• Beavers2010.PatientLRole.ofDegree ArgumentStructure.Affectedness.AffectednessDegree.nonquantized = Beavers2010.PatientLRole.nonquantizedRole
• Beavers2010.PatientLRole.ofDegree ArgumentStructure.Affectedness.AffectednessDegree.potential = Beavers2010.PatientLRole.potentialRole
• Beavers2010.PatientLRole.ofDegree ArgumentStructure.Affectedness.AffectednessDegree.unspecified = Beavers2010.PatientLRole.unspecifiedRole

theorem Beavers2010.PatientLRole.ofDegree_valid (d : ArgumentStructure.Affectedness.AffectednessDegree) : (ofDegree d).valid = true

theorem Beavers2010.PatientLRole.toDegree_ofDegree (d : ArgumentStructure.Affectedness.AffectednessDegree) : (ofDegree d).toDegree = d

theorem Beavers2010.PatientLRole.subset_iff_toDegree_le (q r : PatientLRole) : q.valid = true → r.valid = true → (q.subset r = true ↔ q.toDegree ≤ r.toDegree)

The subset order on valid roles is the substrate's AffectednessDegree order, transported along toDegree.

def Beavers2010.MAP (directRole obliqueRole : PatientLRole) : Bool

The MAP ([Bea10]; canonical wording in Beavers' 2023 Sag Lectures handout): when an argument may be either an object or a PP, it bears role R as an object and the next weakest role Q ⊆_M R as a PP — a minimal weakening, not mere subset.

Equations

• Beavers2010.MAP directRole obliqueRole = obliqueRole.minimalContrast directRole

theorem Beavers2010.MAP_subset (d o : PatientLRole) : MAP d o = true → o.subset d = true

Derived corollary of the MAP (the weakened form an earlier version of this file stated as the MAP itself): the oblique role's entailments are a subset of the direct role's.

theorem Beavers2010.skip_violates_MAP : MAP PatientLRole.quantizedRole PatientLRole.potentialRole = false ∧ PatientLRole.potentialRole.subset PatientLRole.quantizedRole = true

The case the strengthening excludes: a level-skipping weakening (potential oblique under a quantized direct role) satisfies the subset corollary but violates the MAP proper.

structure Beavers2010.AlternationContrast : Type

An observed alternation contrast: a verb with its direct-object and oblique affectedness degrees.

• verb : String
• alternationType : Semantics.Lexical.DiathesisAlternation
• directDegree : ArgumentStructure.Affectedness.AffectednessDegree
• obliqueDegree : ArgumentStructure.Affectedness.AffectednessDegree

def Beavers2010.instReprAlternationContrast.repr : AlternationContrast → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Beavers2010.instReprAlternationContrast : Repr AlternationContrast

Equations

• Beavers2010.instReprAlternationContrast = { reprPrec := Beavers2010.instReprAlternationContrast.repr }

def Beavers2010.instBEqAlternationContrast.beq : AlternationContrast → AlternationContrast → Bool

Equations

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

@[implicit_reducible]

instance Beavers2010.instBEqAlternationContrast : BEq AlternationContrast

Equations

• Beavers2010.instBEqAlternationContrast = { beq := Beavers2010.instBEqAlternationContrast.beq }

def Beavers2010.eatConative : AlternationContrast

eat conative: "ate the pizza" (quantized) vs "ate at the pizza" (nonquantized). The object variant entails total consumption; the oblique entails only some consumption occurred.

Equations

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

def Beavers2010.cutConative : AlternationContrast

cut conative: "cut the rope" (nonquantized) vs "cut at the rope" (potential). The object variant entails some damage; the oblique entails only that damage was possible (contact under modality).

Equations

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

def Beavers2010.hitConative : AlternationContrast

hit conative: "hit the rope" (potential) vs "hit at the rope" (unspecified). The object variant entails potential for change (if contact, then possible result); the oblique entails only potential contact under double modality.

Equations

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

def Beavers2010.loadLocation : AlternationContrast

load locative (location as object): "loaded the wagon" (quantized) vs "loaded hay onto the wagon" — the wagon undergoes quantized change (completely filled), the hay undergoes nonquantized change (moved).

Equations

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

def Beavers2010.loadTheme : AlternationContrast

load locative (theme as object): "loaded the hay" (quantized) vs "loaded the wagon with the hay" — the hay undergoes quantized change (all moved), the wagon undergoes nonquantized change.

Equations

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

def Beavers2010.cutLocation : AlternationContrast

cut/slice locative (location as object): "cut the window with the diamond" (nonquantized) vs "cut the diamond on the window" — both undergo potential change, but the object has nonquantized.

Equations

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

def Beavers2010.cutTheme : AlternationContrast

cut/slice locative (theme as object): same contrast.

Equations

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

def Beavers2010.allContrasts : List AlternationContrast

All attested alternation contrasts.

Equations

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

def Beavers2010.MapHolds (c : AlternationContrast) : Prop

The MAP holds of a contrast: the oblique role is the next-weakest (minimal) weakening of the direct role.

Equations

• Beavers2010.MapHolds c = (Beavers2010.MAP (Beavers2010.PatientLRole.ofDegree c.directDegree) (Beavers2010.PatientLRole.ofDegree c.obliqueDegree) = true)

@[implicit_reducible]

instance Beavers2010.instDecidableMapHolds (c : AlternationContrast) : Decidable (MapHolds c)

Equations

• Beavers2010.instDecidableMapHolds c = id inferInstance

theorem Beavers2010.MapHolds.oblique_le {c : AlternationContrast} (h : MapHolds c) : c.obliqueDegree ≤ c.directDegree

Degree-level corollary via MAP_subset and the substrate's AffectednessDegree order: the direct degree dominates the oblique.

theorem Beavers2010.MAP_eat_conative : MapHolds eatConative

theorem Beavers2010.MAP_cut_conative : MapHolds cutConative

theorem Beavers2010.MAP_hit_conative : MapHolds hitConative

theorem Beavers2010.MAP_load_location : MapHolds loadLocation

theorem Beavers2010.MAP_load_theme : MapHolds loadTheme

theorem Beavers2010.MAP_cut_location : MapHolds cutLocation

theorem Beavers2010.MAP_cut_theme : MapHolds cutTheme

theorem Beavers2010.MAP_holds_all_alternations (c : AlternationContrast) : c ∈ allContrasts → MapHolds c

The MAP — in its strengthened next-weakest form — holds for ALL attested alternation contrasts: every oblique realization is a minimal weakening of its direct counterpart.

theorem Beavers2010.conatives_cover_hierarchy : eatConative.directDegree = ArgumentStructure.Affectedness.AffectednessDegree.quantized ∧ eatConative.obliqueDegree = ArgumentStructure.Affectedness.AffectednessDegree.nonquantized ∧ cutConative.directDegree = ArgumentStructure.Affectedness.AffectednessDegree.nonquantized ∧ cutConative.obliqueDegree = ArgumentStructure.Affectedness.AffectednessDegree.potential ∧ hitConative.directDegree = ArgumentStructure.Affectedness.AffectednessDegree.potential ∧ hitConative.obliqueDegree = ArgumentStructure.Affectedness.AffectednessDegree.unspecified

The three conatives tile the hierarchy — every adjacent pair appears exactly once, so together they exhibit the full implicational chain. (That each is a minimal contrast is the per-contrast MAP_*_conative theorem above.)

def Beavers2010.impossibleConative : AlternationContrast

A hypothetical alternation whose oblique has more entailments than its direct object (potential DO, quantized oblique) — the less prominent realization would carry stronger truth conditions.

Equations

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

def Beavers2010.skippingLocative : AlternationContrast

A level-skipping alternation: quantized direct, potential oblique. Satisfies the subset corollary but not the MAP proper — the degree-level face of skip_violates_MAP.

Equations

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

def Beavers2010.reversedConative : AlternationContrast

A reversed alternation: the oblique strictly outranks the direct.

Equations

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

theorem Beavers2010.reversed_violates_MAP : ¬MapHolds reversedConative

theorem Beavers2010.impossible_violates_MAP : ¬MapHolds impossibleConative

theorem Beavers2010.skipping_violates_MAP : ¬MapHolds skippingLocative ∧ skippingLocative.obliqueDegree ≤ skippingLocative.directDegree

Skipping a level violates the MAP even though the degree order is respected — skip_not_minimal is what excludes it.

theorem Beavers2010.conative_data_attested : Levin1993.Examples.con_cut.judgment = Features.Judgment.acceptable ∧ Levin1993.Examples.con_hit.judgment = Features.Judgment.acceptable

Bridge to [Lev93]'s judgment rows: the conative alternation is attested for cut and hit, confirming the Table 3 contrasts.

theorem Beavers2010.break_no_conative : Levin1993.Examples.con_break.judgment = Features.Judgment.ungrammatical

Bridge to [Lev93]'s judgment rows: break does NOT participate in the conative. This is predicted: break objects undergo quantized change (CoS), and the conative would weaken to nonquantized — but break's meaning inherently requires a specific result state, so the weakening is blocked by the verb's lexical semantics.

theorem Beavers2010.locative_data_attested : Levin1993.Examples.loc_spray.judgment = Features.Judgment.acceptable ∧ Levin1993.Examples.loc_load.judgment = Features.Judgment.acceptable

Bridge to [Lev93]'s judgment rows: the locative alternation is attested for spray/load verbs, confirming the Table 4 contrasts.

The profileToDegree bridge (formerly §8) and its verification theorems have been promoted to Semantics/Events/Affectedness.lean. They are opened at the top of this file.

[Bea10] argues that the MAP and event decompositions are complementary, not competing (the paper's conclusion, §6):

| Approach        | Semantics                        | Morphosyntax             |
|-----------------|----------------------------------|--------------------------|
| Decompositions  | gross causal/temporal structure   | subject/nonsubject       |
| MAP             | fine-grained lexical entailments  | direct/oblique           |

The existing `EntailmentProfile` captures the gross agentivity structure
(P-Agent features → subject selection). Beavers 2010 adds the missing
piece: fine-grained P-Patient structure → direct/oblique alternations. 

theorem Beavers2010.asp_and_map_orthogonal : Features.LevinClassProfiles.mannerContact.subjectProfile.OutranksForSubject Features.LevinClassProfiles.contactObject ∧ ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.contactObject = ArgumentStructure.Affectedness.AffectednessDegree.potential ∧ Features.LevinClassProfiles.mannerContact.subjectProfile.pAgentScore > 0 ∧ Features.LevinClassProfiles.contactObject.pPatientScore > 0

Subject selection (from [Dow91]) and object alternations (from [Bea10]) are independent principles operating on different argument positions. The ASP governs subjects; the MAP governs direct vs. oblique objects.

[Gri11]'s PersistenceLevel reformulates P-Patient as 4 persistence dimensions (existential/qualitative × beginning/end). Beavers' affectedness hierarchy maps systematically onto this lattice:

| Beavers degree   | Grimm persistence    | Interpretation              |
|------------------|----------------------|-----------------------------|
| quantized        | exPersEnd            | Entity created/consumed     |
|                  | quPersBeginning      | Entity changed to specific  |
| nonquantized     | quPersBeginning      | Entity changed (nonspecific)|
| potential         | totalPersistence     | Entity may change           |
| unspecified       | totalPersistence     | No change entailment        |

The mapping is not injective: both `quantized` and `nonquantized` can
map to `quPersBeginning` (the entity changes but persists). The
distinction between them is about *specificity of the result state*,
which Grimm's persistence dimensions don't capture — it's a property
of the scale, not of persistence. This is where the theories are
genuinely complementary. 

def Beavers2010.degreeToPersistence : ArgumentStructure.Affectedness.AffectednessDegree → ArgumentStructure.AgentivityLattice.PersistenceLevel

Map affectedness degrees to their most typical persistence level. This captures the systematic correspondence; edge cases (creation verbs mapping to exPersEnd for quantized) require verb-specific information.

Equations

• Beavers2010.degreeToPersistence ArgumentStructure.Affectedness.AffectednessDegree.quantized = ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning
• Beavers2010.degreeToPersistence ArgumentStructure.Affectedness.AffectednessDegree.nonquantized = ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning
• Beavers2010.degreeToPersistence ArgumentStructure.Affectedness.AffectednessDegree.potential = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence
• Beavers2010.degreeToPersistence ArgumentStructure.Affectedness.AffectednessDegree.unspecified = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence

theorem Beavers2010.changed_lower_than_unaffected : ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning ≤ ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence

The two Grimm levels that correspond to "affected" roles (quPersBeginning = changed, exPersEnd = created/destroyed) are both ranked lower than totalPersistence on Grimm's lattice. Lower persistence = higher affectedness. This is the Grimm-Beavers convergence.

theorem Beavers2010.kick_grimm_beavers_consistent : ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.contactObject = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence ∧ ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.contactObject = ArgumentStructure.Affectedness.AffectednessDegree.potential

Bridge: kick object has persistence totalPersistence (persists, no entailed change) and affectedness potential — exactly the degreeToPersistence correspondence for potential change. Beavers' surface-contact classification ([Bea11] eq. (60c)); note [Gri11]'s own Fig. 5 instead places contact-verb objects at quPersBeginning (TransitivityRank.contact.patientNode), a genuine cross-paper disagreement over whether contact entails impingement.

theorem Beavers2010.build_grimm_beavers_consistent : ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.creationObject = ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd ∧ ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.creationObject = ArgumentStructure.Affectedness.AffectednessDegree.quantized

Bridge: build object has persistence exPersEnd (created) and affectedness quantized — both theories agree on maximal patient status.

theorem Beavers2010.eat_grimm_beavers_consistent : ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.consumptionObject = ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning ∧ ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.consumptionObject = ArgumentStructure.Affectedness.AffectednessDegree.quantized

Bridge: eat object has persistence exPersBeginning (consumed) and affectedness quantized — both theories agree on maximal change.

theorem Beavers2010.grimm_beavers_monotone_canonical : ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.contactObject = ArgumentStructure.Affectedness.AffectednessDegree.potential ∧ ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.contactObject = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence ∧ ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.creationObject = ArgumentStructure.Affectedness.AffectednessDegree.quantized ∧ ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.creationObject = ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd ∧ ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.perception.subjectProfile = ArgumentStructure.Affectedness.AffectednessDegree.unspecified ∧ ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.perception.subjectProfile = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence

The deepest cross-theory result: Grimm's persistence ordering and Beavers' affectedness ordering are monotonically related for canonical verb profiles. Arguments with higher affectedness (Beavers) have lower persistence (Grimm). They formalize the same intuition — degree of change — from complementary perspectives.

Cross-framework bridge from Levin/RHL ArgTemplate (event-template decomposition) to Grimm's GrimmNode (privative agentivity lattice) and Beavers' affectedness degree. Each canonical template is verified to project into the predicted positions in both systems, and the consistency of affectedness ↔ persistence is checked.

def Features.LevinClassProfiles.ArgTemplate.subjectGrimm (t : ArgTemplate) : ArgumentStructure.AgentivityLattice.GrimmNode

Project an ArgTemplate's subject profile to a GrimmNode.

Equations

• t.subjectGrimm = ArgumentStructure.AgentivityLattice.GrimmNode.fromSubjectProfile t.subjectProfile

def Features.LevinClassProfiles.ArgTemplate.objectGrimm (t : ArgTemplate) : Option ArgumentStructure.AgentivityLattice.GrimmNode

Project an ArgTemplate's object profile (if any) to a GrimmNode.

Equations

• t.objectGrimm = Option.map ArgumentStructure.AgentivityLattice.GrimmNode.fromObjectProfile t.objectProfile

def Features.LevinClassProfiles.ArgTemplate.objectAffectedness (t : ArgTemplate) : Option ArgumentStructure.Affectedness.AffectednessDegree

Project an ArgTemplate's object to its affectedness degree.

Equations

• t.objectAffectedness = Option.map ArgumentStructure.Affectedness.profileToDegree t.objectProfile

theorem Beavers2010.mannerContact_subject_grimm : Features.LevinClassProfiles.mannerContact.subjectGrimm.agentivity = ⊤

Manner-contact subject → full agent on the Grimm lattice.

theorem Beavers2010.mannerContact_object_affectedness : Features.LevinClassProfiles.mannerContact.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.potential

Manner-contact object → potential affectedness (no CoS entailed).

theorem Beavers2010.resultChange_object_affectedness : Features.LevinClassProfiles.resultChange.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.nonquantized

Result-change object → nonquantized affectedness (CoS, no IT).

theorem Beavers2010.creation_object_affectedness : Features.LevinClassProfiles.creation.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.quantized

Creation object → quantized affectedness (CoS + IT).

theorem Beavers2010.consumption_object_affectedness : Features.LevinClassProfiles.consumption.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.quantized

Consumption object → quantized affectedness (CoS + IT).

theorem Beavers2010.selfMotion_no_object : Features.LevinClassProfiles.selfMotion.objectAffectedness = none

Self-motion (intransitive) → no object affectedness.

theorem Beavers2010.template_affectedness_hierarchy : ArgumentStructure.Affectedness.AffectednessDegree.nonquantized ≤ ArgumentStructure.Affectedness.AffectednessDegree.quantized ∧ ArgumentStructure.Affectedness.AffectednessDegree.potential ≤ ArgumentStructure.Affectedness.AffectednessDegree.nonquantized ∧ Features.LevinClassProfiles.creation.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.quantized ∧ Features.LevinClassProfiles.resultChange.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.nonquantized ∧ Features.LevinClassProfiles.mannerContact.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.potential ∧ Features.LevinClassProfiles.perception.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.unspecified

Affectedness ordering across templates: the named templates are ordered by truth-conditional strength on the object side, reproducing [Bea10]'s hierarchy: creation/consumption (quantized) > resultChange (nonquantized) > mannerContact (potential) > perception (unspecified).

theorem Beavers2010.mannerContact_cross_projection : Features.LevinClassProfiles.mannerContact.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.potential ∧ Option.map ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.mannerContact.objectProfile = some ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence

The affectedness and persistence projections are consistent for manner-contact objects: potential affectedness ↔ totalPersistence (the object may change but the verb doesn't entail it).

theorem Beavers2010.resultChange_cross_projection : Features.LevinClassProfiles.resultChange.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.nonquantized ∧ Option.map ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.resultChange.objectProfile = some ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning

Result-change: nonquantized ↔ quPersBeginning (changed but persists).

theorem Beavers2010.creation_cross_projection : Features.LevinClassProfiles.creation.objectAffectedness = some ArgumentStructure.Affectedness.AffectednessDegree.quantized ∧ Option.map ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.creation.objectProfile = some ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd

Creation: quantized ↔ exPersEnd (entity comes into existence).