[Dow91] Thematic Proto-Roles and Argument Selection

Study file connecting the proto-role theory (Semantics/ArgumentStructure/EntailmentProfile.lean and the Levin-class template map, Semantics/Lexical/LevinClassProfiles.lean) to argument selection phenomena. The paper's explicit per-argument entailment attributions are typed data rows in Data/ProtoRoles/Dowty1991.json (generated module Data.ProtoRoles.Dowty1991), checked against the class templates in the final section — including the divergences the templates do NOT encode (build-object stationary, break-object incremental themehood, the eat-object dependent-existence tension).

Dowty's original flat-counting ASP

[Dow91]'s Argument Selection Principle uses flat counting: the argument with the greatest number of Proto-Agent entailments is subject. The library's default ASP uses lattice comparison ([Gri11], [davis-koenig-2000]), which handles priority and fixes anomalies like arrive. This study file preserves Dowty's original counting-based predictions to document where they succeed and where they diverge from the modern approach.

Key predictions formalized

• §9.1: Partially symmetric interactive predicates — volition as asymmetric P-Agent
• §9.2: Psych verb doublets — inchoative change-of-state breaks ties
• §9.3: Three verb classes (spray/load, break, hit) — CoS symmetry predicts alternation
• §12: Agentivity × telicity → unaccusativity (Table 1)

def Dowty1991.flatSelectsSubject (p : ArgumentStructure.EntailmentProfile) : Bool

[Dow91]'s original single-argument ASP (flat counting): an argument selects for subjecthood iff its P-Agent count exceeds its P-Patient count. Superseded by lattice-based OutranksForSubject in EntailmentProfile.lean.

Equations

• Dowty1991.flatSelectsSubject p = decide (p.pAgentScore > p.pPatientScore)

def Dowty1991.flatSelectsObject (p : ArgumentStructure.EntailmentProfile) : Bool

Equations

• Dowty1991.flatSelectsObject p = decide (p.pPatientScore > p.pAgentScore)

def Dowty1991.flatOutranksForSubject (arg1 arg2 : ArgumentStructure.EntailmentProfile) : Bool

[Dow91]'s between-argument comparison (flat counting): arg1 outranks arg2 for subjecthood iff arg1 has strictly more P-Agent entailments, OR they tie on P-Agent but arg2 has strictly more P-Patient entailments.

Equations

• Dowty1991.flatOutranksForSubject arg1 arg2 = (decide (arg1.pAgentScore > arg2.pAgentScore) || arg1.pAgentScore == arg2.pAgentScore && decide (arg2.pPatientScore > arg1.pPatientScore))

def Dowty1991.flatAllowsAlternation (arg1 arg2 : ArgumentStructure.EntailmentProfile) : Bool

Corollary 1 (flat counting): neither argument outranks the other → alternation.

Equations

• Dowty1991.flatAllowsAlternation arg1 arg2 = (!Dowty1991.flatOutranksForSubject arg1 arg2 && !Dowty1991.flatOutranksForSubject arg2 arg1)

def Dowty1991.flatPredictsUnaccusative (p : ArgumentStructure.EntailmentProfile) : Bool

[Dow91] Corollary 2 (flat counting): unaccusative iff pPatient > pAgent.

Equations

• Dowty1991.flatPredictsUnaccusative p = decide (p.pPatientScore > p.pAgentScore)

def Dowty1991.flatPredictsUnergative (p : ArgumentStructure.EntailmentProfile) : Bool

Complement: unergative iff pAgent > pPatient.

Equations

• Dowty1991.flatPredictsUnergative p = decide (p.pAgentScore > p.pPatientScore)

Verbs like kiss, embrace, marry denote actions requiring volitional involvement of two parties, but only the SUBJECT is entailed to be volitional. This single asymmetric P-Agent entailment predicts the transitive argument configuration.

def Dowty1991.kissSubjectProfile : ArgumentStructure.EntailmentProfile

"kiss" subject: V+M+IE — volitional, in motion, independently existing.

Equations

• Dowty1991.kissSubjectProfile = { volition := true, movement := true, independentExistence := true }

def Dowty1991.kissObjectProfile : ArgumentStructure.EntailmentProfile

