Affectedness

[Bea11]'s scalar-theoretic affectedness hierarchy: the four-level degree scale, two independent typeclass primitives (result states, force recipients), the Beavers (60a–c) predicates and eq. (62) implication chain over them, stackable mixin classes, and the projection of [Dow91]'s P-Patient entailments onto the scale ([Bea10]).

Main definitions

• AffectednessDegree — the four-level scale, a LinearOrder
• HasScalarResult, HasLatentScale — the two scalar primitives
• Quantized, NonQuantized, Potential — Beavers (60a–c) on a thematic relation, with the eq. (62) chain (nonQuantized_of_quantized, potential_of_nonQuantized) and its hypothesis ScalarToLatent
• LawfulScalarLatent — the forgetful link as a coherence mixin between the two primitives
• IsQuantizedAffected, IsNonQuantizedAffected, IsPotentialAffected — eq. (62) as stackable mixin classes
• AffectednessDegree.holdsAt — the predicate each degree names, with eq. (62) as the order's semantics (holdsAt_antitone)
• profileToDegree — projection of EntailmentProfile onto the scale

Implementation notes

The two primitives are formally independent; the eq. (62) middle arrow takes ScalarToLatent as an explicit hypothesis. The affectedness classes are stackable mixins, not an extends chain: declare the strongest class that holds and the weaker ones are derived (the ordered-algebra IsOrderedRing precedent) — the leftmost arrow by instance, the middle arrow by IsNonQuantizedAffected.isPotential'. The middle arrow is deliberately not an instance: its δ would be a metavariable during synthesis, and the forgetful link is a modeling assumption that should stay visible at use sites. IsQuantizedAffected is Type-valued so the verb's named final degree survives as data. (60d) is trivially satisfied by any argument of θ (take θ′ := θ) — Beavers' point that the rightmost degree is mere participation; a degree tag only here, since participation is carried by θ's typing (in the paper both (60c) and (60d) are contentful under quantification restricted to the predicate's role inventory). Accordingly the file formalizes two of (62)'s three arrows; the rightmost is trivial under this typing. One of three EntailmentProfile projections (AgentivityNode P-Agent, this file P-Patient strength → MAP (Studies/Beavers2010.lean), PersistenceLevel → case regions); distinct from the surface (MeaningComponents.changeOfState) and root (LexKind.result) change-of-state notions ([BKG20]).

The affectedness degree scale

inductive ArgumentStructure.Affectedness.AffectednessDegree : Type

[Bea11] eq. (62): four affectedness degrees, ordered by truth-conditional strength, weakest first.

• unspecified : AffectednessDegree

  Mere event participation (see, follow, ponder — Beavers' "other activities/states").

• potential : AffectednessDegree

  Force recipient: latent scale exists (hit, wipe).

• nonquantized : AffectednessDegree

  Some result state entailed (cool, widen).

• quantized : AffectednessDegree

  Specific final degree entailed (break, destroy).

@[implicit_reducible]

instance ArgumentStructure.Affectedness.instDecidableEqAffectednessDegree : DecidableEq AffectednessDegree

Equations

• ArgumentStructure.Affectedness.instDecidableEqAffectednessDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ArgumentStructure.Affectedness.instFintypeAffectednessDegree : Fintype AffectednessDegree

Equations

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

@[implicit_reducible]

instance ArgumentStructure.Affectedness.instReprAffectednessDegree : Repr AffectednessDegree

Equations

• ArgumentStructure.Affectedness.instReprAffectednessDegree = { reprPrec := ArgumentStructure.Affectedness.instReprAffectednessDegree.repr }

def ArgumentStructure.Affectedness.instReprAffectednessDegree.repr : AffectednessDegree → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ArgumentStructure.Affectedness.instInhabitedAffectednessDegree : Inhabited AffectednessDegree

Equations

• ArgumentStructure.Affectedness.instInhabitedAffectednessDegree = { default := ArgumentStructure.Affectedness.instInhabitedAffectednessDegree.default }

def ArgumentStructure.Affectedness.AffectednessDegree.strength : AffectednessDegree → ℕ

Numeric strength: higher index = stronger truth conditions.

Equations

• ArgumentStructure.Affectedness.AffectednessDegree.unspecified.strength = 0
• ArgumentStructure.Affectedness.AffectednessDegree.potential.strength = 1
• ArgumentStructure.Affectedness.AffectednessDegree.nonquantized.strength = 2
• ArgumentStructure.Affectedness.AffectednessDegree.quantized.strength = 3

@[implicit_reducible]

instance ArgumentStructure.Affectedness.AffectednessDegree.instLinearOrder : LinearOrder AffectednessDegree

Equations

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

Scalar-result and latent-scale primitives

class ArgumentStructure.Affectedness.HasScalarResult (α : Type u_4) (δ : Type u_5) (β : Type u_6) : Type (max (max u_4 u_5) u_6)

resultAt x g e: theme x ends event e holding degree g on the verb's lexical dimension δ ([Bea11] eq. 60a–b). Beavers' own result′(x, s, g, e) carries a first-class scale token s (not a state); typing the scale away as δ is why ScalarToLatent is a hypothesis here where the paper's (62) middle arrow is free existential generalization, and it puts the §4 Figure/Path mereology out of this interface's reach.

• resultAt : α → δ → β → Prop

  Theme x ends event e holding degree g on dimension δ.

class ArgumentStructure.Affectedness.HasLatentScale (α : Type u_4) (β : Type u_5) : Type (max u_4 u_5)

latentScale x e: theme x is a force-recipient at event e — a latent scale, no transition entailed ([Bea11] eq. 60c). The force-recipient category is [RHL01]'s (following Croft); its codification as a latent scale is Beavers' own proposal, building on [Ten92]'s latent aspectual structure.

• latentScale : α → β → Prop

  Theme x is a force-recipient at event e (latent scale relation).

Beavers (60a–c) affectedness predicates

def ArgumentStructure.Affectedness.Quantized {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] (θ : α → β → Prop) (g_φ : δ) : Prop

[Bea11] eq. (60a): θ entails the theme ends the event at the specific degree g_φ the verb names (break, destroy).

Equations

• ArgumentStructure.Affectedness.Quantized θ g_φ = ∀ (x : α) (e : β), θ x e → ArgumentStructure.Affectedness.HasScalarResult.resultAt x g_φ e

def ArgumentStructure.Affectedness.NonQuantized {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] (θ : α → β → Prop) : Prop

[Bea11] eq. (60b): θ entails the theme ends the event at some degree (widen, cool). Scalar change without a net scalar RESULT (doubling-back motion, [BKG20] ch. 4 recapping their 2017 typology) is a boundary case this predicate formalizes as result-at-event's-end.

Equations

• ArgumentStructure.Affectedness.NonQuantized θ = ∀ (x : α) (e : β), θ x e → ∃ (g : δ), ArgumentStructure.Affectedness.HasScalarResult.resultAt x g e

def ArgumentStructure.Affectedness.Potential {α : Type u_1} {β : Type u_2} [HasLatentScale α β] (θ : α → β → Prop) : Prop

[Bea11] eq. (60c): θ entails the theme is a force-recipient (hit, wipe).

Equations

• ArgumentStructure.Affectedness.Potential θ = ∀ (x : α) (e : β), θ x e → ArgumentStructure.Affectedness.HasLatentScale.latentScale x e

def ArgumentStructure.Affectedness.ScalarToLatent (α : Type u_4) (δ : Type u_5) (β : Type u_6) [HasScalarResult α δ β] [HasLatentScale α β] : Prop

The forgetful link: a result-bearing theme is a force-recipient. Hypothesis of eq. (62)'s middle arrow: free in the paper's formulation (existential generalization over the θ-relation); a hypothesis here only because the encoding discards the scale token.

Equations

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

class ArgumentStructure.Affectedness.LawfulScalarLatent (α : Type u_4) (δ : Type u_5) (β : Type u_6) [HasScalarResult α δ β] [HasLatentScale α β] : Prop

The forgetful link as a coherence mixin between the two primitives: holds in the canonical model; per-model instances declare it.

• toLatent : ScalarToLatent α δ β

  The ScalarToLatent witness.

Implication chain (Beavers eq. 62)

theorem ArgumentStructure.Affectedness.nonQuantized_of_quantized {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] {θ : α → β → Prop} {g_φ : δ} (h : Quantized θ g_φ) : NonQuantized θ

[Bea11] eq. (62), leftmost arrow.

theorem ArgumentStructure.Affectedness.potential_of_nonQuantized {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] {θ : α → β → Prop} [HasLatentScale α β] (forget : ScalarToLatent α δ β) (h : NonQuantized θ) : Potential θ

[Bea11] eq. (62), middle arrow, under the forgetful link.

Typeclass mixins (Beavers eq. 62)

class ArgumentStructure.Affectedness.IsPotentialAffected {α : Type u_1} {β : Type u_2} [HasLatentScale α β] (θ : α → β → Prop) : Prop

Eq. (60c) as the bottom of the mixin stack (hit, wipe).

• isPotential : Potential θ

  Beavers (60c): every event of θ has a force-receiving theme.

class ArgumentStructure.Affectedness.IsNonQuantizedAffected {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] (θ : α → β → Prop) : Prop

Eq. (60b): a result-state commitment (widen, cool).

• isNonQuantized : NonQuantized θ

  Beavers (60b): every event of θ ends with some result degree.

class ArgumentStructure.Affectedness.IsQuantizedAffected {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] (θ : α → β → Prop) : Type u_3

Eq. (60a): the verb's specific final degree, kept as data (break, destroy; the SINC bridge is in Semantics/Aspect/Incremental.lean).

• finalDegree : δ

  The lexically-named specific final degree g_φ.

• isQuantized : Quantized θ (finalDegree θ)

  Witness that θ entails the theme ends the event with this degree.

instance ArgumentStructure.Affectedness.IsQuantizedAffected.toIsNonQuantizedAffected {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] {θ : α → β → Prop} [inst : IsQuantizedAffected θ] : IsNonQuantizedAffected θ

Eq. (62), leftmost arrow, free at the class level: quantized-affected verbs are non-quantized-affected.

theorem ArgumentStructure.Affectedness.IsNonQuantizedAffected.isPotential' {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] {θ : α → β → Prop} [HasLatentScale α β] [LawfulScalarLatent α δ β] [inst : IsNonQuantizedAffected θ] : IsPotentialAffected θ

Eq. (62), middle arrow at the class level, under the LawfulScalarLatent mixin. Deliberately a theorem, not an instance (see Implementation notes).

Degree interpretation (Beavers eq. 60 and 62)

def ArgumentStructure.Affectedness.AffectednessDegree.holdsAt {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] [HasLatentScale α β] (θ : α → β → Prop) : AffectednessDegree → Prop

The predicate each degree names, for a fixed θ ([Bea11] eq. 60): unspecified is participation itself, carried by θ's typing.

Equations

• ArgumentStructure.Affectedness.AffectednessDegree.holdsAt θ ArgumentStructure.Affectedness.AffectednessDegree.unspecified = True
• ArgumentStructure.Affectedness.AffectednessDegree.holdsAt θ ArgumentStructure.Affectedness.AffectednessDegree.potential = ArgumentStructure.Affectedness.Potential θ
• ArgumentStructure.Affectedness.AffectednessDegree.holdsAt θ ArgumentStructure.Affectedness.AffectednessDegree.nonquantized = ArgumentStructure.Affectedness.NonQuantized θ
• ArgumentStructure.Affectedness.AffectednessDegree.holdsAt θ ArgumentStructure.Affectedness.AffectednessDegree.quantized = ∃ (g : δ), ArgumentStructure.Affectedness.Quantized θ g

theorem ArgumentStructure.Affectedness.AffectednessDegree.holdsAt_antitone {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] [HasLatentScale α β] [LawfulScalarLatent α δ β] {θ : α → β → Prop} {d d' : AffectednessDegree} (hle : d' ≤ d) (h : holdsAt θ d) : holdsAt θ d'

Eq. (62) as the order's semantics: a degree entails every weaker one. The scale-token elision makes the potential step depend on LawfulScalarLatent (see HasScalarResult's docstring).

Projection from EntailmentProfile

def ArgumentStructure.Affectedness.profileToDegree (p : EntailmentProfile) : AffectednessDegree

Approximating adapter (linglib's, not Beavers') from [Dow91] entailments, via [Bea10]'s reduction of Dowty's P-Patient entailments to the affectedness entailments: CoS/IT split quantized/nonquantized; CA/St split potential/unspecified. Known misfits on Beavers' own exemplars (break, shatter are quantized without incrementality; cut, slice non-quantized with it) — the faithful route is the scalar witness (finalDegree), per the bridge note below.

Equations

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

theorem ArgumentStructure.Affectedness.profileToDegree_depends_only_on_patient (p q : EntailmentProfile) (hcos : p.changeOfState = q.changeOfState) (hit : p.incrementalTheme = q.incrementalTheme) (hca : p.causallyAffected = q.causallyAffected) (hst : p.stationary = q.stationary) : profileToDegree p = profileToDegree q

Profiles agreeing on {CoS, IT, CA, St} map to the same degree — the remaining six features are irrelevant.

@[simp]

theorem ArgumentStructure.Affectedness.profileToDegree_eq_quantized_iff (p : EntailmentProfile) : profileToDegree p = AffectednessDegree.quantized ↔ p.incrementalTheme = true ∧ p.changeOfState = true

The quantized fiber: exactly IT ∧ CoS.

@[simp]

theorem ArgumentStructure.Affectedness.profileToDegree_eq_nonquantized_iff (p : EntailmentProfile) : profileToDegree p = AffectednessDegree.nonquantized ↔ p.changeOfState = true ∧ p.incrementalTheme = false

The nonquantized fiber: exactly CoS without IT.

@[simp]

theorem ArgumentStructure.Affectedness.profileToDegree_eq_potential_iff (p : EntailmentProfile) : profileToDegree p = AffectednessDegree.potential ↔ p.changeOfState = false ∧ (p.causallyAffected = true ∨ p.stationary = true)

The potential fiber: exactly no CoS with CA or St.

@[simp]

theorem ArgumentStructure.Affectedness.profileToDegree_eq_unspecified_iff (p : EntailmentProfile) : profileToDegree p = AffectednessDegree.unspecified ↔ p.changeOfState = false ∧ p.causallyAffected = false ∧ p.stationary = false

The unspecified fiber: exactly no CoS, no CA, no St.

Bridge to the typeclass chain

Connecting profileToDegree to IsQuantizedAffected structurally needs per-verb substrate binding a fragment verb's profile to its θ; until that lands, consumers declare the strongest mixin the verb's scalar witnesses support.