Prominence Scales and Differential Argument Marking [Jus24] [Has21]

[Ais03] [Has19]

Framework-agnostic prominence hierarchies for referential properties. These scales underlie both differential flagging (case marking: DOM, DSM) and differential indexing (verbal agreement), as argued by [Jus24] and building on [Ais03].

Scales

Three independently motivated prominence hierarchies:

• Animacy: Human > Animate > Inanimate
• Definiteness: Personal Pronoun > Proper Name > Definite NP > Indefinite Specific > Non-specific
• Person: 1st > 2nd > 3rd

These are the same scales for all argument roles (A, P, R, T), but the polarity of differential marking depends on argument role:

• P/T marking targets prominent referents (departures from low default)
• A/R marking targets non-prominent referents (departures from high default)

Argument Roles ([Has21], §2–5)

Five roles span monotransitive and ditransitive clauses:

• S: sole argument of intransitive (reference point for alignment)
• A: agent-like argument of monotransitive
• P: patient-like argument of monotransitive
• R: recipient-like argument of ditransitive (higher role rank, like A)
• T: theme-like argument of ditransitive (lower role rank, like P)

Marking Channels

Differential argument marking has two independent realization channels:

• Flagging: morphological case on the NP
• Indexing: verbal agreement / cross-referencing

These serve different functions — flagging disambiguates roles, indexing tracks referents through discourse — but both are governed by the same prominence scales.

inductive Features.Prominence.AnimacyLevel : Type

Levels of the animacy prominence scale. Human > Animate > Inanimate.

• human : AnimacyLevel

  Most prominent: human referents

• animate : AnimacyLevel

  Non-human animates

• inanimate : AnimacyLevel

  Least prominent: inanimate referents

@[implicit_reducible]

instance Features.Prominence.instDecidableEqAnimacyLevel : DecidableEq AnimacyLevel

Equations

• Features.Prominence.instDecidableEqAnimacyLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prominence.instReprAnimacyLevel : Repr AnimacyLevel

Equations

• Features.Prominence.instReprAnimacyLevel = { reprPrec := Features.Prominence.instReprAnimacyLevel.repr }

def Features.Prominence.instReprAnimacyLevel.repr : AnimacyLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prominence.instInhabitedAnimacyLevel : Inhabited AnimacyLevel

Equations

• Features.Prominence.instInhabitedAnimacyLevel = { default := Features.Prominence.instInhabitedAnimacyLevel.default }

def Features.Prominence.AnimacyLevel.rank : AnimacyLevel → ℕ

Numeric rank on the animacy scale: Human (2) > Animate (1) > Inanimate (0).

Equations

• Features.Prominence.AnimacyLevel.human.rank = 2
• Features.Prominence.AnimacyLevel.animate.rank = 1
• Features.Prominence.AnimacyLevel.inanimate.rank = 0

@[implicit_reducible]

instance Features.Prominence.instLinearOrderAnimacyLevel : LinearOrder AnimacyLevel

Inanimate < Animate < Human (ordered by prominence rank).

Equations

• Features.Prominence.instLinearOrderAnimacyLevel = LinearOrder.lift' Features.Prominence.AnimacyLevel.rank Features.Prominence.instLinearOrderAnimacyLevel._proof_1

def Features.Prominence.AnimacyLevel.all : List AnimacyLevel

All animacy levels (exhaustive enumeration for finite verification).

Equations

• Features.Prominence.AnimacyLevel.all = [Features.Prominence.AnimacyLevel.human, Features.Prominence.AnimacyLevel.animate, Features.Prominence.AnimacyLevel.inanimate]

theorem Features.Prominence.AnimacyLevel.all_length : all.length = 3

inductive Features.Prominence.AnimacyRank : Type

Fine-grained animacy hierarchy for nominal plural marking and agreement ([SS74], [Cor00]).

Languages mark plural on nouns according to an implicational scale:

speaker > addressee > 3rd person > kin > human > higher animals > lower animals > discrete inanimates > nondiscrete inanimates