"kiss" object: M+IE only — same minus volition.

Equations

• Dowty1991.kissObjectProfile = { movement := true, independentExistence := true }

theorem Dowty1991.kiss_subject_outranks : kissSubjectProfile.OutranksForSubject kissObjectProfile

The subject outranks the object (lattice: {V,M,IE} ⊃ {M,IE}).

theorem Dowty1991.kiss_subject_outranks_flat : flatOutranksForSubject kissSubjectProfile kissObjectProfile = true

Same result under Dowty's flat counting.

theorem Dowty1991.kiss_asymmetry_is_volition : kissSubjectProfile.pAgentScore = kissObjectProfile.pAgentScore + 1

Volition adds exactly 1 to the subject's P-Agent score.

theorem Dowty1991.kiss_collective_alternation : kissSubjectProfile.AllowsAlternation kissSubjectProfile

The collective intransitive ("Kim and Sandy kissed") is predicted: when both participants have symmetric volition, neither outranks.

Psych verbs come in doublets (like/please, fear/frighten) with reversed argument configurations. Under the stative reading, Experiencer and Stimulus have equal P-Agent scores → alternation is predicted.

theorem Dowty1991.psychStative_alternation : ThetaRole.experiencer.canonicalProfile.AllowsAlternation ThetaRole.stimulus.canonicalProfile

Stative: Experiencer and Stimulus have incomparable P-Agent sets ({S,IE} ⊥ {C,IE}) and equal P-Patient (both 0) → alternation.

def Dowty1991.expInchoativeProfile : ArgumentStructure.EntailmentProfile

Under inchoative interpretation, the Experiencer enters a new mental state → gains changeOfState (P-Patient entailment a).

Equations

• Dowty1991.expInchoativeProfile = { sentience := true, independentExistence := true, changeOfState := true }

def Dowty1991.stimProfile : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.stimProfile = ThetaRole.stimulus.canonicalProfile

theorem Dowty1991.psych_inchoative_stimulus_is_subject : stimProfile.OutranksForSubject expInchoativeProfile

Inchoative breaks the tie: Stimulus outranks Experiencer for subject because the Experiencer now has more P-Patient → Experiencer is a "better" object → Stimulus is subject. Predicts StimExp frame.

[Dow91] identifies three classes based on CoS distribution across non-subject arguments. When CoS is symmetric (both or neither), alternation is possible. When asymmetric, the CoS argument is fixed as DO. The comparison with [Lev93]'s alternation judgments lives in Studies/Levin1993.lean (dowty_* theorems).

def Dowty1991.cosSymmetric (arg1 arg2 : ArgumentStructure.EntailmentProfile) : Bool

Equations

• Dowty1991.cosSymmetric arg1 arg2 = (arg1.changeOfState == arg2.changeOfState)

def Dowty1991.sprayLoadTheme : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.sprayLoadTheme = { independentExistence := true, changeOfState := true, causallyAffected := true }

def Dowty1991.sprayLoadLocation : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.sprayLoadLocation = { independentExistence := true, changeOfState := true, causallyAffected := true, stationary := true }

theorem Dowty1991.sprayLoad_cos_symmetric : cosSymmetric sprayLoadTheme sprayLoadLocation = true

def Dowty1991.breakDirectObject : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.breakDirectObject = { changeOfState := true, incrementalTheme := true, causallyAffected := true, stationary := true }

def Dowty1991.breakInstrument : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.breakInstrument = { movement := true, independentExistence := true }

theorem Dowty1991.break_cos_asymmetric : cosSymmetric breakDirectObject breakInstrument = false

theorem Dowty1991.break_DO_more_patient : breakDirectObject.pPatientScore > breakInstrument.pPatientScore

def Dowty1991.hitArg1 : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.hitArg1 = { independentExistence := true, causallyAffected := true, stationary := true }

def Dowty1991.hitArg2 : ArgumentStructure.EntailmentProfile

Equations

• Dowty1991.hitArg2 = { movement := true, independentExistence := true, causallyAffected := true }

theorem Dowty1991.hit_cos_symmetric : cosSymmetric hitArg1 hitArg2 = true

