inductive Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier : Type

The five degree modifiers studied, ordered by strength.

• slightly : Modifier
• kindOf : Modifier
• quite : Modifier
• very : Modifier
• extremely : Modifier

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instDecidableEqModifier : DecidableEq Modifier

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instDecidableEqModifier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqModifier.beq : Modifier → Modifier → Bool

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqModifier.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqModifier : BEq Modifier

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqModifier = { beq := Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqModifier.beq }

def Phenomena.Politeness.Studies.MachinoEtAl2025.instReprModifier.repr : Modifier → ℕ → Std.Format

Equations

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

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instReprModifier : Repr Modifier

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instReprModifier = { reprPrec := Phenomena.Politeness.Studies.MachinoEtAl2025.instReprModifier.repr }

inductive Phenomena.Politeness.Studies.MachinoEtAl2025.Culture : Type

Cultural variety

• americanEnglish : Culture
• britishEnglish : Culture

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instDecidableEqCulture : DecidableEq Culture

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instDecidableEqCulture x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqCulture.beq : Culture → Culture → Bool

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqCulture.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqCulture : BEq Culture

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqCulture = { beq := Phenomena.Politeness.Studies.MachinoEtAl2025.instBEqCulture.beq }

def Phenomena.Politeness.Studies.MachinoEtAl2025.instReprCulture.repr : Culture → ℕ → Std.Format

Equations

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

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instReprCulture : Repr Culture

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instReprCulture = { reprPrec := Phenomena.Politeness.Studies.MachinoEtAl2025.instReprCulture.repr }

def Phenomena.Politeness.Studies.MachinoEtAl2025.modifierRank : Modifier → ℕ

Strength rank (within amplifiers/downtoners separately). Higher = more extreme effect on threshold.

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierRank Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.slightly = 1
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierRank Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.kindOf = 2
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierRank Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.quite = 3
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierRank Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.very = 4
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierRank Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.extremely = 5

structure Phenomena.Politeness.Studies.MachinoEtAl2025.InterpretationDatum : Type

A modifier interpretation datum

• modifier : Modifier
• culture : Culture
• meanState : Float

  Mean interpreted state (0–3 scale, like Yoon et al. heart states)

• notes : String

  Higher meanState = modifier pushes interpretation toward higher quality

def Phenomena.Politeness.Studies.MachinoEtAl2025.instReprInterpretationDatum.repr : InterpretationDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instReprInterpretationDatum : Repr InterpretationDatum

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instReprInterpretationDatum = { reprPrec := Phenomena.Politeness.Studies.MachinoEtAl2025.instReprInterpretationDatum.repr }

def Phenomena.Politeness.Studies.MachinoEtAl2025.ame_slightly : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.ame_kindOf : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.ame_quite : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.ame_very : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.ame_extremely : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.bre_slightly : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.bre_kindOf : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.bre_quite : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.bre_very : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.bre_extremely : InterpretationDatum

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.interpretationData : List InterpretationDatum

All interpretation data

Equations

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

structure Phenomena.Politeness.Studies.MachinoEtAl2025.PolitenessRating : Type

Politeness rating datum

• modifier : Modifier
• culture : Culture
• rating : Float

  Mean politeness rating (1–7 Likert scale)

• notes : String

instance Phenomena.Politeness.Studies.MachinoEtAl2025.instReprPolitenessRating : Repr PolitenessRating

Equations

• Phenomena.Politeness.Studies.MachinoEtAl2025.instReprPolitenessRating = { reprPrec := Phenomena.Politeness.Studies.MachinoEtAl2025.instReprPolitenessRating.repr }

def Phenomena.Politeness.Studies.MachinoEtAl2025.instReprPolitenessRating.repr : PolitenessRating → ℕ → Std.Format

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.politeness_slightly_ame : PolitenessRating

Downtoners are rated as more polite than amplifiers. This is the key connection to Yoon et al.: hedging = politeness strategy.

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.politeness_very_ame : PolitenessRating

Equations

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

def Phenomena.Politeness.Studies.MachinoEtAl2025.modifierDirection : Culture → Modifier → Semantics.Degree.ModifierDirection

Culture-specific modifier direction. Key finding: "quite" differs across varieties.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierDirection x✝ Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.slightly = Semantics.Degree.ModifierDirection.downtoner
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierDirection x✝ Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.kindOf = Semantics.Degree.ModifierDirection.downtoner
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierDirection x✝ Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.very = Semantics.Degree.ModifierDirection.amplifier
• Phenomena.Politeness.Studies.MachinoEtAl2025.modifierDirection x✝ Phenomena.Politeness.Studies.MachinoEtAl2025.Modifier.extremely = Semantics.Degree.ModifierDirection.amplifier