If a language marks plural at a given point on the scale, it marks plural at all higher points. This refines the coarser AnimacyLevel (human/animate/inanimate) used for differential argument marking.

• speaker : AnimacyRank
• addressee : AnimacyRank
• thirdPerson : AnimacyRank
• kin : AnimacyRank
• human : AnimacyRank
• higherAnimal : AnimacyRank
• lowerAnimal : AnimacyRank
• discreteInanimate : AnimacyRank
• nondiscreteInanimate : AnimacyRank

@[implicit_reducible]

instance Features.Prominence.instDecidableEqAnimacyRank : DecidableEq AnimacyRank

Equations

• Features.Prominence.instDecidableEqAnimacyRank x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prominence.instReprAnimacyRank : Repr AnimacyRank

Equations

• Features.Prominence.instReprAnimacyRank = { reprPrec := Features.Prominence.instReprAnimacyRank.repr }

def Features.Prominence.instReprAnimacyRank.repr : AnimacyRank → ℕ → Std.Format

Equations

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

def Features.Prominence.AnimacyRank.toNat : AnimacyRank → ℕ

Numeric rank for comparison (higher = more likely to be plural-marked).

Equations

• Features.Prominence.AnimacyRank.speaker.toNat = 8
• Features.Prominence.AnimacyRank.addressee.toNat = 7
• Features.Prominence.AnimacyRank.thirdPerson.toNat = 6
• Features.Prominence.AnimacyRank.kin.toNat = 5
• Features.Prominence.AnimacyRank.human.toNat = 4
• Features.Prominence.AnimacyRank.higherAnimal.toNat = 3
• Features.Prominence.AnimacyRank.lowerAnimal.toNat = 2
• Features.Prominence.AnimacyRank.discreteInanimate.toNat = 1
• Features.Prominence.AnimacyRank.nondiscreteInanimate.toNat = 0

def Features.Prominence.AnimacyRank.toAnimacyLevel : AnimacyRank → AnimacyLevel

Coarsen the 9-level animacy hierarchy to the 3-level scale used for differential argument marking. The mapping:

• speaker/addressee/thirdPerson/kin/human → .human
• higherAnimal/lowerAnimal → .animate
• discreteInanimate/nondiscreteInanimate → .inanimate

Equations

• Features.Prominence.AnimacyRank.speaker.toAnimacyLevel = Features.Prominence.AnimacyLevel.human
• Features.Prominence.AnimacyRank.addressee.toAnimacyLevel = Features.Prominence.AnimacyLevel.human
• Features.Prominence.AnimacyRank.thirdPerson.toAnimacyLevel = Features.Prominence.AnimacyLevel.human
• Features.Prominence.AnimacyRank.kin.toAnimacyLevel = Features.Prominence.AnimacyLevel.human
• Features.Prominence.AnimacyRank.human.toAnimacyLevel = Features.Prominence.AnimacyLevel.human
• Features.Prominence.AnimacyRank.higherAnimal.toAnimacyLevel = Features.Prominence.AnimacyLevel.animate
• Features.Prominence.AnimacyRank.lowerAnimal.toAnimacyLevel = Features.Prominence.AnimacyLevel.animate
• Features.Prominence.AnimacyRank.discreteInanimate.toAnimacyLevel = Features.Prominence.AnimacyLevel.inanimate
• Features.Prominence.AnimacyRank.nondiscreteInanimate.toAnimacyLevel = Features.Prominence.AnimacyLevel.inanimate

theorem Features.Prominence.AnimacyRank.toAnimacyLevel_monotone (r₁ r₂ : AnimacyRank) (h : r₁.toNat ≥ r₂.toNat) : r₁.toAnimacyLevel.rank ≥ r₂.toAnimacyLevel.rank

Coarsening is monotone: higher rank implies ≥ level.

