Prominence Scales and Differential Argument Marking @cite{just-2024} @cite{haspelmath-2021}

@cite{aissen-2003} @cite{haspelmath-2019}

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 @cite{just-2024} and building on @cite{aissen-2003}.

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 (@cite{haspelmath-2021}, §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 Core.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

instance Core.Prominence.instDecidableEqAnimacyLevel : DecidableEq AnimacyLevel

Equations

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

instance Core.Prominence.instBEqAnimacyLevel : BEq AnimacyLevel

Equations

• Core.Prominence.instBEqAnimacyLevel = { beq := Core.Prominence.instBEqAnimacyLevel.beq }

def Core.Prominence.instBEqAnimacyLevel.beq : AnimacyLevel → AnimacyLevel → Bool

Equations

• Core.Prominence.instBEqAnimacyLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Prominence.instReprAnimacyLevel.repr : AnimacyLevel → Nat → Std.Format

Equations

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

instance Core.Prominence.instReprAnimacyLevel : Repr AnimacyLevel

Equations

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

instance Core.Prominence.instInhabitedAnimacyLevel : Inhabited AnimacyLevel

Equations

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

def Core.Prominence.instInhabitedAnimacyLevel.default : AnimacyLevel

Equations

• Core.Prominence.instInhabitedAnimacyLevel.default = Core.Prominence.AnimacyLevel.human

def Core.Prominence.AnimacyLevel.rank : AnimacyLevel → Nat

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

Equations

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

def Core.Prominence.AnimacyLevel.all : List AnimacyLevel

All animacy levels (exhaustive enumeration for finite verification).

Equations

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

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

inductive Core.Prominence.AnimacyRank : Type

Fine-grained animacy hierarchy for nominal plural marking and agreement (@cite{smith-stark-1974}, @cite{corbett-2000}).

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

instance Core.Prominence.instDecidableEqAnimacyRank : DecidableEq AnimacyRank

Equations

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

def Core.Prominence.instBEqAnimacyRank.beq : AnimacyRank → AnimacyRank → Bool

Equations

• Core.Prominence.instBEqAnimacyRank.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Prominence.instBEqAnimacyRank : BEq AnimacyRank

Equations

• Core.Prominence.instBEqAnimacyRank = { beq := Core.Prominence.instBEqAnimacyRank.beq }

instance Core.Prominence.instReprAnimacyRank : Repr AnimacyRank

Equations

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

def Core.Prominence.instReprAnimacyRank.repr : AnimacyRank → Nat → Std.Format

Equations

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

def Core.Prominence.AnimacyRank.toNat : AnimacyRank → Nat

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

Equations

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

def Core.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

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

theorem Core.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 Core.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 Core.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 Core.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

instance Core.Prominence.instDecidableEqDefinitenessLevel : DecidableEq DefinitenessLevel

Equations

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

def Core.Prominence.instBEqDefinitenessLevel.beq : DefinitenessLevel → DefinitenessLevel → Bool

Equations

• Core.Prominence.instBEqDefinitenessLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Prominence.instBEqDefinitenessLevel : BEq DefinitenessLevel

Equations

• Core.Prominence.instBEqDefinitenessLevel = { beq := Core.Prominence.instBEqDefinitenessLevel.beq }

def Core.Prominence.instReprDefinitenessLevel.repr : DefinitenessLevel → Nat → Std.Format

Equations

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

instance Core.Prominence.instReprDefinitenessLevel : Repr DefinitenessLevel

Equations

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

instance Core.Prominence.instInhabitedDefinitenessLevel : Inhabited DefinitenessLevel

Equations

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

def Core.Prominence.instInhabitedDefinitenessLevel.default : DefinitenessLevel

Equations

• Core.Prominence.instInhabitedDefinitenessLevel.default = Core.Prominence.DefinitenessLevel.personalPronoun

def Core.Prominence.DefinitenessLevel.rank : DefinitenessLevel → Nat

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

Equations

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

def Core.Prominence.DefinitenessLevel.all : List DefinitenessLevel

All definiteness levels (exhaustive enumeration).

Equations

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

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

theorem Core.Prominence.animacy_human_gt_animate : AnimacyLevel.human.rank > AnimacyLevel.animate.rank

theorem Core.Prominence.animacy_animate_gt_inanimate : AnimacyLevel.animate.rank > AnimacyLevel.inanimate.rank

theorem Core.Prominence.definiteness_pronoun_gt_proper : DefinitenessLevel.personalPronoun.rank > DefinitenessLevel.properName.rank

theorem Core.Prominence.definiteness_proper_gt_definite : DefinitenessLevel.properName.rank > DefinitenessLevel.definite.rank

theorem Core.Prominence.definiteness_definite_gt_indSp : DefinitenessLevel.definite.rank > DefinitenessLevel.indefiniteSpecific.rank

theorem Core.Prominence.definiteness_indSp_gt_nonSp : DefinitenessLevel.indefiniteSpecific.rank > DefinitenessLevel.nonSpecific.rank

inductive Core.Prominence.PersonLevel : Type

Person prominence scale. 1st > 2nd > 3rd. SAP (speech-act participants, 1st/2nd) are more prominent than 3rd person.

• first : PersonLevel
• second : PersonLevel
• third : PersonLevel

instance Core.Prominence.instDecidableEqPersonLevel : DecidableEq PersonLevel

Equations

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

instance Core.Prominence.instBEqPersonLevel : BEq PersonLevel

Equations

• Core.Prominence.instBEqPersonLevel = { beq := Core.Prominence.instBEqPersonLevel.beq }

def Core.Prominence.instBEqPersonLevel.beq : PersonLevel → PersonLevel → Bool

Equations

• Core.Prominence.instBEqPersonLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Prominence.instReprPersonLevel.repr : PersonLevel → Nat → Std.Format

Equations

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

instance Core.Prominence.instReprPersonLevel : Repr PersonLevel

Equations

• Core.Prominence.instReprPersonLevel = { reprPrec := Core.Prominence.instReprPersonLevel.repr }

def Core.Prominence.instInhabitedPersonLevel.default : PersonLevel

Equations

• Core.Prominence.instInhabitedPersonLevel.default = Core.Prominence.PersonLevel.first

instance Core.Prominence.instInhabitedPersonLevel : Inhabited PersonLevel

Equations

• Core.Prominence.instInhabitedPersonLevel = { default := Core.Prominence.instInhabitedPersonLevel.default }

def Core.Prominence.PersonLevel.rank : PersonLevel → Nat

Numeric rank on the person scale: 1st (2) > 2nd (1) > 3rd (0).

Equations

• Core.Prominence.PersonLevel.first.rank = 2
• Core.Prominence.PersonLevel.second.rank = 1
• Core.Prominence.PersonLevel.third.rank = 0

def Core.Prominence.PersonLevel.all : List PersonLevel

All person levels.

Equations

• Core.Prominence.PersonLevel.all = [Core.Prominence.PersonLevel.first, Core.Prominence.PersonLevel.second, Core.Prominence.PersonLevel.third]

def Core.Prominence.PersonLevel.isSAP : PersonLevel → Bool

Whether a person level is a speech-act participant (SAP = local).

Equations

• Core.Prominence.PersonLevel.first.isSAP = true
• Core.Prominence.PersonLevel.second.isSAP = true
• Core.Prominence.PersonLevel.third.isSAP = false

theorem Core.Prominence.person_first_gt_second : PersonLevel.first.rank > PersonLevel.second.rank

theorem Core.Prominence.person_second_gt_third : PersonLevel.second.rank > PersonLevel.third.rank

inductive Core.Prominence.ArgumentRole : Type

Argument roles spanning monotransitive and ditransitive clauses.

Follows @cite{comrie-1978} and @cite{haspelmath-2021} 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

instance Core.Prominence.instDecidableEqArgumentRole : DecidableEq ArgumentRole

Equations

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

def Core.Prominence.instBEqArgumentRole.beq : ArgumentRole → ArgumentRole → Bool

Equations

• Core.Prominence.instBEqArgumentRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Prominence.instBEqArgumentRole : BEq ArgumentRole

Equations

• Core.Prominence.instBEqArgumentRole = { beq := Core.Prominence.instBEqArgumentRole.beq }

def Core.Prominence.instReprArgumentRole.repr : ArgumentRole → Nat → Std.Format

Equations

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

instance Core.Prominence.instReprArgumentRole : Repr ArgumentRole

Equations

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

def Core.Prominence.ArgumentRole.roleRank : ArgumentRole → Nat

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

Equations

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

def Core.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

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

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

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

Equations

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

inductive Core.Prominence.MarkingChannel : Type

Two independent channels for marking argument properties on verbs or NPs (@cite{haspelmath-2019}, @cite{just-2024} §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

instance Core.Prominence.instDecidableEqMarkingChannel : DecidableEq MarkingChannel

Equations

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

def Core.Prominence.instBEqMarkingChannel.beq : MarkingChannel → MarkingChannel → Bool

Equations

• Core.Prominence.instBEqMarkingChannel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Prominence.instBEqMarkingChannel : BEq MarkingChannel

Equations

• Core.Prominence.instBEqMarkingChannel = { beq := Core.Prominence.instBEqMarkingChannel.beq }

instance Core.Prominence.instReprMarkingChannel : Repr MarkingChannel

Equations

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

def Core.Prominence.instReprMarkingChannel.repr : MarkingChannel → Nat → Std.Format

Equations

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

def Core.Prominence.prominenceRank (a : AnimacyLevel) (d : DefinitenessLevel) : Nat

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

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

def Core.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

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

structure Core.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 Core.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 @cite{aissen-2003}'s staircase prediction, extended to P indexing by @cite{just-2024}.

Equations

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

def Core.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 @cite{just-2024}: A indexing marks non-prominent As.

Equations

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

def Core.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 Core.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 Core.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 Core.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.)

Equations

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

def Core.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 Core.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 Core.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 Core.Prominence.animacyCutoffP_monotone (ch : MarkingChannel) (cutoff : AnimacyLevel) : (DifferentialMarkingProfile.animacyCutoffP "" ch cutoff).isMonotone = true

Animacy-cutoff P profiles are always monotone.

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

Definiteness-cutoff P profiles are always monotone.

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

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

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

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

theorem Core.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 Core.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 : PersonLevel

  Person of the A argument

• pPerson : PersonLevel

  Person of the P argument

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

Equations

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

instance Core.Prominence.instDecidableEqScenario : DecidableEq Scenario

Equations

• Core.Prominence.instDecidableEqScenario = Core.Prominence.instDecidableEqScenario.decEq

instance Core.Prominence.instBEqScenario : BEq Scenario

Equations

• Core.Prominence.instBEqScenario = { beq := Core.Prominence.instBEqScenario.beq }

def Core.Prominence.instBEqScenario.beq : Scenario → Scenario → Bool

Equations

• Core.Prominence.instBEqScenario.beq { aPerson := a, pPerson := a_1 } { aPerson := b, pPerson := b_1 } = (a == b && a_1 == b_1)
• Core.Prominence.instBEqScenario.beq x✝¹ x✝ = false

instance Core.Prominence.instReprScenario : Repr Scenario

Equations

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

def Core.Prominence.instReprScenario.repr : Scenario → Nat → Std.Format

Equations

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

def Core.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.rank > s.pPerson.rank)

