Documentation

Studies.BeltramaSoltBurnett2023

Two experiments crossed three variants of a duration, approximate about fifty minutes, underspecified fifty minutes and precise forty-nine minutes, with four scenarios ranked by their need for precision, and had the speaker rated on scales that reduce to Status, Solidarity and anti-Solidarity. Precise speakers are rated above approximate ones on Status and anti-Solidarity and below them on Solidarity, and the underspecified variant patterns with the precise one on Status and with the approximate one on anti-Solidarity. The paper reads this in two ways (pp. 828–829): the underspecified variant is a neutral zero point, so that precision and approximation are separate indexical loci, or round numbers partake of both ends of a single opposition.

Main statements #

borneOut_contrastField, borneOut_neutral: both readings are borne out by the means of both experiments (p. 828), though on the opposition reading the precise and approximate variants are antipodal and each fits a single persona, while on the neutral reading they are separate loci (separateLoci_neutral) and each fits two personae.
not_needHypothesis: no table of cell means that agrees with the cells Experiment 2 reports satisfies the hypothesis that raising the need for precision favors the more precise variant; the other reported interactions run as it predicts (favors_exp1, favors_exp2).
loadsMostOn_exp1, loadsMostOn_exp2_iff: by maximal loading, the principal components recover the planned grouping of the scales in Experiment 1, and in Experiment 2 for every scale but friendly, which loads most on Status.

Implementation notes #

Status, Solidarity and anti-Solidarity are read as the competence, warmth and anti-solidarity of SocialMeaning.Dimension.
The neutral reading takes the paper's verdict on each comparison with the underspecified variant, counting the trend of Experiment 1 on Status as a difference, as the paper does (p. 818); no p-value is thresholded.
The underspecified variant is ranked between the others in precision, being compatible with a precise and an imprecise interpretation (p. 809).
The context hypothesis is stated over full tables of cell means, which the paper only plots (Figures 2–4, 9–11); the theorems hold of every table agreeing with the printed cells.

References #

The variants #

theorem BeltramaSoltBurnett2023.underspecified_eq_representative (e : Experiment) :

↑(stimuli e Variant.underspecified).before = Degree.representative 10 ↑(stimuli e Variant.precise).before ∧ ↑(stimuli e Variant.underspecified).after = Degree.representative 10 ↑(stimuli e Variant.precise).after

The underspecified durations report the precise ones at the grain of ten minutes, each the multiple of ten closest to it (p. 807).

def BeltramaSoltBurnett2023.Approximator.modifier :

Approximator → Numerals.NumeralModifier

The numeral modifier an approximator is.

Equations

Instances For

theorem BeltramaSoltBurnett2023.precise_not_mem_underspecified (e : Experiment) :

(stimuli e Variant.precise).after ∉ Degree.Comparison.eq.interval (stimuli e Variant.underspecified).after ∪ Degree.Comparison.ge.interval (stimuli e Variant.underspecified).after

Of a trip that takes the precise duration, the underspecified description is false read literally, on the two-sided and on the lower-bounded meaning of the bare numeral (p. 807).

theorem BeltramaSoltBurnett2023.precise_mem_approximate (e : Experiment) {a : Approximator} (ha : (stimuli e Variant.approximate).afterApproximator = some a) {m : Modifier (Set ℕ)} (hr : m ∈ Semantics.Denotes.denote a.modifier) (hne : m {(stimuli e Variant.approximate).after} ≠ {(stimuli e Variant.approximate).after}) :

(stimuli e Variant.precise).after ∈ m {(stimuli e Variant.approximate).after}

The approximate description of the trip is true on every reading of its approximator that is not exact.

Two readings of the underspecified variant #

def BeltramaSoltBurnett2023.Factor.dimension :

Factor ≃ SocialMeaning.Dimension

The dimension of social evaluation a composite score measures.

Equations

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

Instances For

def BeltramaSoltBurnett2023.means (e : Experiment) :

SocialMeaning.AssociationField Variant SocialMeaning.Dimension ℚ

The mean composite scores of an experiment.

Equations

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

Instances For

def BeltramaSoltBurnett2023.BorneOut (F : SocialMeaning.AssociationField Variant SocialMeaning.Dimension SignType) (e : Experiment) :

A sign field is borne out by an experiment when the means order every two variants that the field orders.

Equations

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

Instances For

@[instance_reducible]

instance BeltramaSoltBurnett2023.instDecidableBorneOut (F : SocialMeaning.AssociationField Variant SocialMeaning.Dimension SignType) (e : Experiment) :