theorem Features.Prominence.AnimacyRank.hierarchy_ordering : speaker.toNat > addressee.toNat ∧ addressee.toNat > thirdPerson.toNat ∧ thirdPerson.toNat > kin.toNat ∧ kin.toNat > human.toNat ∧ human.toNat > higherAnimal.toNat ∧ higherAnimal.toNat > lowerAnimal.toNat ∧ lowerAnimal.toNat > discreteInanimate.toNat ∧ discreteInanimate.toNat > nondiscreteInanimate.toNat

The hierarchy is consistent: speaker outranks addressee outranks third person, and so forth down the scale.

def Features.Prominence.AnimacyRank.respectsHierarchy (markedRanks : List AnimacyRank) : Bool

The hierarchy predicts: if a language marks plural at rank r, it marks plural at all ranks above r.

Equations

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

inductive Features.Prominence.DefinitenessLevel : Type

Levels of the definiteness prominence scale. Personal Pronoun > Proper Name > Definite NP > Indefinite Specific NP > Non-specific NP.

• personalPronoun : DefinitenessLevel

  Most prominent: personal pronouns

• properName : DefinitenessLevel

  Proper names

• definite : DefinitenessLevel

  Definite NPs (with article or demonstrative)

• indefiniteSpecific : DefinitenessLevel

  Indefinite but specific NPs

• nonSpecific : DefinitenessLevel

  Least prominent: non-specific indefinites

@[implicit_reducible]

instance Features.Prominence.instDecidableEqDefinitenessLevel : DecidableEq DefinitenessLevel

Equations

• Features.Prominence.instDecidableEqDefinitenessLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Prominence.instReprDefinitenessLevel.repr : DefinitenessLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prominence.instReprDefinitenessLevel : Repr DefinitenessLevel

Equations

• Features.Prominence.instReprDefinitenessLevel = { reprPrec := Features.Prominence.instReprDefinitenessLevel.repr }

@[implicit_reducible]

instance Features.Prominence.instInhabitedDefinitenessLevel : Inhabited DefinitenessLevel

Equations

• Features.Prominence.instInhabitedDefinitenessLevel = { default := Features.Prominence.instInhabitedDefinitenessLevel.default }

def Features.Prominence.DefinitenessLevel.rank : DefinitenessLevel → ℕ

Numeric rank on the definiteness scale: Pronoun (4) > Proper (3) > Definite (2) > IndSp (1) > NonSp (0).

Equations

• Features.Prominence.DefinitenessLevel.personalPronoun.rank = 4
• Features.Prominence.DefinitenessLevel.properName.rank = 3
• Features.Prominence.DefinitenessLevel.definite.rank = 2
• Features.Prominence.DefinitenessLevel.indefiniteSpecific.rank = 1
• Features.Prominence.DefinitenessLevel.nonSpecific.rank = 0

@[implicit_reducible]

instance Features.Prominence.instLinearOrderDefinitenessLevel : LinearOrder DefinitenessLevel

NonSpecific < IndefiniteSpecific < Definite < ProperName < PersonalPronoun (ordered by prominence rank).

Equations

• Features.Prominence.instLinearOrderDefinitenessLevel = LinearOrder.lift' Features.Prominence.DefinitenessLevel.rank Features.Prominence.instLinearOrderDefinitenessLevel._proof_1

def Features.Prominence.DefinitenessLevel.all : List DefinitenessLevel

All definiteness levels (exhaustive enumeration).

Equations

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

theorem Features.Prominence.DefinitenessLevel.all_length : all.length = 5

theorem Features.Prominence.animacy_rank_injective (a b : AnimacyLevel) (h : a.rank = b.rank) : a = b

Distinct animacy levels have distinct ranks — the rank function is injective.

theorem Features.Prominence.animacy_rank_bounded (a : AnimacyLevel) : a.rank ≤ 2

Animacy ranks are bounded: 0 ≤ rank ≤ 2.

theorem Features.Prominence.definiteness_rank_injective (a b : DefinitenessLevel) (h : a.rank = b.rank) : a = b