def Core.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.rank < s.pPerson.rank)

def Core.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.rank == s.pPerson.rank)

def Core.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 = (s.aPerson.isSAP && s.pPerson.isSAP)

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

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

Equations

• s.isDirect = (s.aPerson.isSAP && !s.pPerson.isSAP)

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

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

Equations

• s.isInverse = (!s.aPerson.isSAP && s.pPerson.isSAP)

def Core.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 = (!s.aPerson.isSAP && !s.pPerson.isSAP)

def Core.Prominence.Scenario.all : List Scenario

All 9 person-pair scenarios.

Equations

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

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

def Core.Prominence.differentialTargetsProminent : 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).

Equations

• Core.Prominence.differentialTargetsProminent Core.Prominence.ArgumentRole.P = true
• Core.Prominence.differentialTargetsProminent Core.Prominence.ArgumentRole.T = true
• Core.Prominence.differentialTargetsProminent Core.Prominence.ArgumentRole.A = false
• Core.Prominence.differentialTargetsProminent Core.Prominence.ArgumentRole.R = false
• Core.Prominence.differentialTargetsProminent Core.Prominence.ArgumentRole.S = false

theorem Core.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 Core.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 Core.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 Core.Prominence.Scenario.frequencyClass (s : Scenario) : Nat

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 Core.Prominence.Scenario.upstreamDegree (s : Scenario) : Nat

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

Equations

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

theorem Core.Prominence.downstream_frequency_class : { aPerson := PersonLevel.first, pPerson := PersonLevel.third }.frequencyClass = 2

theorem Core.Prominence.upstream_frequency_class : { aPerson := PersonLevel.third, pPerson := PersonLevel.first }.frequencyClass = 0

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

Frequency class is monotone: downstream > balanced > upstream.