Documentation

Studies.Eckert2008

Eckert (2008): Variation and the indexical field #

This file formalizes the indexical field of [Eck08]. On [Sil03]'s indexical order, a first-order index marks membership in a population and every nth-order value is available for an n + 1st reconstrual, so the paper takes the meaning of a variable to be not a fixed category but the constellation of ideologically linked meanings that continual reconstrual creates, any of which a situated use may activate. An ideological field records what each meaning is available to be construed as (IdeologicalField), a reconstrual adds those construals to a set of meanings, and the indexical field of a first-order index is its closure under reconstrual, a closure operator whose closed sets are the sets no reconstrual extends.

The examples are the paper's. [Lab63]'s Martha's Vineyard (ay) is an indicator become a marker. The (ING) field of Figure 3, after [CK07], holds favourable and unfavourable meanings for both variants, and a hearer expects the variant whose field holds the impression formed of the speaker. The stances of the /t/ release field of Figure 4 accrete into qualities, social types anchor the field, and [Pod07]'s diva combines the two extremes of the articulation continuum. Among the Belten High groups of Figure 1, the burnout girls alone are among the leaders of every variable.

Implementation notes #

Figures 3 and 4 are recorded as printed and the ideological links as the text states them; the graded strengths of SocialMeaning.AssociationField are not in the paper. Leads marks a group among the greatest or second-greatest users of Figure 1 and is derived from the text's two generalizations, that girls lead the older changes and burnouts the newer. The burned-out burnout girls, the Beijing variables of Figure 2 from [Zha05], Podesva's release-rate measurements and the (DH) discussion are not represented.

References #

Indexical order and the indexical field #

@[reducible, inline]

abbrev Eckert2008.IdeologicalField (T : Type u_1) :

Type u_1

An ideological field records, for each potential meaning, the meanings it is available to be construed as, the links along which an nth-order value acquires an n + 1st.

Equations

Eckert2008.IdeologicalField T = (T → Finset T)

Instances For

def Eckert2008.IdeologicalField.construe {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) (S : Finset T) :

Finset T

One reconstrual of S adds to its meanings everything they are construed as.

Equations

I.construe S = S ∪ S.biUnion I

Instances For

@[simp]

theorem Eckert2008.IdeologicalField.mem_construe {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) {S : Finset T} {t : T} :

t ∈ I.construe S ↔ t ∈ S ∨ ∃ s ∈ S, t ∈ I s

theorem Eckert2008.IdeologicalField.subset_construe {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) (S : Finset T) :

S ⊆ I.construe S

theorem Eckert2008.IdeologicalField.construe_mono {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) :

Monotone I.construe

theorem Eckert2008.IdeologicalField.monotone_construe_iterate {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) (S : Finset T) :

Monotone fun (n : ℕ) => I.construe^[n] S

Reconstrual only adds meanings, so the values of order n are among those of order n + 1.

def Eckert2008.IdeologicalField.indexicalField {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) [Fintype T] :

ClosureOperator (Finset T)

The indexical field of a first-order index is its closure under the ideological links, every meaning the index is continually reconstrued as.

Equations

I.indexicalField = ClosureOperator.mk₂ (fun (S : Finset T) => {t : T | ∃ s ∈ S, Relation.ReflTransGen (fun (a b : T) => b ∈ I a) s t}) ⋯ ⋯

Instances For

@[simp]

theorem Eckert2008.IdeologicalField.mem_indexicalField {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) {S : Finset T} {t : T} [Fintype T] :

t ∈ I.indexicalField S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun (a b : T) => b ∈ I a) s t

theorem Eckert2008.IdeologicalField.iterate_construe_subset_indexicalField {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) [Fintype T] (n : ℕ) (S : Finset T) :

I.construe^[n] S ⊆ I.indexicalField S

The reconstruals of every order lie in the field.

theorem Eckert2008.IdeologicalField.mem_indexicalField_iff_exists_iterate {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) {S : Finset T} {t : T} [Fintype T] :

t ∈ I.indexicalField S ↔ ∃ (n : ℕ), t ∈ I.construe^[n] S

Continual reconstrual creates, in the end, the indexical field, a meaning lying in the field exactly when some order of reconstrual reaches it.

theorem Eckert2008.IdeologicalField.isClosed_iff {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) {S : Finset T} [Fintype T] :

I.indexicalField.IsClosed S ↔ I.construe S = S

A set of meanings is closed exactly when no reconstrual extends it.