Decidable (BorneOut F e)

Equations

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

def BeltramaSoltBurnett2023.SeparateLoci (F : SocialMeaning.AssociationField Variant SocialMeaning.Dimension SignType) :

The precise and approximate variants are separate indexical loci when each indexes a dimension the other does not.

Equations

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

Instances For

theorem BeltramaSoltBurnett2023.SeparateLoci.not_antipodal {F : SocialMeaning.AssociationField Variant SocialMeaning.Dimension SignType} (h : SeparateLoci F) :

¬F.Antipodal Variant.precise Variant.approximate

theorem BeltramaSoltBurnett2023.underspecified_mem_uIoo (e : Experiment) (d : SocialMeaning.Dimension) :

means e Variant.underspecified d ∈ Set.uIoo (means e Variant.precise d) (means e Variant.approximate d)

The underspecified variant is rated strictly between the precise and the approximate ones on every dimension in both experiments (p. 827).

def BeltramaSoltBurnett2023.contrastField (e : Experiment) :

SocialMeaning.AssociationField Variant SocialMeaning.Dimension SignType

On the opposition reading the variants are measured against the underspecified one, every difference of means counting.

Equations

BeltramaSoltBurnett2023.contrastField e = ((BeltramaSoltBurnett2023.means e).contrast BeltramaSoltBurnett2023.Variant.underspecified).signs

Instances For

theorem BeltramaSoltBurnett2023.antipodal_contrastField (e : Experiment) :

(contrastField e).Antipodal Variant.precise Variant.approximate

The precise and approximate variants are the two ends of a single opposition, since the underspecified variant lies between them.

theorem BeltramaSoltBurnett2023.contrastField_exp2 :

contrastField Experiment.exp2 = contrastField Experiment.exp1

Experiment 2 replicates the opposition of Experiment 1 (p. 825).

theorem BeltramaSoltBurnett2023.ground_contrastField_precise (e : Experiment) :

(contrastField e).ground.indexes Variant.precise = {SocialMeaning.Pole.competent, SocialMeaning.Pole.cold, SocialMeaning.Pole.antiSolidary}

theorem BeltramaSoltBurnett2023.ground_contrastField_approximate (e : Experiment) :

(contrastField e).ground.indexes Variant.approximate = {SocialMeaning.Pole.incompetent, SocialMeaning.Pole.warm, SocialMeaning.Pole.solidary}

theorem BeltramaSoltBurnett2023.lift_contrastField_precise (e : Experiment) :

(contrastField e).ground.lift Variant.precise = {{SocialMeaning.Pole.competent, SocialMeaning.Pole.cold, SocialMeaning.Pole.antiSolidary}}