theorem Dowty1991.hit_no_cos : hitArg1.changeOfState = false ∧ hitArg2.changeOfState = false

theorem Dowty1991.hit_no_IT : hitArg1.incrementalTheme = false ∧ hitArg2.incrementalTheme = false

[Dow91] Table 1: the interaction of agentivity (most salient P-Agent property) and telicity (most salient P-Patient property) predicts the unergative/unaccusative split. Only the two "pure" cells are stable; the mixed cells are where cross-linguistic variation occurs.

inductive Dowty1991.IntransClass : Type

• unergative : IntransClass
• unaccusative : IntransClass
• unstable : IntransClass

@[implicit_reducible]

instance Dowty1991.instDecidableEqIntransClass : DecidableEq IntransClass

Equations

• Dowty1991.instDecidableEqIntransClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dowty1991.instReprIntransClass.repr : IntransClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dowty1991.instReprIntransClass : Repr IntransClass

Equations

• Dowty1991.instReprIntransClass = { reprPrec := Dowty1991.instReprIntransClass.repr }

def Dowty1991.table1 (agentive telic : Bool) : IntransClass

Equations

• Dowty1991.table1 true false = Dowty1991.IntransClass.unergative
• Dowty1991.table1 false true = Dowty1991.IntransClass.unaccusative
• Dowty1991.table1 agentive telic = Dowty1991.IntransClass.unstable

theorem Dowty1991.cell1_unergative : table1 true false = IntransClass.unergative

theorem Dowty1991.cell4_unaccusative : table1 false true = IntransClass.unaccusative

theorem Dowty1991.cell2_unstable : table1 true true = IntransClass.unstable

theorem Dowty1991.cell3_unstable : table1 false false = IntransClass.unstable

theorem Dowty1991.run_cell1 : table1 Features.LevinClassProfiles.selfMotion.subjectProfile.volition Features.LevinClassProfiles.selfMotion.subjectProfile.changeOfState = IntransClass.unergative

theorem Dowty1991.die_cell4 : table1 Features.LevinClassProfiles.disappearance.subjectProfile.volition Features.LevinClassProfiles.disappearance.subjectProfile.changeOfState = IntransClass.unaccusative

The key divergence between [Dow91]'s flat counting and the modern priority-based ASP. Flat counting gets arrive wrong because it counts movement + IE (2 P-Agent) > changeOfState (1 P-Patient), predicting unergative. The modern ASP correctly identifies arrive as unaccusative because it lacks the priority features (volition, causation).

theorem Dowty1991.arrive_flat_wrong : flatPredictsUnaccusative Features.LevinClassProfiles.directedMotion.subjectProfile = false

Flat counting predicts arrive is NOT unaccusative (2 P-Ag > 1 P-Pat).

theorem Dowty1991.arrive_modern_correct : Features.LevinClassProfiles.directedMotion.subjectProfile.PredictsUnaccusative

Modern priority-based ASP correctly predicts arrive IS unaccusative.

theorem Dowty1991.arrive_table1_correct : table1 Features.LevinClassProfiles.directedMotion.subjectProfile.volition Features.LevinClassProfiles.directedMotion.subjectProfile.changeOfState = IntransClass.unaccusative

Table 1 also correctly predicts arrive as unaccusative (non-agentive + telic = cell 4).

theorem Dowty1991.arrive_anomaly_summary : table1 Features.LevinClassProfiles.directedMotion.subjectProfile.volition Features.LevinClassProfiles.directedMotion.subjectProfile.changeOfState = IntransClass.unaccusative ∧ Features.LevinClassProfiles.directedMotion.subjectProfile.PredictsUnaccusative ∧ flatPredictsUnaccusative Features.LevinClassProfiles.directedMotion.subjectProfile = false ∧ English.Predicates.Verbal.arrive.unaccusative = true

Agreement: Table 1 and the modern ASP converge on arrive being unaccusative. Flat counting diverges — this is the anomaly that motivated [davis-koenig-2000]'s priority refinement.

theorem Dowty1991.die_both_agree : flatPredictsUnaccusative Features.LevinClassProfiles.disappearance.subjectProfile = true ∧ Features.LevinClassProfiles.disappearance.subjectProfile.PredictsUnaccusative