Distinct definiteness levels have distinct ranks — the rank function is injective.

theorem Features.Prominence.definiteness_rank_bounded (d : DefinitenessLevel) : d.rank ≤ 4

Definiteness ranks are bounded: 0 ≤ rank ≤ 4.

def Person.prominence : Person → ℕ

Numeric rank on the person prominence scale: 1st (2) > 2nd (1) > 3rd (0) ([Has21] §6). Stated over the canonical Person inventory (the dissolved Person's role): clusivity-marked firsts rank with first; the impersonal zero is [−participant] and is placed with third person (a linglib convention — the scale's source does not discuss impersonals).

Equations

• Person.first.prominence = 2
• Person.firstInclusive.prominence = 2
• Person.firstExclusive.prominence = 2
• Person.second.prominence = 1
• Person.third.prominence = 0
• Person.zero.prominence = 0

@[reducible, inline]

abbrev Features.Prominence.personScaleLevels : List Person

The three-way prominence scale carrier: the tripartition values.

Equations

• Features.Prominence.personScaleLevels = Person.System.tripartition.values

theorem Features.Prominence.person_prominence_injective (a : Person) : a ∈ personScaleLevels → ∀ b ∈ personScaleLevels, a.prominence = b.prominence → a = b

Prominence separates the tripartition: on first/second/third the rank function is injective.

theorem Features.Prominence.person_prominence_bounded (p : Person) : p.prominence ≤ 2

Person prominence ranks are bounded: 0 ≤ rank ≤ 2.

theorem Features.Prominence.prominence_pos_iff_sap (p : Person) : 1 ≤ p.prominence ↔ p.IsSAP

Prominence tracks SAP-hood: rank ≥ 1 iff speech-act participant.

inductive Features.Prominence.ArgumentRole : Type

Argument roles spanning monotransitive and ditransitive clauses.

Follows [Com78] and [Has21] in using S/A/P/R/T (not subject/object) to avoid theory-dependent constituency assumptions.

Role rank determines the direction of differential marking:

• Higher-rank roles (A, R) default to high prominence; differential marking targets the NON-prominent end (anti-monotone / lower set).
• Lower-rank roles (P, T) default to low prominence; differential marking targets the PROMINENT end (monotone / upper set).
• S is the alignment reference point.

• S : ArgumentRole

  S: sole argument of an intransitive verb

• A : ArgumentRole

  A: the more agent-like argument of a transitive verb

• P : ArgumentRole

  P: the more patient-like argument of a transitive verb

• R : ArgumentRole

  R: the recipient-like argument of a ditransitive verb

• T : ArgumentRole

  T: the theme-like argument of a ditransitive verb

@[implicit_reducible]

instance Features.Prominence.instDecidableEqArgumentRole : DecidableEq ArgumentRole

Equations

• Features.Prominence.instDecidableEqArgumentRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prominence.instReprArgumentRole : Repr ArgumentRole

Equations

• Features.Prominence.instReprArgumentRole = { reprPrec := Features.Prominence.instReprArgumentRole.repr }

def Features.Prominence.instReprArgumentRole.repr : ArgumentRole → ℕ → Std.Format

Equations

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

def Features.Prominence.ArgumentRole.roleRank : ArgumentRole → ℕ

Role rank: A > P for monotransitives, R > T for ditransitives. S is in between. Higher rank = higher default prominence expectation.

Equations

• Features.Prominence.ArgumentRole.A.roleRank = 4
• Features.Prominence.ArgumentRole.R.roleRank = 3
• Features.Prominence.ArgumentRole.S.roleRank = 2
• Features.Prominence.ArgumentRole.T.roleRank = 1
• Features.Prominence.ArgumentRole.P.roleRank = 0

def Features.Prominence.ArgumentRole.highDefault : ArgumentRole → Bool

Whether this role has high default prominence (A-like). Differential marking for high-default roles targets non-prominent referents.

Equations