theorem Eckert2008.IdeologicalField.indexicalField_eq_iterate {T : Type u_1} [DecidableEq T] (I : IdeologicalField T) {S : Finset T} [Fintype T] {n : ℕ} (h : I.construe (I.construe^[n] S) = I.construe^[n] S) :

I.indexicalField S = I.construe^[n] S

Once a reconstrual stabilizes, it is the indexical field.

Martha's Vineyard (ay) #

inductive Eckert2008.VineyardMeaning :

The meanings of centralized (ay) are membership among Vineyarders and the claim about what a Vineyarder is that the fishermen made with the variant, local authenticity and opposition to the mainland.

vineyarder : VineyardMeaning
localAuthenticity : VineyardMeaning
oppositionToMainland : VineyardMeaning

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqVineyardMeaning :

DecidableEq VineyardMeaning

Equations

Eckert2008.instDecidableEqVineyardMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeVineyardMeaning :

Fintype VineyardMeaning

Equations

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

def Eckert2008.vineyardIdeology :

IdeologicalField VineyardMeaning

The island's ideological field makes available to the index the evaluation of Vineyarders that the disagreements about the future of the island raised.

Equations

Instances For

def Eckert2008.centralizedAy :

Finset VineyardMeaning

The first-order index of centralized (ay) is membership among Vineyarders.

Equations

Eckert2008.centralizedAy = {Eckert2008.VineyardMeaning.vineyarder}

Instances For

theorem Eckert2008.vineyard_marker :

VineyardMeaning.localAuthenticity ∉ centralizedAy ∧ VineyardMeaning.localAuthenticity ∈ vineyardIdeology.construe centralizedAy

The indicator becomes a marker, local authenticity being a second-order value of centralized (ay) and not a first-order one.

theorem Eckert2008.indexicalField_centralizedAy :

vineyardIdeology.indexicalField centralizedAy = {VineyardMeaning.vineyarder, VineyardMeaning.localAuthenticity, VineyardMeaning.oppositionToMainland}

The field of [Lab63]'s variant reconstrued holds Vineyarders and what a Vineyarder is.

The (ING) field, Figure 3 #

inductive Eckert2008.INGVariant :

The velar and apical variants of (ING).

velar : INGVariant
apical : INGVariant

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqINGVariant :

DecidableEq INGVariant

Equations

Eckert2008.instDecidableEqINGVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeINGVariant :

Fintype INGVariant

Equations

Eckert2008.instFintypeINGVariant = { elems := { val := ↑Eckert2008.INGVariant.enumList, nodup := Eckert2008.INGVariant.enumList_nodup }, complete := Eckert2008.instFintypeINGVariant._proof_1 }

inductive Eckert2008.INGMeaning :

The potential meanings of Figure 3, the velar variant heard as educated, formal, effortful and articulate or pretentious, the apical as uneducated, relaxed, easygoing or lazy, and inarticulate or unpretentious.

educated : INGMeaning
uneducated : INGMeaning
formal : INGMeaning
relaxed : INGMeaning
effortful : INGMeaning
easygoing : INGMeaning
lazy : INGMeaning
articulate : INGMeaning
pretentious : INGMeaning
inarticulate : INGMeaning
unpretentious : INGMeaning

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqINGMeaning :

DecidableEq INGMeaning

Equations

Eckert2008.instDecidableEqINGMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeINGMeaning :

Fintype INGMeaning

Equations

Eckert2008.instFintypeINGMeaning = { elems := { val := ↑Eckert2008.INGMeaning.enumList, nodup := Eckert2008.INGMeaning.enumList_nodup }, complete := Eckert2008.instFintypeINGMeaning._proof_1 }

def Eckert2008.ingField :

INGVariant → Finset INGMeaning

The (ING) field of Figure 3, black for the velar variant and gray for the apical.

Equations

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

Instances For

inductive Eckert2008.Evaluation :

A hearer's evaluation of a meaning is favourable or unfavourable.

favourable : Evaluation
unfavourable : Evaluation

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqEvaluation :

DecidableEq Evaluation

Equations

Eckert2008.instDecidableEqEvaluation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeEvaluation :

Fintype Evaluation

Equations

Eckert2008.instFintypeEvaluation = { elems := { val := ↑Eckert2008.Evaluation.enumList, nodup := Eckert2008.Evaluation.enumList_nodup }, complete := Eckert2008.instFintypeEvaluation._proof_1 }