Flat counting gets die right (both methods agree).

theorem Dowty1991.run_both_agree : flatPredictsUnergative Features.LevinClassProfiles.selfMotion.subjectProfile = true ∧ Features.LevinClassProfiles.selfMotion.subjectProfile.PredictsUnergative

Flat counting gets run right (both methods agree).

These theorems verify that the English Fragment verb entries store exactly the Levin-class template profiles of LevinClassProfiles.lean — the stored fields are derivable from the class map (sweep_instr is the deliberate instrument-sense override).

theorem Dowty1991.kick_subject_profile_matches : English.Predicates.Verbal.kick.subjectEntailments = some Features.LevinClassProfiles.mannerContact.subjectProfile

theorem Dowty1991.kick_object_profile_matches : English.Predicates.Verbal.kick.objectEntailments = some Features.LevinClassProfiles.contactObject

theorem Dowty1991.eat_subject_profile_matches : English.Predicates.Verbal.eat.subjectEntailments = some Features.LevinClassProfiles.consumption.subjectProfile

theorem Dowty1991.eat_object_profile_matches : English.Predicates.Verbal.eat.objectEntailments = some Features.LevinClassProfiles.consumptionObject

theorem Dowty1991.build_subject_profile_matches : English.Predicates.Verbal.build.subjectEntailments = some Features.LevinClassProfiles.creation.subjectProfile

theorem Dowty1991.build_object_profile_matches : English.Predicates.Verbal.build.objectEntailments = some Features.LevinClassProfiles.creationObject

theorem Dowty1991.run_subject_profile_matches : English.Predicates.Verbal.run.subjectEntailments = some Features.LevinClassProfiles.selfMotion.subjectProfile

theorem Dowty1991.arrive_subject_profile_matches : English.Predicates.Verbal.arrive.subjectEntailments = some Features.LevinClassProfiles.directedMotion.subjectProfile

theorem Dowty1991.see_subject_profile_matches : English.Predicates.Verbal.see.subjectEntailments = some Features.LevinClassProfiles.perception.subjectProfile

theorem Dowty1991.sweep_subject_profile_matches : English.Predicates.Verbal.sweep.subjectEntailments = some Features.LevinClassProfiles.wipeManner.subjectProfile

theorem Dowty1991.sweep_instr_subject_profile_matches : English.Predicates.Verbal.sweep_instr.subjectEntailments = some Features.LevinClassProfiles.wipeInstrument.subjectProfile

theorem Dowty1991.stored_profiles_derivable_from_class : (English.Predicates.Verbal.kick.objectEntailments = English.Predicates.Verbal.kick.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.objectProfile) ∧ (English.Predicates.Verbal.eat.objectEntailments = English.Predicates.Verbal.eat.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.objectProfile) ∧ (English.Predicates.Verbal.build.objectEntailments = English.Predicates.Verbal.build.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.objectProfile) ∧ (English.Predicates.Verbal.see.subjectEntailments = English.Predicates.Verbal.see.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.subjectProfile) ∧ (English.Predicates.Verbal.sweep.subjectEntailments = English.Predicates.Verbal.sweep.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.subjectProfile) ∧ English.Predicates.Verbal.sweep_instr.subjectEntailments ≠ English.Predicates.Verbal.sweep_instr.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.subjectProfile

The stored fragment profiles coincide with the Levin-class fallback — effectiveSubjectEntailments/effectiveObjectEntailments would be unchanged without them. sweep_instr is the deliberate exception: its instrument sense overrides the wipe-class (manner-subclass) default.

theorem Dowty1991.arrive_prediction_matches_fragment : decide Features.LevinClassProfiles.directedMotion.subjectProfile.PredictsUnaccusative = English.Predicates.Verbal.arrive.unaccusative

Agreement: arrive prediction matches the fragment annotation.

theorem Dowty1991.run_prediction_matches_fragment : decide Features.LevinClassProfiles.selfMotion.subjectProfile.PredictsUnaccusative = English.Predicates.Verbal.run.unaccusative

Agreement: run prediction matches the fragment annotation.