• Features.Prominence.ArgumentRole.A.highDefault = true
• Features.Prominence.ArgumentRole.R.highDefault = true
• x✝.highDefault = false

def Features.Prominence.ArgumentRole.lowDefault : ArgumentRole → Bool

Whether this role has low default prominence (P-like). Differential marking for low-default roles targets prominent referents.

Equations

• Features.Prominence.ArgumentRole.P.lowDefault = true
• Features.Prominence.ArgumentRole.T.lowDefault = true
• x✝.lowDefault = false

inductive Features.Prominence.MarkingChannel : Type

Two independent channels for marking argument properties on verbs or NPs ([Has19], [Jus24] §2).

• Flagging: morphological case on the NP (e.g., accusative suffix)
• Indexing: verbal agreement / cross-referencing (e.g., Set A/B markers)

These serve distinct functions: flagging disambiguates roles, indexing tracks referents. Both are governed by the same prominence scales but the two dimensions are logically independent.

• flagging : MarkingChannel

  Case morphology on the NP

• indexing : MarkingChannel

  Verbal agreement / cross-referencing

@[implicit_reducible]

instance Features.Prominence.instDecidableEqMarkingChannel : DecidableEq MarkingChannel

Equations

• Features.Prominence.instDecidableEqMarkingChannel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Prominence.instReprMarkingChannel.repr : MarkingChannel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prominence.instReprMarkingChannel : Repr MarkingChannel

Equations

• Features.Prominence.instReprMarkingChannel = { reprPrec := Features.Prominence.instReprMarkingChannel.repr }

def Features.Prominence.prominenceRank (a : AnimacyLevel) (d : DefinitenessLevel) : ℕ

Combined prominence rank for a cell in the animacy × definiteness grid. Sum of the two individual ranks, giving a scalar from 0 (inanimate, nonspecific) to 6 (human, personal pronoun).

Equations

• Features.Prominence.prominenceRank a d = a.rank + d.rank

def Features.Prominence.isDefaultZone (role : ArgumentRole) (a : AnimacyLevel) (d : DefinitenessLevel) : Bool

Default prominence expectation per argument role.

High-default roles (A, R) are typically human, definite, topical. Low-default roles (P, T) are typically inanimate, indefinite. S is the reference point — no strong default.

Differential marking targets departures from these defaults:

• P/T marking targets prominent referents (high prominence, unexpected)
• A/R marking targets non-prominent referents (low prominence, unexpected)

Returns true when the cell represents the "expected" (unmarked) zone.

Equations

• Features.Prominence.isDefaultZone Features.Prominence.ArgumentRole.A a d = decide (Features.Prominence.prominenceRank a d ≥ 3)
• Features.Prominence.isDefaultZone Features.Prominence.ArgumentRole.R a d = decide (Features.Prominence.prominenceRank a d ≥ 3)
• Features.Prominence.isDefaultZone Features.Prominence.ArgumentRole.S a d = true
• Features.Prominence.isDefaultZone Features.Prominence.ArgumentRole.P a d = decide (Features.Prominence.prominenceRank a d ≤ 2)
• Features.Prominence.isDefaultZone Features.Prominence.ArgumentRole.T a d = decide (Features.Prominence.prominenceRank a d ≤ 2)

structure Features.Prominence.DifferentialMarkingProfile : Type

A differential marking profile: which cells in the animacy × definiteness grid receive overt differential marking for a given argument role and channel.

Covers all four combinations of role × channel: P flagging, A flagging, P indexing, A indexing.

• name : String

  Language name

• role : ArgumentRole

  Which argument role: A or P

• channel : MarkingChannel

  Realization channel: flagging (case) or indexing (agreement)

• marks : AnimacyLevel → DefinitenessLevel → Bool

  Whether cell (a, d) receives differential marking

def Features.Prominence.DifferentialMarkingProfile.isMonotoneP (p : DifferentialMarkingProfile) : Bool

