Indexical fields

An indexical field, in Eckert's sense, assigns each variant of a linguistic variable the meanings a use of it may activate, stances, qualities or persona traits, as a function Variant → Finset Meaning. An association field grades the assignment, giving each variant a signed strength toward each trait, positive when the variant indexes the trait and negative when it indexes away from it, and the traits a variant indexes toward form its indexical field.

Main definitions

• AssociationField: the signed strength with which each variant indexes each trait, a matrix over an ordered ring.
• AssociationField.Indexes: a variant indexes a trait, the strength being positive.
• AssociationField.Antipodal: two variants index every trait in opposite directions.
• AssociationField.support: the indexical field of the traits a variant indexes.
• AssociationField.contrast: each variant's strengths less those of a reference variant.
• AssociationField.signs: the sign field of a field.

Main results

• AssociationField.Antipodal.disjoint_support: an antipodal pair index no trait in common.
• AssociationField.antipodal_signs_contrast_iff: two variants are antipodal in the signs of their contrasts with a reference exactly when the reference lies strictly between them, or ties with both, on every trait.

Implementation notes

An association field is a Matrix, so composing associations through a mediating domain, Ochs's indirect indexicality, is matrix multiplication, and inheriting a field along a map of variant spaces is Matrix.submatrix. The carrier is any type with a zero and an order, SignType for the sign-valued fields of Beltrama, Solt and Burnett, an ordered semiring for strengths that compose; Burnett's grounded fields are indexical fields over the Stereotype Content Model properties.

References

• [Eck08]
• [Och92]
• [BSB23]
• [Bur19]

@[reducible, inline]

abbrev SocialMeaning.AssociationField (Variant : Type u_1) (Trait : Type u_2) (R : Type u_3) : Type (max u_1 u_2 u_3)

An association field assigns each variant of a variable a signed strength toward each trait, positive when the variant indexes the trait and negative when it indexes away.

Equations

• SocialMeaning.AssociationField Variant Trait R = Matrix Variant Trait R

def SocialMeaning.AssociationField.Indexes {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Zero R] [LT R] (M : AssociationField Variant Trait R) (v : Variant) (t : Trait) : Prop

A variant indexes a trait when its association with the trait is positive.

Equations

• M.Indexes v t = (0 < M v t)

@[instance_reducible]

instance SocialMeaning.AssociationField.instDecidableRelIndexesOfDecidableLT {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Zero R] [LT R] (M : AssociationField Variant Trait R) [DecidableLT R] : DecidableRel M.Indexes

Equations

• M.instDecidableRelIndexesOfDecidableLT x✝¹ x✝ = SocialMeaning.AssociationField.instDecidableRelIndexesOfDecidableLT._aux_1 M x✝¹ x✝

def SocialMeaning.AssociationField.support {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Zero R] [LT R] (M : AssociationField Variant Trait R) [Fintype Trait] [DecidableLT R] (v : Variant) : Finset Trait

The support of a variant is the indexical field of the traits it indexes.

Equations

• M.support v = Finset.filter (M.Indexes v) Finset.univ

@[simp]

theorem SocialMeaning.AssociationField.mem_support {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v : Variant} {t : Trait} [Zero R] [LT R] (M : AssociationField Variant Trait R) [Fintype Trait] [DecidableLT R] : t ∈ M.support v ↔ M.Indexes v t

def SocialMeaning.AssociationField.Antipodal {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [InvolutiveNeg R] (M : AssociationField Variant Trait R) (v₁ v₂ : Variant) : Prop

Two variants are antipodal when they index every trait in opposite directions.

Equations

• M.Antipodal v₁ v₂ = (M v₁ = -M v₂)

@[instance_reducible]

instance SocialMeaning.AssociationField.instDecidableAntipodalOfFintypeOfDecidableEq {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [InvolutiveNeg R] (M : AssociationField Variant Trait R) [Fintype Trait] [DecidableEq R] (v₁ v₂ : Variant) : Decidable (M.Antipodal v₁ v₂)

Equations

• M.instDecidableAntipodalOfFintypeOfDecidableEq v₁ v₂ = { decide := decide (∀ a ∈ Finset.univ, M v₁ a = (-M v₂) a), reflects_decide := ⋯ }

theorem SocialMeaning.AssociationField.Antipodal.symm {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v₁ v₂ : Variant} [InvolutiveNeg R] {M : AssociationField Variant Trait R} (h : M.Antipodal v₁ v₂) : M.Antipodal v₂ v₁

theorem SocialMeaning.AssociationField.antipodal_comm {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v₁ v₂ : Variant} [InvolutiveNeg R] {M : AssociationField Variant Trait R} : M.Antipodal v₁ v₂ ↔ M.Antipodal v₂ v₁

theorem SocialMeaning.AssociationField.Antipodal.indexes_iff {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v₁ v₂ : Variant} {t : Trait} [AddGroup R] [Preorder R] [AddLeftStrictMono R] {M : AssociationField Variant Trait R} (h : M.Antipodal v₁ v₂) : M.Indexes v₁ t ↔ M v₂ t < 0

An antipodal pair index a trait in opposite directions.

theorem SocialMeaning.AssociationField.Antipodal.disjoint_support {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v₁ v₂ : Variant} [AddGroup R] [Preorder R] [AddLeftStrictMono R] {M : AssociationField Variant Trait R} [Fintype Trait] [DecidableLT R] (h : M.Antipodal v₁ v₂) : Disjoint (M.support v₁) (M.support v₂)

An antipodal pair index no trait in common.

def SocialMeaning.AssociationField.contrast {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Sub R] (M : AssociationField Variant Trait R) (v₀ : Variant) : AssociationField Variant Trait R

The contrast of a field with a reference variant takes each variant's strengths less those of the reference.

Equations

• M.contrast v₀ = Matrix.of fun (v : Variant) (t : Trait) => M v t - M v₀ t

@[simp]

theorem SocialMeaning.AssociationField.contrast_apply {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Sub R] (M : AssociationField Variant Trait R) (v₀ v : Variant) (t : Trait) : M.contrast v₀ v t = M v t - M v₀ t

def SocialMeaning.AssociationField.signs {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] (M : AssociationField Variant Trait R) : AssociationField Variant Trait SignType

The sign field of a field.

Equations

• M.signs = Matrix.map M ⇑SignType.sign

@[simp]

theorem SocialMeaning.AssociationField.signs_apply {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] (M : AssociationField Variant Trait R) (v : Variant) (t : Trait) : M.signs v t = SignType.sign (M v t)

theorem SocialMeaning.AssociationField.lt_of_signs_contrast_lt {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v w : Variant} {t : Trait} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {M : AssociationField Variant Trait R} {v₀ : Variant} (h : (M.contrast v₀).signs v t < (M.contrast v₀).signs w t) : M v t < M w t

The signs of contrasts order two variants on a trait only as the field does.

theorem SocialMeaning.AssociationField.antipodal_signs_contrast_iff {Variant : Type u_1} {Trait : Type u_2} {R : Type u_3} {v₁ v₂ : Variant} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {M : AssociationField Variant Trait R} {v₀ : Variant} : (M.contrast v₀).signs.Antipodal v₁ v₂ ↔ ∀ (t : Trait), M v₀ t ∈ Set.uIoo (M v₁ t) (M v₂ t) ∨ M v₁ t = M v₀ t ∧ M v₂ t = M v₀ t