[Gri11]'s agentivity lattice reformulates Dowty's proto-roles with lattice structure and connects them to case assignment. Here we verify that Grimm's lattice predictions are consistent with the ASP predictions above, and that it also resolves the arrive anomaly.

theorem Dowty1991.arrive_grimm_not_nom : (ArgumentStructure.AgentivityLattice.GrimmNode.fromSubjectProfile Features.LevinClassProfiles.directedMotion.subjectProfile).toCaseRegion ≠ ArgumentStructure.AgentivityLattice.CaseRegion.nomErg

Grimm's lattice handles the arrive anomaly: arrive's subject has motion but not instigation → not in the NOM/ERG region. Consistent with the priority-based ASP and Table 1, but not flat counting.

theorem Dowty1991.arrive_cross_theory : table1 Features.LevinClassProfiles.directedMotion.subjectProfile.volition Features.LevinClassProfiles.directedMotion.subjectProfile.changeOfState = IntransClass.unaccusative ∧ Features.LevinClassProfiles.directedMotion.subjectProfile.PredictsUnaccusative ∧ flatPredictsUnaccusative Features.LevinClassProfiles.directedMotion.subjectProfile = false ∧ (ArgumentStructure.AgentivityLattice.GrimmNode.fromSubjectProfile Features.LevinClassProfiles.directedMotion.subjectProfile).toCaseRegion ≠ ArgumentStructure.AgentivityLattice.CaseRegion.nomErg ∧ English.Predicates.Verbal.arrive.unaccusative = true

Full cross-theory convergence on arrive: Table 1, modern ASP, and [Gri11]'s lattice all predict unaccusative/non-agent. Only flat counting diverges.

theorem Dowty1991.kick_asp_grimm_consistent : Features.LevinClassProfiles.mannerContact.subjectProfile.OutranksForSubject Features.LevinClassProfiles.contactObject ∧ (ArgumentStructure.AgentivityLattice.GrimmNode.fromSubjectProfile Features.LevinClassProfiles.mannerContact.subjectProfile).toCaseRegion.toAccusativeCase = Case.nom ∧ (ArgumentStructure.AgentivityLattice.GrimmNode.fromObjectProfile Features.LevinClassProfiles.contactObject).toCaseRegion.toAccusativeCase = Case.inst

Kick: ASP outranking and [Gri11]'s subject region converge — subject → NOM in an accusative system. The object, under the corrected surface-contact profile (no entailed change; [Dow91] never discusses kick), falls in Grimm's oblique region (INST), outside canonical ACC — see Grimm2011.kick_object_persistence for the Grimm-vs-Beavers divergence on contact-verb objects.

theorem Dowty1991.die_asp_grimm_consistent : Features.LevinClassProfiles.disappearance.subjectProfile.PredictsUnaccusative ∧ flatPredictsUnaccusative Features.LevinClassProfiles.disappearance.subjectProfile = true ∧ (ArgumentStructure.AgentivityLattice.GrimmNode.fromObjectProfile Features.LevinClassProfiles.disappearance.subjectProfile).toCaseRegion = ArgumentStructure.AgentivityLattice.CaseRegion.accAbs

Die: ASP, flat counting, and [Gri11] all agree on unaccusative. Grimm's lattice maps the sole argument to ACC/ABS (patient region).

theorem Dowty1991.kiss_subject_dominates : ArgumentStructure.AgentivityLattice.AgentivityNode.fromEntailmentProfile kissObjectProfile < ArgumentStructure.AgentivityLattice.AgentivityNode.fromEntailmentProfile kissSubjectProfile

Kiss on [Gri11]'s Fig. 1 lattice: the object's agentivity node {motion} sits strictly below the subject's {volition, motion} — the §1 asymmetry restated as strict lattice dominance.

theorem Dowty1991.kiss_flat_count_from_lattice : kissObjectProfile.pAgentScore ≤ kissSubjectProfile.pAgentScore

Corollary: the flat-count direction follows from lattice dominance via featureCount_monotone and pAgentScore_decomposition — Dowty's counting comparison (kiss_asymmetry_is_volition) is demoted to a consequence of Grimm's order.