Monotonicity for P marking (upper set): if a cell is marked, all more prominent cells are also marked. This is [Ais03]'s staircase prediction, extended to P indexing by [Jus24].

Equations

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

def Features.Prominence.DifferentialMarkingProfile.isMonotoneA (p : DifferentialMarkingProfile) : Bool

Anti-monotonicity for A marking (lower set): if a cell is marked, all less prominent cells are also marked. This is the "mirror image" predicted by [Jus24]: A indexing marks non-prominent As.

Equations

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

theorem Features.Prominence.DifferentialMarkingProfile.isMonotoneP_of (p : DifferentialMarkingProfile) (h : ∀ {a a' : AnimacyLevel} {d d' : DefinitenessLevel}, a ≤ a' → d ≤ d' → p.marks a d = true → p.marks a' d' = true) : p.isMonotoneP = true

Wiring to the scale order: pointwise monotonicity (marking closed under moving up both scales) yields the isMonotoneP staircase. A one-dimensional cutoff discharges the hypothesis with le_trans on the scale's LinearOrder (Core.Order.atOrAbove_isUpperSet), so cutoff profiles inherit monotonicity from the order rather than decide.

theorem Features.Prominence.DifferentialMarkingProfile.isMonotoneA_of (p : DifferentialMarkingProfile) (h : ∀ {a a' : AnimacyLevel} {d d' : DefinitenessLevel}, a' ≤ a → d' ≤ d → p.marks a d = true → p.marks a' d' = true) : p.isMonotoneA = true

Anti-monotone (lower-set) counterpart of isMonotoneP_of, for A/R roles.

def Features.Prominence.DifferentialMarkingProfile.isMonotone (p : DifferentialMarkingProfile) : Bool

Role-appropriate monotonicity: low-default roles (P, T) must be monotone (upper set), high-default roles (A, R) must be anti-monotone (lower set). S profiles are vacuously monotone.

Equations

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

def Features.Prominence.DifferentialMarkingProfile.isAnimacyOnly (p : DifferentialMarkingProfile) : Bool

Whether a marking profile depends only on animacy (definiteness is irrelevant).

Equations

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

def Features.Prominence.DifferentialMarkingProfile.isDefinitenessOnly (p : DifferentialMarkingProfile) : Bool

Whether a marking profile depends only on definiteness (animacy is irrelevant).

Equations

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

def Features.Prominence.DifferentialMarkingProfile.animacyCutoffP (name : String) (channel : MarkingChannel) (cutoff : AnimacyLevel) : DifferentialMarkingProfile

Construct a one-dimensional animacy-based P-marking profile: P arguments at or above the cutoff are marked. (For A marking, use animacyCutoffA.) The cutoff is the scale's LinearOrder (Core.Order.atOrAbove), not a raw rank comparison.

Equations

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

def Features.Prominence.DifferentialMarkingProfile.definitenessCutoffP (name : String) (channel : MarkingChannel) (cutoff : DefinitenessLevel) : DifferentialMarkingProfile

Construct a one-dimensional definiteness-based P-marking profile.

Equations

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

def Features.Prominence.DifferentialMarkingProfile.animacyCutoffA (name : String) (channel : MarkingChannel) (cutoff : AnimacyLevel) : DifferentialMarkingProfile

Construct a one-dimensional animacy-based A-marking profile: A arguments at or below the cutoff are marked (anti-monotone / lower set).

Equations

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

def Features.Prominence.DifferentialMarkingProfile.definitenessCutoffA (name : String) (channel : MarkingChannel) (cutoff : DefinitenessLevel) : DifferentialMarkingProfile

Construct a one-dimensional definiteness-based A-marking profile.

Equations

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

theorem Features.Prominence.animacyCutoffP_monotone (ch : MarkingChannel) (cutoff : AnimacyLevel) : (DifferentialMarkingProfile.animacyCutoffP "" ch cutoff).isMonotone = true

