@cite{hartshorne-etal-2016} — Empirical Data

@cite{hartshorne-etal-2016}

Psych verbs, the linking problem, and the acquisition of language. Cognition 157: 268–288.

Core empirical claim

The experiencer-subject / experiencer-object split maps onto a semantic distinction between habitual attitudes and caused emotional episodes:

Verb class	Semantic type	Example
Fear-type (Class I, exp-subj)	Habitual attitude	"Mary fears spiders"
Frighten-type (Class II, exp-obj)	Caused emotional episode	"Spiders frighten Mary"

This is diagnosed by three empirical properties:

1. Duration: attitudes are longer-lasting than episodes
2. Causation: episodes encode causal responsibility of stimulus; attitudes do not
3. Cross-linguistic: the mapping holds in English, Mandarin, Korean, Japanese

Semantic structures (Fig. 11)

• Attitudes: BE(experiencer, emotional_state ABOUT target)
• Episodes: CAUSE(stimulus, BECOME(experiencer, emotional_state))

Linking mechanism (Section 5.4.1)

Prominence preservation: the highest argument in the semantic structure maps to subject. For attitudes, experiencer is the argument of BE (the main predicate), so it is highest → subject. For episodes, stimulus is the argument of CAUSE (the outermost predicate), so it is highest → subject.

Studies

Study	Language	Population	Finding
1	English	Adults	Fear-type rated longer duration
2–4	English, Mandarin, Korean, Japanese	Adults	Frighten-type rated higher causation
5	English	Adults (novel verbs)	Generalization to nonce verbs
6–7	Japanese	Adults (novel verbs)	Generalization + morphological cue
8	Russian	Adults (novel verbs)	Generalization cross-linguistically
9	English	Children (4–5 y.o.)	Early emergence of the distinction

inductive Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType : Type

The two semantic types for psych verbs (@cite{hartshorne-etal-2016}, Fig. 11).

This is the paper's central theoretical claim: psych verb classes correspond to distinct semantic types, not merely different linking patterns.

• habitualAttitude : SemanticType

  BE(experiencer, emotional_state ABOUT target). Enduring psychological state directed at a target.

• causedEpisode : SemanticType

  CAUSE(stimulus, BECOME(experiencer, emotional_state)). Specific instance where a stimulus causes an emotion.

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqSemanticType : DecidableEq SemanticType

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqSemanticType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticType : BEq SemanticType

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticType = { beq := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticType.beq }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticType.beq : SemanticType → SemanticType → Bool

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticType.repr : SemanticType → ℕ → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticType : Repr SemanticType

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticType = { reprPrec := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticType.repr }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.PsychVerbClass.toSemanticType : Data.PsychVerbClass → Option SemanticType

Map B&R class to Hartshorne et al.'s semantic type.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.PsychVerbClass.toSemanticType Phenomena.PsychVerbs.Data.PsychVerbClass.classIII = none

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.ClassIIReading.toSemanticType : Data.ClassIIReading → Option SemanticType

Map Class II reading to semantic type. Eventive Class II = caused episode (clear mapping). Stative Class II does not cleanly map to either Hartshorne category: stative frighten-type verbs ("concern", "bore") still encode stimulus causation (unlike attitudes) but have longer duration than eventive Class II (p. 273: avg 3.7 vs 2.9 vs fear-type 5.2).

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.ClassIIReading.toSemanticType Phenomena.PsychVerbs.Data.ClassIIReading.stative = none

structure Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticTypeProfile : Type

Properties that distinguish the two semantic types empirically.

• longerDuration : Bool

  Does the verb encode longer duration? Attitudes = true (enduring), episodes = false (transient).

• stimulusCausal : Bool

  Does the verb encode causal responsibility of the stimulus? Episodes = true (CAUSE), attitudes = false (no CAUSE).