def Eckert2008.INGMeaning.evaluation :

INGMeaning → Option Evaluation

The text attaches evaluations to the meanings the figure pairs as alternatives, the apical speaker heard as inarticulate or lazy or else as unpretentious or easygoing and the velar speaker as articulate or as pretentious; the other meanings carry none.

Equations

Instances For

def Eckert2008.activate (e : Evaluation) (v : INGVariant) :

Finset INGMeaning

A hearer's evaluation activates the region of a variant's field it evaluates that way.

Equations

Eckert2008.activate e v = {x ∈ Eckert2008.ingField v | x.evaluation = some e}

Instances For

theorem Eckert2008.activate_nonempty (e : Evaluation) (v : INGVariant) :

(activate e v).Nonempty

The pairs do not work in lockstep, each variant having favourable and unfavourable meanings.

def Eckert2008.expected (i : INGMeaning) :

Finset INGVariant

Presupposed indexicality expects of a speaker the variants whose field holds the impression the hearer has formed of the speaker from general style and content.

Equations

Eckert2008.expected i = {x : Eckert2008.INGVariant | i ∈ Eckert2008.ingField x}

Instances For

theorem Eckert2008.expected_educated_uneducated :

expected INGMeaning.educated = {INGVariant.velar} ∧ expected INGMeaning.uneducated = {INGVariant.apical}

An impression of the speaker as educated leads the hearer to expect the velar variant, one as uneducated the apical.

inductive Eckert2008.Move :

The social moves a hearer attributes to the wrong variant.

pretentious : Move
condescending : Move
insincere : Move

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqMove :

DecidableEq Move

Equations

Eckert2008.instDecidableEqMove x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeMove :

Fintype Move

Equations

Eckert2008.instFintypeMove = { elems := { val := ↑Eckert2008.Move.enumList, nodup := Eckert2008.Move.enumList_nodup }, complete := Eckert2008.instFintypeMove._proof_1 }

@[instance_reducible]

instance Eckert2008.instInhabitedMove :

Inhabited Move

Equations

Eckert2008.instInhabitedMove = { default := Eckert2008.instInhabitedMove.default }

def Eckert2008.interpret (i : INGMeaning) (v : INGVariant) :

Finset Move

The expected variant passes, and the wrong one is heard as pretentious, condescending or insincere.

Equations

Eckert2008.interpret i v = if v ∈ Eckert2008.expected i then ∅ else Finset.univ

Instances For

theorem Eckert2008.interpret_eq_empty_iff (i : INGMeaning) (v : INGVariant) :

interpret i v = ∅ ↔ v ∈ expected i

theorem Eckert2008.interpret_velar_of_uneducated :

interpret INGMeaning.uneducated INGVariant.velar = Finset.univ

The velar variant from a speaker taken to be uneducated is heard as a move.

The /t/ release field, Figure 4 #

inductive Eckert2008.TStance :

The stances of Figure 4, momentary and situated.

formal : TStance
clear : TStance
emphatic : TStance
annoyed : TStance
angry : TStance
careful : TStance
exasperated : TStance
polite : TStance
effortful : TStance

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqTStance :

DecidableEq TStance

Equations

Eckert2008.instDecidableEqTStance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeTStance :

Fintype TStance

Equations

Eckert2008.instFintypeTStance = { elems := { val := ↑Eckert2008.TStance.enumList, nodup := Eckert2008.TStance.enumList_nodup }, complete := Eckert2008.instFintypeTStance._proof_1 }

inductive Eckert2008.TQuality :

The permanent qualities of Figure 4, and the quality of habitually taking a stance, the angry person of stance accretion.

educated : TQuality
articulate : TQuality
elegant : TQuality
prissy : TQuality
habitual (s : TStance) : TQuality

Instances For

def Eckert2008.instDecidableEqTQuality.decEq (x✝ x✝¹ : TQuality) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqTQuality :

DecidableEq TQuality

Equations

Eckert2008.instDecidableEqTQuality = Eckert2008.instDecidableEqTQuality.decEq

@[instance_reducible]

instance Eckert2008.instFintypeTQuality :

Fintype TQuality

Equations

Eckert2008.instFintypeTQuality = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Eckert2008.TStance) Eckert2008.TQuality.proxyTypeEquiv

inductive Eckert2008.TMeaning :

A meaning of /t/ release is a stance or a quality.

stance (s : TStance) : TMeaning
quality (q : TQuality) : TMeaning