Animacy-cutoff P profiles are always monotone — the marked region is the upper set Core.Order.atOrAbove cutoff on the animacy axis, lifted through isMonotoneP_of by le_trans.

theorem Features.Prominence.definitenessCutoffP_monotone (ch : MarkingChannel) (cutoff : DefinitenessLevel) : (DifferentialMarkingProfile.definitenessCutoffP "" ch cutoff).isMonotone = true

Definiteness-cutoff P profiles are always monotone — same isMonotoneP_of

• le_trans, now on the definiteness axis.

theorem Features.Prominence.animacyCutoffA_monotone (ch : MarkingChannel) (cutoff : AnimacyLevel) : (DifferentialMarkingProfile.animacyCutoffA "" ch cutoff).isMonotone = true

Animacy-cutoff A profiles are always anti-monotone (lower set).

theorem Features.Prominence.definitenessCutoffA_monotone (ch : MarkingChannel) (cutoff : DefinitenessLevel) : (DifferentialMarkingProfile.definitenessCutoffA "" ch cutoff).isMonotone = true

Definiteness-cutoff A profiles are always anti-monotone (lower set).

theorem Features.Prominence.animacy_mirror_image (cutoff : AnimacyLevel) : (AnimacyLevel.all.all fun (a : AnimacyLevel) => DefinitenessLevel.all.all fun (d : DefinitenessLevel) => (DifferentialMarkingProfile.animacyCutoffP "" MarkingChannel.indexing cutoff).marks a d || (DifferentialMarkingProfile.animacyCutoffA "" MarkingChannel.indexing cutoff).marks a d) = true

For any one-dimensional animacy cutoff, P marking at level c and A marking at level c produce complementary profiles: every cell is marked by exactly one of them (except the cutoff row itself, marked by both).

structure Features.Prominence.Scenario : Type

A monotransitive scenario: the person combination of A and P.

Scenario splits arise when argument coding depends not on a single argument's prominence but on the combination of A-person and P-person. E.g., 1→3 ("I see him") vs. 3→1 ("He sees me") may get different flagging or indexing.

• aPerson : Person

  Person of the A argument

• pPerson : Person

  Person of the P argument

def Features.Prominence.instDecidableEqScenario.decEq (x✝ x✝¹ : Scenario) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Features.Prominence.instDecidableEqScenario : DecidableEq Scenario

Equations

• Features.Prominence.instDecidableEqScenario = Features.Prominence.instDecidableEqScenario.decEq

def Features.Prominence.instReprScenario.repr : Scenario → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prominence.instReprScenario : Repr Scenario

Equations

• Features.Prominence.instReprScenario = { reprPrec := Features.Prominence.instReprScenario.repr }

def Features.Prominence.Scenario.isDownstream (s : Scenario) : Bool

Whether a scenario is "downstream": A has higher person rank than P. This is the "usual" direction — the role-reference association predicts high-rank roles (A) to have high-prominence referents. Downstream scenarios tend to get the shortest coding.

Equations

• s.isDownstream = decide (s.aPerson.prominence > s.pPerson.prominence)

def Features.Prominence.Scenario.isUpstream (s : Scenario) : Bool

Whether a scenario is "upstream": P has higher person rank than A. This is the "unusual" direction — against the role-reference association. Upstream scenarios tend to get the longest coding.

Equations

• s.isUpstream = decide (s.aPerson.prominence < s.pPerson.prominence)

def Features.Prominence.Scenario.isBalanced (s : Scenario) : Bool

Whether a scenario is "balanced": A and P have the same person rank (e.g., 3→3). Intermediate coding predicted.

Equations

• s.isBalanced = (s.aPerson.prominence == s.pPerson.prominence)

def Features.Prominence.Scenario.isLocal (s : Scenario) : Bool

Whether a scenario is "local": both arguments are SAP (1st or 2nd). Local scenarios (1↔2) are frequent and tend to get short coding.

Equations

• s.isLocal = (decide s.aPerson.IsSAP && decide s.pPerson.IsSAP)