The paper's explicit per-argument attributions (generated rows in Data.ProtoRoles.Dowty1991, one per stated entailment, with locators) checked against the class-template profiles. Positive checks confirm the templates encode what Dowty states; the divergence theorems record what they deliberately do NOT encode.

def Dowty1991.matchesProfile (d : ProtoRoleDatum) (p : ArgumentStructure.EntailmentProfile) : Bool

Every entailment a data row explicitly attributes agrees with profile p; fields the paper is silent or hedged about are unconstrained.

Equations

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

theorem Dowty1991.primary_transitives_match_templates : matchesProfile Rows.buildSubject ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile = true ∧ matchesProfile Rows.writeSubject ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile = true ∧ matchesProfile Rows.murderSubject ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile = true ∧ matchesProfile Rows.eatSubject ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile = true ∧ matchesProfile Rows.washSubject ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile = true ∧ matchesProfile Rows.murderObject ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile = true ∧ matchesProfile Rows.washObject ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile = true ∧ matchesProfile Rows.writeObject Features.LevinClassProfiles.creationObject = true ∧ matchesProfile Rows.eatObject Features.LevinClassProfiles.consumptionObject = true

The (35) primary transitive verbs: each stated subject attribution (V+S+C+M, no P-Patient, p. 577) holds of the accomplishment template subject, and each stated object attribution (CoS+CA) holds of the accomplishment/creation/consumption objects.

theorem Dowty1991.hit_class_matches_contact_object : matchesProfile Rows.hitObject Features.LevinClassProfiles.contactObject = true ∧ matchesProfile Rows.hitObject hitArg1 = true ∧ matchesProfile Rows.hitInstrument hitArg2 = true

The hit-class attributions ((64 III), §9.3.3): the direct object is non-moving, unchanged, and a non-incremental-theme — exactly consistent with the mannerContact/wipeManner contacted object (CA+St, no CoS) and with this file's §3 hit-class argument profiles.

theorem Dowty1991.exemplars_match_templates : matchesProfile Rows.seeSubject Features.LevinClassProfiles.perception.subjectProfile = true ∧ matchesProfile Rows.needSubject Features.LevinClassProfiles.desire.subjectProfile = true ∧ Option.map (matchesProfile Rows.needObject) Features.LevinClassProfiles.desire.objectProfile = some true ∧ Option.map (matchesProfile Rows.seekObject) Features.LevinClassProfiles.desire.objectProfile = some true

The (29)/(30) single-entailment exemplars land in the right templates: see (29b) in the perception subject, need (29e) in the desire subject, need's de dicto object (30e) in the desire object.

theorem Dowty1991.psych_desire_split_justified : matchesProfile Rows.likeSubject Features.LevinClassProfiles.psychState.subjectProfile = true ∧ matchesProfile Rows.needSubject Features.LevinClassProfiles.desire.subjectProfile = true ∧ matchesProfile Rows.needSubject Features.LevinClassProfiles.psychState.subjectProfile = false

The split of the former single state-subject profile is Dowty's own: admire-class experiencers are sentience-entailed ((38): like), so psychState fits them; want-class subjects are NOT ((29e)/p. 573: need entails subject existence "but none of (a)-(d)"), so the sentient profile mis-states them — desire fits instead.

theorem Dowty1991.psych_doublet_tie : Features.LevinClassProfiles.psychState.subjectProfile.AllowsAlternation Features.LevinClassProfiles.stimulusProfile ∧ Option.map (matchesProfile Rows.likeObject) Features.LevinClassProfiles.psychState.objectProfile = some true ∧ matchesProfile Rows.pleaseSubject Features.LevinClassProfiles.stimulusProfile = true

The (38) doublet tie: the experiencer ({S,IE}) and stimulus ({C,IE}) profiles are Proto-Agent-incomparable with no Proto-Patient difference, so neither outranks — Corollary 1 predicts both lexicalizations (like/please). The stated stimulus attributions (causation, no sentience) hold of the template's stimulus object.

theorem Dowty1991.inchoative_experiencer_matches : matchesProfile Rows.surpriseObjectInchoative expInchoativeProfile = true ∧ stimProfile.OutranksForSubject expInchoativeProfile