theorem BeltramaSoltBurnett2023.borneOut_contrastField (e e' : Experiment) :

BorneOut (contrastField e) e'

def BeltramaSoltBurnett2023.Verdict.sign :

Verdict → SignType

The direction of a verdict; a trend counts.

Equations

Instances For

def BeltramaSoltBurnett2023.neutral (e : Experiment) :

SocialMeaning.AssociationField Variant SocialMeaning.Dimension SignType

On the neutral reading the underspecified variant is the zero point, and a variant indexes a dimension in the direction of its reported difference from it (p. 828).

Equations

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

Instances For

theorem BeltramaSoltBurnett2023.neutral_eq_zero_or_eq_contrastField (e : Experiment) (v : Variant) (d : SocialMeaning.Dimension) :

neutral e v d = 0 ∨ neutral e v d = contrastField e v d

Where the paper reports a difference, it runs in the direction of the means.

theorem BeltramaSoltBurnett2023.separateLoci_neutral (e : Experiment) :

SeparateLoci (neutral e)

In both experiments the Status contrast is driven by approximation alone and the anti-Solidarity contrast by precision alone (p. 828).

theorem BeltramaSoltBurnett2023.not_separateLoci_contrastField (e : Experiment) :

¬SeparateLoci (contrastField e)

theorem BeltramaSoltBurnett2023.ground_neutral_precise :

(neutral Experiment.exp2).ground.indexes Variant.precise = {SocialMeaning.Pole.cold, SocialMeaning.Pole.antiSolidary}

theorem BeltramaSoltBurnett2023.ground_neutral_approximate :

(neutral Experiment.exp2).ground.indexes Variant.approximate = {SocialMeaning.Pole.incompetent, SocialMeaning.Pole.warm}

theorem BeltramaSoltBurnett2023.card_lift_neutral_precise :

((neutral Experiment.exp2).ground.lift Variant.precise).card = 2

theorem BeltramaSoltBurnett2023.borneOut_neutral (e e' : Experiment) :

BorneOut (neutral e) e'

Scenario modulation #

def BeltramaSoltBurnett2023.Factor.valence :

Factor → ℚ

The favorable direction of a composite score; the anti-Solidarity scales measure low solidarity (p. 812).

Equations

Instances For

def BeltramaSoltBurnett2023.Scenario.need :

Scenario → ℕ

The need for precision of a scenario, highest for the record and lowest in Bonding (p. 811).

Equations

Instances For

def BeltramaSoltBurnett2023.Variant.precision :

Variant → ℕ

The precision of a variant.

Equations

Instances For

def BeltramaSoltBurnett2023.Agrees (e : Experiment) (T : Scenario → Variant → Factor → ℚ) :

A table of cell means agrees with the cells an experiment reports.

Equations

BeltramaSoltBurnett2023.Agrees e T = ∀ r ∈ BeltramaSoltBurnett2023.scenarioRatings, r.experiment = e → T r.scenario r.variant r.factor = r.mean.toRat

Instances For

def BeltramaSoltBurnett2023.Favors (T : Scenario → Variant → Factor → ℚ) (f : Factor) (s s' : Scenario) (v w : Variant) :

Scenario s favors variant v over variant w on a composite score more than scenario s' does.

Equations

BeltramaSoltBurnett2023.Favors T f s s' v w = (f.valence * (T s' v f - T s' w f) < f.valence * (T s v f - T s w f))

Instances For

def BeltramaSoltBurnett2023.NeedHypothesis (T : Scenario → Variant → Factor → ℚ) :

The hypothesis of p. 810 is that a scenario that needs precision more favors a more precise variant more.

Equations

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

Instances For

theorem BeltramaSoltBurnett2023.favors_exp1 {T : Scenario → Variant → Factor → ℚ} (hT : Agrees Experiment.exp1 T) :

Favors T Factor.status Scenario.forTheRecord Scenario.bonding Variant.precise Variant.approximate ∧ Favors T Factor.antiSolidarity Scenario.forTheRecord Scenario.bonding Variant.underspecified Variant.approximate

theorem BeltramaSoltBurnett2023.favors_exp2 {T : Scenario → Variant → Factor → ℚ} (hT : Agrees Experiment.exp2 T) :

Favors T Factor.solidarity Scenario.forTheRecord Scenario.stranger Variant.precise Variant.underspecified ∧ Favors T Factor.status Scenario.persuasive Scenario.forTheRecord Variant.precise Variant.underspecified

In Experiment 2 the For-the-record scenario favors the precise variant over the underspecified one on Solidarity more than the Stranger scenario does, as the hypothesis predicts, but the Persuasive scenario favors it on Status more than For-the-record does (p. 823), against the hypothesis; the paper leaves this unexplained (p. 830).

theorem BeltramaSoltBurnett2023.not_needHypothesis {T : Scenario → Variant → Factor → ℚ} (hT : Agrees Experiment.exp2 T) :

¬NeedHypothesis T

The grouping of the scales #

def BeltramaSoltBurnett2023.LoadsMostOn (e : Experiment) (s : Scale) (f : Factor) :

A scale loads most on a principal component, the criterion by which the paper assigns a scale that loads on two (note 2).

Equations

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

Instances For

@[instance_reducible]

instance BeltramaSoltBurnett2023.instDecidableLoadsMostOn (e : Experiment) (s : Scale) (f : Factor) :

Decidable (LoadsMostOn e s f)

Equations

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

theorem BeltramaSoltBurnett2023.loadsMostOn_exp1 (s : Scale) :

LoadsMostOn Experiment.exp1 s (scales s).dimension

In Experiment 1 every scale loads most on the dimension it was included to measure.

theorem BeltramaSoltBurnett2023.loadsMostOn_exp2_iff (s : Scale) :

LoadsMostOn Experiment.exp2 s (scales s).dimension ↔ s ≠ Scale.friendly

In Experiment 2 every scale but friendly loads most on the dimension it was included to measure; friendly loads most on Status (Table 3).

theorem BeltramaSoltBurnett2023.loadsMostOn_friendly_exp2 :

LoadsMostOn Experiment.exp2 Scale.friendly Factor.status