def Features.Prominence.Scenario.isDirect (s : Scenario) : Bool

Whether a scenario is "direct": SAP acts on 3rd person. A subtype of downstream scenarios.

Equations

• s.isDirect = (decide s.aPerson.IsSAP && !decide s.pPerson.IsSAP)

def Features.Prominence.Scenario.isInverse (s : Scenario) : Bool

Whether a scenario is "inverse": 3rd person acts on SAP. A subtype of upstream scenarios.

Equations

• s.isInverse = (!decide s.aPerson.IsSAP && decide s.pPerson.IsSAP)

def Features.Prominence.Scenario.isNonlocal (s : Scenario) : Bool

Whether a scenario is "non-local": 3rd person acts on 3rd person. A subtype of balanced scenarios.

Equations

• s.isNonlocal = (!decide s.aPerson.IsSAP && !decide s.pPerson.IsSAP)

def Features.Prominence.Scenario.all : List Scenario

All 9 person-pair scenarios. Explicit literal so decide reduces; the equivalent map over personScaleLevels pairs typechecks but defeats kernel-level decide over Scenario.all.all (...).

Equations

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

theorem Features.Prominence.Scenario.all_length : all.length = 9

def Features.Prominence.differentialTargetsProminent (r : ArgumentRole) : Bool

The direction of differential marking: for a given role, does differential coding target the prominent end (upper set) or the non-prominent end (lower set)?

Returns true when differential marking targets the prominent end. P and T → true (mark prominent referents); A and R → false (mark non-prominent referents); S → false.

Definitionally r.lowDefault — the two functions agree pointwise over all five argument roles. The aliasing makes U3, U7, U8 in Studies/Haspelmath2021.lean rfl against the substrate, rather than re-proving the equality in the study file.

Equations

• Features.Prominence.differentialTargetsProminent r = r.lowDefault

theorem Features.Prominence.R_like_A_default : ArgumentRole.R.highDefault = ArgumentRole.A.highDefault

R behaves like A: both have high default prominence and differential marking targets the non-prominent end.

theorem Features.Prominence.T_like_P_default : ArgumentRole.T.lowDefault = ArgumentRole.P.lowDefault

T behaves like P: both have low default prominence and differential marking targets the prominent end.

theorem Features.Prominence.role_rank_ordering : ArgumentRole.A.roleRank > ArgumentRole.R.roleRank ∧ ArgumentRole.R.roleRank > ArgumentRole.S.roleRank ∧ ArgumentRole.S.roleRank > ArgumentRole.T.roleRank ∧ ArgumentRole.T.roleRank > ArgumentRole.P.roleRank

Role rank ordering: A > R > S > T > P.

def Features.Prominence.Scenario.frequencyClass (s : Scenario) : ℕ

Frequency class for scenarios: downstream (usual) most frequent. Downstream = 2, balanced = 1, upstream = 0.

Equations

• s.frequencyClass = if s.isDownstream = true then 2 else if s.isBalanced = true then 1 else 0

def Features.Prominence.Scenario.upstreamDegree (s : Scenario) : ℕ

Gradient upstream degree: how far P's rank exceeds A's. Uses Nat saturating subtraction (negative → 0).

Equations

• s.upstreamDegree = s.pPerson.prominence - s.aPerson.prominence

theorem Features.Prominence.downstream_frequency_class : { aPerson := Person.first, pPerson := Person.third }.frequencyClass = 2

theorem Features.Prominence.upstream_frequency_class : { aPerson := Person.third, pPerson := Person.first }.frequencyClass = 0

theorem Features.Prominence.frequency_class_monotone : { aPerson := Person.first, pPerson := Person.third }.frequencyClass > { aPerson := Person.third, pPerson := Person.third }.frequencyClass ∧ { aPerson := Person.third, pPerson := Person.third }.frequencyClass > { aPerson := Person.third, pPerson := Person.first }.frequencyClass

Frequency class is monotone: downstream > balanced > upstream.