Croft's inchoative restriction (p. 580): under the inchoative reading the experiencer gains a change of state — the stated attribution matches this file's §2 inchoative experiencer profile, which the stimulus then outranks for subject.

theorem Dowty1991.buy_sell_tie : matchesProfile Rows.buySubject Features.LevinClassProfiles.possessionTransfer.subjectProfile = true ∧ matchesProfile Rows.buySeller Features.LevinClassProfiles.possessionTransfer.subjectProfile = true ∧ matchesProfile Rows.sellSubject Features.LevinClassProfiles.possessionTransfer.subjectProfile = true ∧ matchesProfile Rows.sellBuyer Features.LevinClassProfiles.possessionTransfer.subjectProfile = true ∧ Features.LevinClassProfiles.possessionTransfer.subjectProfile.AllowsAlternation Features.LevinClassProfiles.possessionTransfer.subjectProfile

§3.2: buyer and seller are both attributed volition and nothing distinguishes them ("nor are they different in any proto-role entailments", §8.3 p. 579) — the class map gives give-class and obtain-class subjects one shared profile, and Corollary 1 licenses the doublet: a profile never outranks itself.

theorem Dowty1991.build_object_stationary_divergence : matchesProfile Rows.buildObject Features.LevinClassProfiles.creationObject = false ∧ matchesProfile Rows.buildObject (have __src := Features.LevinClassProfiles.creationObject; { volition := __src.volition, sentience := __src.sentience, causation := __src.causation, movement := __src.movement, independentExistence := __src.independentExistence, changeOfState := __src.changeOfState, incrementalTheme := __src.incrementalTheme, causallyAffected := __src.causallyAffected, stationary := true, dependentExistence := __src.dependentExistence }) = true

Build-object stationary divergence: "all of 28" (pp. 572–573) includes (28d) stationary, but the creation template object (CoS+IT+CA+DE) deliberately omits St — the row disagrees with the template on exactly that field. Recorded as data, not flipped: the class-level template follows the (35)/p. 577 hedge ("(mostly) ... stationary"), which does not commit every creation object to (28d).

theorem Dowty1991.break_object_it_divergence : matchesProfile Rows.breakObject ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile = false ∧ matchesProfile Rows.breakObject (have __src := ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile; { volition := __src.volition, sentience := __src.sentience, causation := __src.causation, movement := __src.movement, independentExistence := __src.independentExistence, changeOfState := __src.changeOfState, incrementalTheme := true, causallyAffected := __src.causallyAffected, stationary := __src.stationary, dependentExistence := __src.dependentExistence }) = true

Break-object incremental-themehood divergence: (64 II) attributes "change of state (and Incremental Themehood)" to the break-class direct object, but the resultChange/accomplishment object template carries no IT (per-verb addition by design). The row disagrees with the template on exactly that field.

theorem Dowty1991.eat_object_de_tension : matchesProfile Rows.eatObject Features.LevinClassProfiles.consumptionObject = true ∧ ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile Features.LevinClassProfiles.consumptionObject = ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning ∧ ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile (have __src := Features.LevinClassProfiles.consumptionObject; { volition := __src.volition, sentience := __src.sentience, causation := __src.causation, movement := __src.movement, independentExistence := __src.independentExistence, changeOfState := __src.changeOfState, incrementalTheme := __src.incrementalTheme, causallyAffected := __src.causallyAffected, stationary := __src.stationary, dependentExistence := true }) = ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd

Eat-object dependent-existence tension: (30e)(i) counts destruction — the argument "will not exist after the event" — as dependent existence, which would put DE on eat's object; the paper never states this for eat (the (35) hedge leaves DE open), and the consumption template omits DE because the Grimm bridge disambiguation is load-bearing: adding DE to an incremental theme flips PersistenceLevel.fromPatientProfile from exPersBeginning (consumption) to exPersEnd (creation), misclassifying eat as a creation verb. Recorded, not flipped.

theorem Dowty1991.spray_load_rows_match : matchesProfile Rows.loadTheme sprayLoadTheme = true ∧ matchesProfile Rows.loadLocation sprayLoadLocation = true

The spray/load rows ((64 I), p. 594): both nonsubject arguments are attributed a change of state, matching this file's §3 profiles.