Instances For

def Eckert2008.instDecidableEqTMeaning.decEq (x✝ x✝¹ : TMeaning) :

Decidable (x✝ = x✝¹)

Equations

Eckert2008.instDecidableEqTMeaning.decEq (Eckert2008.TMeaning.stance a) (Eckert2008.TMeaning.stance b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Eckert2008.instDecidableEqTMeaning.decEq (Eckert2008.TMeaning.stance s) (Eckert2008.TMeaning.quality q) = isFalse ⋯
Eckert2008.instDecidableEqTMeaning.decEq (Eckert2008.TMeaning.quality q) (Eckert2008.TMeaning.stance s) = isFalse ⋯
Eckert2008.instDecidableEqTMeaning.decEq (Eckert2008.TMeaning.quality a) (Eckert2008.TMeaning.quality b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqTMeaning :

DecidableEq TMeaning

Equations

Eckert2008.instDecidableEqTMeaning = Eckert2008.instDecidableEqTMeaning.decEq

@[instance_reducible]

instance Eckert2008.instFintypeTMeaning :

Fintype TMeaning

Equations

Eckert2008.instFintypeTMeaning = Fintype.ofEquiv (Eckert2008.TStance ⊕ Eckert2008.TQuality) Eckert2008.TMeaning.proxyTypeEquiv

def Eckert2008.accretion :

IdeologicalField TMeaning

Stance accretion is the ideological field on which a stance is available to be construed as the quality of habitually taking it, the mechanism by which the field is elaborated.

Equations

Eckert2008.accretion (Eckert2008.TMeaning.stance a) = {Eckert2008.TMeaning.quality (Eckert2008.TQuality.habitual a)}
Eckert2008.accretion (Eckert2008.TMeaning.quality a) = ∅

Instances For

theorem Eckert2008.quality_habitual_mem_construe {S : Finset TMeaning} {s : TStance} (h : TMeaning.stance s ∈ S) :

TMeaning.quality (TQuality.habitual s) ∈ accretion.construe S

The stances of a set of meanings accrete into qualities.

def Eckert2008.tRelease :

Finset TMeaning

The field of /t/ release of Figure 4, nine stances and four qualities.

Equations

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

Instances For

theorem Eckert2008.indexicalField_tRelease :

accretion.indexicalField tRelease = accretion.construe tRelease

Qualities are construed no further, so accretion elaborates the field in one round, and the indexical field of /t/ release is Figure 4 with the habitual quality of each of its stances.

inductive Eckert2008.SocialType :

The social types of Figure 4 are the enregistered voices at the less fluid end of the field that anchor interpretation, the British of the stereotype /t/ release evokes, the school teacher of the standard of clear speech, the nerd girl who builds on that standard while distancing herself from teachers, and the gay diva of [Pod07]'s Heath.

british : SocialType
schoolTeacher : SocialType
nerdGirl : SocialType
gayDiva : SocialType

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqSocialType :

DecidableEq SocialType

Equations

Eckert2008.instDecidableEqSocialType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Eckert2008.SocialType.anchors :

SocialType → Finset TMeaning

Each type anchors the meanings the text gives it, the British the articulateness of their stereotype and the elegance it opens up, the teacher clear, careful standard speech, the nerd girl its clarity and education, the diva the prissiness of the teacher's pet with exasperation.

Equations

One or more equations did not get rendered due to their size.
Eckert2008.SocialType.british.anchors = {Eckert2008.TMeaning.quality Eckert2008.TQuality.articulate, Eckert2008.TMeaning.quality Eckert2008.TQuality.elegant}
Eckert2008.SocialType.nerdGirl.anchors = {Eckert2008.TMeaning.stance Eckert2008.TStance.clear, Eckert2008.TMeaning.quality Eckert2008.TQuality.educated}
Eckert2008.SocialType.gayDiva.anchors = {Eckert2008.TMeaning.quality Eckert2008.TQuality.prissy, Eckert2008.TMeaning.stance Eckert2008.TStance.exasperated}

Instances For

theorem Eckert2008.nerdGirl_anchors_subset :

SocialType.nerdGirl.anchors ⊆ SocialType.schoolTeacher.anchors

The nerd girls build on the school-teachery standard from which they distance themselves.

theorem Eckert2008.gayDiva_habitual_exasperated :

TMeaning.quality (TQuality.habitual TStance.exasperated) ∈ accretion.construe SocialType.gayDiva.anchors

The diva's generalized attitude of exasperation is the stance accreted into a quality.

inductive Eckert2008.Articulation :

The continuum of /t/ articulation runs from hypo- to hyperarticulation, from the deletion stigmatized in African American English through the flap of American English and the release of British English to the exaggerated release of the diva's parody.

deletion : Articulation
flap : Articulation
released : Articulation
exaggeratedRelease : Articulation

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqArticulation :

DecidableEq Articulation

Equations

Eckert2008.instDecidableEqArticulation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeArticulation :

Fintype Articulation

Equations

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

def Eckert2008.Articulation.rank :

Articulation → ℕ

The position of an articulation on the continuum.

Equations

Instances For

@[instance_reducible]

instance Eckert2008.instLinearOrderArticulation :

LinearOrder Articulation

Equations

Eckert2008.instLinearOrderArticulation = LinearOrder.lift' Eckert2008.Articulation.rank Eckert2008.instLinearOrderArticulation._proof_1

@[instance_reducible]

instance Eckert2008.instOrderBotArticulation :

OrderBot Articulation

Equations

Eckert2008.instOrderBotArticulation = { bot := Eckert2008.Articulation.deletion, bot_le := Eckert2008.instOrderBotArticulation._proof_1 }

@[instance_reducible]

instance Eckert2008.instOrderTopArticulation :

OrderTop Articulation

Equations

Eckert2008.instOrderTopArticulation = { top := Eckert2008.Articulation.exaggeratedRelease, le_top := Eckert2008.instOrderTopArticulation._proof_1 }

def Eckert2008.divaStyle :

Finset Articulation

The diva style combines deletion with exaggerated bursts.

Equations

Eckert2008.divaStyle = {Eckert2008.Articulation.deletion, Eckert2008.Articulation.exaggeratedRelease}

Instances For

theorem Eckert2008.divaStyle_eq :

divaStyle = {⊥, ⊤}

The diva style is the two extremes of the continuum.

Belten High, Figure 1 #

inductive Eckert2008.Gender :

girl : Gender
boy : Gender

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqGender :

DecidableEq Gender

Equations

Eckert2008.instDecidableEqGender x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Eckert2008.Orientation :

The school-oriented jocks and the urban-oriented burnouts.

jock : Orientation
burnout : Orientation

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqOrientation :

DecidableEq Orientation

Equations

Eckert2008.instDecidableEqOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Eckert2008.Group :

A social category of Figure 1 crosses gender with orientation.

gender : Gender
orientation : Orientation

Instances For

def Eckert2008.instDecidableEqGroup.decEq (x✝ x✝¹ : Group) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqGroup :

DecidableEq Group

Equations

Eckert2008.instDecidableEqGroup = Eckert2008.instDecidableEqGroup.decEq

inductive Eckert2008.Stratum :

The seven variables fall into three strata, the older fronting components of the Northern Cities Shift, stabilized across the suburbs, the newer backing changes more advanced near the urban centre, and negative concord.

older : Stratum
newer : Stratum
negativeConcord : Stratum

Instances For

@[instance_reducible]

instance Eckert2008.instDecidableEqStratum :

DecidableEq Stratum

Equations

Eckert2008.instDecidableEqStratum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eckert2008.instFintypeStratum :

Fintype Stratum

Equations

Eckert2008.instFintypeStratum = { elems := { val := ↑Eckert2008.Stratum.enumList, nodup := Eckert2008.Stratum.enumList_nodup }, complete := Eckert2008.instFintypeStratum._proof_1 }

def Eckert2008.Leads (g : Group) :

Stratum → Prop

A group leads a stratum when it is among the greatest or second-greatest users Figure 1 marks, girls for the older changes and burnouts for the newer urban changes and negative concord.

Equations

Instances For

@[instance_reducible]

instance Eckert2008.instDecidablePredStratumLeads (g : Group) :

DecidablePred (Leads g)

Equations

theorem Eckert2008.leads_all_iff (g : Group) :

(∀ (s : Stratum), Leads g s) ↔ g = { gender := Gender.girl, orientation := Orientation.burnout }

The burnout girls alone are among the leaders of every variable, the two leaderships crossing gender with orientation, the urban–suburban opposition embedded within the school.

theorem Eckert2008.jockBoys_lead_none (s : Stratum) :

¬Leads { gender := Gender.boy, orientation := Orientation.jock } s

The jock boys lead nothing.