• involvesBecome : Bool

  Does the verb involve a transition (BECOME)? Episodes = true (BECOME), attitudes = false (BE).

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqSemanticTypeProfile.decEq (x✝ x✝¹ : SemanticTypeProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqSemanticTypeProfile : DecidableEq SemanticTypeProfile

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqSemanticTypeProfile = Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqSemanticTypeProfile.decEq

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticTypeProfile : BEq SemanticTypeProfile

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticTypeProfile = { beq := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticTypeProfile.beq }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticTypeProfile.beq : SemanticTypeProfile → SemanticTypeProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqSemanticTypeProfile.beq x✝¹ x✝ = false

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticTypeProfile.repr : SemanticTypeProfile → ℕ → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticTypeProfile : Repr SemanticTypeProfile

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticTypeProfile = { reprPrec := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprSemanticTypeProfile.repr }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.attitudeProfile : SemanticTypeProfile

Profile for habitual attitudes (fear-type). Long duration, no causal responsibility, no transition.

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.attitudeProfile = { longerDuration := true, stimulusCausal := false, involvesBecome := false }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.episodeProfile : SemanticTypeProfile

Profile for caused emotional episodes (frighten-type). Short duration, causal responsibility, involves transition.

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.episodeProfile = { longerDuration := false, stimulusCausal := true, involvesBecome := true }

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.profiles_differ_on_all : attitudeProfile.longerDuration ≠ episodeProfile.longerDuration ∧ attitudeProfile.stimulusCausal ≠ episodeProfile.stimulusCausal ∧ attitudeProfile.involvesBecome ≠ episodeProfile.involvesBecome

The two profiles differ on every dimension.

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType.expectedProfile : SemanticType → SemanticTypeProfile

Map semantic type to its expected profile.

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType.habitualAttitude.expectedProfile = Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.attitudeProfile
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType.causedEpisode.expectedProfile = Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.episodeProfile

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType.prominentRole : SemanticType → Data.SubjectRole

The structurally prominent role in each semantic type (Section 5.4.1).

In the attitude structure BE(experiencer, state ABOUT target), experiencer is the highest argument (argument of the main predicate BE).

In the episode structure CAUSE(stimulus, BECOME(experiencer, state)), stimulus is the highest argument (argument of the outermost predicate CAUSE).

This determines linking via prominence preservation: the highest argument maps to subject position.

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType.habitualAttitude.prominentRole = Phenomena.PsychVerbs.Data.SubjectRole.experiencer
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.SemanticType.causedEpisode.prominentRole = Phenomena.PsychVerbs.Data.SubjectRole.stimulus

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.prominence_determines_linking (c : Data.PsychVerbClass) (t : SemanticType) (h : PsychVerbClass.toSemanticType c = some t) : c.expectedSubjectRole = some t.prominentRole

Prominence preservation (@cite{hartshorne-etal-2016}, Section 5.4.1): the most prominent argument in the semantic decomposition becomes the subject. This is the paper's central theoretical claim about HOW semantic type determines argument structure.

The predicted subject role from prominence matches the observed Belletti & Rizzi class pattern: Class I → experiencer-subject, Class II → stimulus-subject.

inductive Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.Language : Type

Languages tested in @cite{hartshorne-etal-2016}.

• english : Language
• mandarin : Language
• korean : Language
• japanese : Language
• russian : Language

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqLanguage : DecidableEq Language

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instDecidableEqLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqLanguage : BEq Language

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqLanguage = { beq := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqLanguage.beq }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqLanguage.beq : Language → Language → Bool

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqLanguage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprLanguage : Repr Language

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprLanguage = { reprPrec := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprLanguage.repr }

structure Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.CrossLinguisticDatum : Type

Cross-linguistic replication datum: the attitude/episode distinction holds in each language tested.

• language : Language
• fearLongerDuration : Bool

  Do fear-type verbs rate higher on duration than frighten-type?

• frightenMoreCausal : Bool

  Do frighten-type verbs rate higher on causation than fear-type?

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqCrossLinguisticDatum : BEq CrossLinguisticDatum

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqCrossLinguisticDatum = { beq := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqCrossLinguisticDatum.beq }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqCrossLinguisticDatum.beq : CrossLinguisticDatum → CrossLinguisticDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqCrossLinguisticDatum.beq x✝¹ x✝ = false

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprCrossLinguisticDatum : Repr CrossLinguisticDatum

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprCrossLinguisticDatum = { reprPrec := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprCrossLinguisticDatum.repr }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprCrossLinguisticDatum.repr : CrossLinguisticDatum → ℕ → Std.Format

Equations

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

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.crossLinguisticData : List CrossLinguisticDatum

Cross-linguistic data: all four languages show the same pattern. Experiments 1–4, summarized in Fig. 7–8.

Equations

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

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.crosslinguistic_universal : (crossLinguisticData.all fun (d : CrossLinguisticDatum) => d.fearLongerDuration && d.frightenMoreCausal) = true

The attitude/episode distinction is universal across tested languages.

structure Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.GeneralizationDatum : Type

A generalization experiment: does the semantic type distinction guide argument structure assignment for novel (nonce) verbs?

• language : Language
• isChildPopulation : Bool
• attitudePredictExpSubj : Bool

  Attitude semantics → experiencer-subject preference?

• episodePredictExpObj : Bool

  Episode semantics → experiencer-object preference?

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqGeneralizationDatum.beq : GeneralizationDatum → GeneralizationDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqGeneralizationDatum.beq x✝¹ x✝ = false

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqGeneralizationDatum : BEq GeneralizationDatum

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqGeneralizationDatum = { beq := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqGeneralizationDatum.beq }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprGeneralizationDatum.repr : GeneralizationDatum → ℕ → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprGeneralizationDatum : Repr GeneralizationDatum

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprGeneralizationDatum = { reprPrec := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprGeneralizationDatum.repr }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.generalizationData : List GeneralizationDatum

Generalization data from Experiments 5–9. Adults and children use the semantic type distinction to determine argument structure for novel verbs across languages.

Equations

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

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.generalization_universal : (generalizationData.all fun (d : GeneralizationDatum) => d.attitudePredictExpSubj && d.episodePredictExpObj) = true

All generalization experiments show the predicted pattern.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.children_generalize : ((List.filter (fun (x : GeneralizationDatum) => x.isChildPopulation) generalizationData).all fun (d : GeneralizationDatum) => d.attitudePredictExpSubj && d.episodePredictExpObj) = true

The distinction emerges early in development (4–5 y.o.).

structure Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.VerbDatum : Type

A psych verb datum from Hartshorne et al.'s norming studies.

• verb : String
• semanticType : SemanticType
• brClass : Data.PsychVerbClass

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqVerbDatum : BEq VerbDatum

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqVerbDatum = { beq := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqVerbDatum.beq }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqVerbDatum.beq : VerbDatum → VerbDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instBEqVerbDatum.beq x✝¹ x✝ = false

instance Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprVerbDatum : Repr VerbDatum

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprVerbDatum = { reprPrec := Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprVerbDatum.repr }

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.instReprVerbDatum.repr : VerbDatum → ℕ → Std.Format

Equations

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

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.verbData : List VerbDatum

Representative verb data from @cite{hartshorne-etal-2016}. Fear-type verbs are habitual attitudes, frighten-type are caused episodes.

Equations

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

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.fear_type_are_attitudes : ((List.filter (fun (x : VerbDatum) => x.brClass == Data.PsychVerbClass.classI) verbData).all fun (x : VerbDatum) => x.semanticType == SemanticType.habitualAttitude) = true

All fear-type verbs in the data are habitual attitudes.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.frighten_type_are_episodes : ((List.filter (fun (x : VerbDatum) => x.brClass == Data.PsychVerbClass.classII) verbData).all fun (x : VerbDatum) => x.semanticType == SemanticType.causedEpisode) = true

All frighten-type verbs in the data are caused episodes.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.class_type_alignment : (verbData.all fun (d : VerbDatum) => match d.brClass with | Data.PsychVerbClass.classI => d.semanticType == SemanticType.habitualAttitude | Data.PsychVerbClass.classII => d.semanticType == SemanticType.causedEpisode | Data.PsychVerbClass.classIII => true) = true

The class–type mapping is perfect: no verb has a mismatched type.

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.semanticTypeToCausalSource : SemanticType → Semantics.Causation.PsychCausation.CausalSource

Map Hartshorne et al.'s semantic type to Kim's CausalSource. Habitual attitudes = internal (mental representation maintains state); caused episodes = external (percept triggers state change).

Equations

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

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.causalSourceToSemanticType : Semantics.Causation.PsychCausation.CausalSource → SemanticType

Map Kim's CausalSource back to semantic type.

Equations

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

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.semanticType_source_roundtrip (t : SemanticType) : causalSourceToSemanticType (semanticTypeToCausalSource t) = t

Roundtrip: SemanticType → CausalSource → SemanticType.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.source_semanticType_roundtrip (s : Semantics.Causation.PsychCausation.CausalSource) : semanticTypeToCausalSource (causalSourceToSemanticType s) = s

Roundtrip: CausalSource → SemanticType → CausalSource.

def Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.causalSourceToProfile : Semantics.Causation.PsychCausation.CausalSource → SemanticTypeProfile

Derive the expected empirical profile from CausalSource.

• External: short duration (episode), causal stimulus, involves BECOME
• Internal: long duration (attitude), no causal stimulus, no BECOME

Equations

• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.external = Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.episodeProfile
• Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.internal = Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.attitudeProfile

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.internal_longer_duration : (causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.internal).longerDuration = true

Duration: internal source → longer duration (enduring attitude).

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.external_shorter_duration : (causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.external).longerDuration = false

Duration: external source → shorter duration (transient episode).

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.external_stimulus_causal : (causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.external).stimulusCausal = true

Causation: external source → stimulus is causal.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.internal_stimulus_not_causal : (causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.internal).stimulusCausal = false

Causation: internal source → stimulus not causal.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.external_involves_become : (causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.external).involvesBecome = true

Transition: external source → involves BECOME.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.internal_no_become : (causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.internal).involvesBecome = false

Transition: internal source → no BECOME.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.sources_differ_on_all : causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.external ≠ causalSourceToProfile Semantics.Causation.PsychCausation.CausalSource.internal

The two causal sources predict opposite empirical profiles.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.profile_agreement (t : SemanticType) : causalSourceToProfile (semanticTypeToCausalSource t) = t.expectedProfile

The profile derived via CausalSource agrees with the profile derived directly from SemanticType. This is non-trivial: we defined the two mappings independently and they agree.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.external_predicts_transition (Time : Type u_1) [LinearOrder Time] : (Semantics.Causation.PsychCausalLink.CausalSource.toLink Time Semantics.Causation.PsychCausation.CausalSource.external).involvesTransition = true

External source predicts transition (BECOME).

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.internal_predicts_no_transition (Time : Type u_1) [LinearOrder Time] : (Semantics.Causation.PsychCausalLink.CausalSource.toLink Time Semantics.Causation.PsychCausation.CausalSource.internal).involvesTransition = false

Internal source predicts no transition.

theorem Phenomena.PsychVerbs.Studies.HartshorneEtAl2016.transition_prediction_consistent (t : SemanticType) (Time : Type u_1) [LinearOrder Time] : (Semantics.Causation.PsychCausalLink.CausalSource.toLink Time (semanticTypeToCausalSource t)).involvesTransition = (causalSourceToProfile (semanticTypeToCausalSource t)).involvesBecome

Consistency: PsychCausalLink's transition prediction agrees with the empirical profile derived from SemanticType. Both are derived independently — the agreement is a genuine check.