Schlotterbeck & Wang (2023): An incremental RSA model for adjective ordering preferences

This file formalizes the paper's fully incremental Rational Speech Act model (Table 1) and the qualitative predictions it draws from it for the order of two prenominal adjectives. The incremental literal listener (l0) interprets a word sequence from the noun outward, each word against the support of the distribution the later words left, so a context-dependent meaning such as the k%-semantics of a dimension adjective (kPercent) can resolve differently in the two orders. The incremental sequence speaker produces the words left to right, scoring each prefix by its utility for the referent and each word by a language model (seqSpeaker); the global speaker scores whole sequences, and the incremental utterance speaker is a softmax over the sequence speaker with an utterance prior.

The paper's theoretical result is the listener-level sanity check: at a context-independent semantics the incremental listener is the one-shot literal listener at the product meaning, because Bayesian updates compose, so it cannot distinguish word orders (l0_perm), and the global speaker is then indifferent between them. The speaker-level prediction, the effect of discriminatory strength, comes from the language model that produces either adjective first and then the other: with an order-blind listener the sequence speaker's preference between the two orders is its preference between their first words, and at a uniform prior and Boolean meanings the more informative first word is the one true of fewer referents (seqSpeaker_real_lt_of_card_lt). The k%-semantics witnesses that the listener does distinguish orders once meanings depend on the comparison class (l0_big_blue_ne).

Implementation notes

• Meanings are graded and bounded by one; the comparison class is a finset of referents, and the support of a distribution is the finset of referents it gives positive mass. Sequences are surface-order lists with the noun-adjacent word last, and the speakers over sequences of a fixed length are weight kernels on Fin n → U.
• The paper leaves the cost function unspecified; here the cost factor exp (−β c) depends on the sequence length alone, which covers per-word costs and cost zero, and the rationality β is free rather than pinned to the paper's one.
• With the noise floor ε > 0 of the paper's color semantics no color word empties the support, so in the paper's simulations every later word is interpreted against the whole display; the order-sensitivity witness uses a sharp color meaning. The perceptual blur of the size distribution manipulation is not modeled.

References

• [SW23b]
• [CGGP19]
• [DHG+20]
• [SDG17]
• [FG12]

Meanings and the language model

noncomputable def SchlotterbeckWang2023.sharp {U : Type u_1} {R : Type u_2} (ext : U → Finset R → Finset R) : U → Finset R → R → ENNReal

A Boolean semantics, as graded meanings.

Equations

• SchlotterbeckWang2023.sharp ext u C = (↑(ext u C)).indicator 1

theorem SchlotterbeckWang2023.sharp_apply_le_one {U : Type u_1} {R : Type u_2} (ext : U → Finset R → Finset R) (u : U) (C : Finset R) (r : R) : sharp ext u C r ≤ 1

def SchlotterbeckWang2023.extSeq {U : Type u_1} {R : Type u_2} [Fintype R] [DecidableEq R] (ext : U → Finset R → Finset R) : List U → Finset R

The sequentially intersective update of a Boolean semantics builds the extension of a sequence from the noun outward.

Equations

• SchlotterbeckWang2023.extSeq ext [] = Finset.univ
• SchlotterbeckWang2023.extSeq ext (u :: us) = SchlotterbeckWang2023.extSeq ext us ∩ ext u (SchlotterbeckWang2023.extSeq ext us)

noncomputable def SchlotterbeckWang2023.alternation {U : Type u_1} [DecidableEq U] (a b : U) : List U → U → ENNReal

The paper's language model puts either adjective first, with equal probability, then the other.

Equations

• SchlotterbeckWang2023.alternation a b [] x✝ = if x✝ = a ∨ x✝ = b then 2⁻¹ else 0
• SchlotterbeckWang2023.alternation a b [u'] x✝ = if u' = a ∧ x✝ = b ∨ u' = b ∧ x✝ = a then 1 else 0
• SchlotterbeckWang2023.alternation a b x✝¹ x✝ = 0

theorem SchlotterbeckWang2023.alternation_comm {U : Type u_1} [DecidableEq U] (a b : U) : alternation a b = alternation b a

theorem SchlotterbeckWang2023.alternation_ne_top {U : Type u_1} [DecidableEq U] {a b : U} (us : List U) (u : U) : alternation a b us u ≠ ⊤

noncomputable def SchlotterbeckWang2023.supp {R : Type u_2} [Fintype R] [MeasurableSpace R] (ν : MeasureTheory.Measure R) : Finset R

The support of a distribution over referents, the comparison class the next word is interpreted against.

Equations

• SchlotterbeckWang2023.supp ν = {r : R | ν {r} ≠ 0}

theorem SchlotterbeckWang2023.mem_supp {R : Type u_2} [Fintype R] [MeasurableSpace R] {ν : MeasureTheory.Measure R} {r : R} : r ∈ supp ν ↔ ν {r} ≠ 0

The incremental listener (rows 1–2)

noncomputable def SchlotterbeckWang2023.l0 {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] (μ : MeasureTheory.Measure R) (sem : U → Finset R → R → ENNReal) : List U → MeasureTheory.Measure R

The incremental literal listener of rows (1)–(2) reads a word sequence in surface order, the noun-adjacent word last. That word is interpreted first, against the prior's support, and each earlier word against the support of the distribution the later words left.

Equations

• One or more equations did not get rendered due to their size.
• SchlotterbeckWang2023.l0 μ sem [] = μ

theorem SchlotterbeckWang2023.l0_apply_le_one {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} [MeasureTheory.IsProbabilityMeasure μ] (us : List U) (s : Set R) : (l0 μ sem us) s ≤ 1

Utilities and sequence weights (rows 4–5 and 7)

noncomputable def SchlotterbeckWang2023.utility {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] (μ : MeasureTheory.Measure R) (sem : U → Finset R → R → ENNReal) (β : ℝ) (cost : ℕ → ENNReal) (us : List U) (r : R) : ENNReal

The utility of row (7) scores the sequence us for the referent r at rationality β, with cost n the cost factor exp (−β c) of an n-word sequence.

Equations

• SchlotterbeckWang2023.utility μ sem β cost us r = (SchlotterbeckWang2023.l0 μ sem us) {r} ^ β * cost us.length

noncomputable def SchlotterbeckWang2023.seqWeight {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] (μ : MeasureTheory.Measure R) (sem : U → Finset R → R → ENNReal) (β : ℝ) (cost : ℕ → ENNReal) (pLang : List U → U → ENNReal) (r : R) (us : List U) : ENNReal

Unrolling rows (4)–(5), the weight of producing us word by word scores each prefix by its utility and each word by the language model's probability given the words before it.

Equations

• SchlotterbeckWang2023.seqWeight μ sem β cost pLang r us = ∏ i : Fin us.length, SchlotterbeckWang2023.utility μ sem β cost (List.take (↑i + 1) us) r * pLang (List.take (↑i) us) us[i]

theorem SchlotterbeckWang2023.utility_ne_top {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} {r : R} [MeasureTheory.IsProbabilityMeasure μ] (hβ : 0 ≤ β) (hcost : ∀ (n : ℕ), cost n ≠ ⊤) (us : List U) : utility μ sem β cost us r ≠ ⊤

Two adjectives

theorem SchlotterbeckWang2023.seqWeight_pair_alternation {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} [DecidableEq U] (r : R) (a b : U) : seqWeight μ sem β cost (alternation a b) r [a, b] = 2⁻¹ * (utility μ sem β cost [a] r * utility μ sem β cost [a, b] r)

theorem SchlotterbeckWang2023.seqWeight_pair_lt_iff {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} [DecidableEq U] (r : R) (a b : U) : seqWeight μ sem β cost (alternation a b) r [a, b] < seqWeight μ sem β cost (alternation a b) r [b, a] ↔ utility μ sem β cost [a] r * utility μ sem β cost [a, b] r < utility μ sem β cost [b] r * utility μ sem β cost [b, a] r

Under the paper's language model the sequence speaker's order preference compares the utilities accumulated along the two production paths.

theorem SchlotterbeckWang2023.seqWeight_pair_lt_iff_of_l0_eq {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} {r : R} {a b : U} [DecidableEq U] [MeasureTheory.IsProbabilityMeasure μ] (hβ : 0 ≤ β) (hcost : ∀ (n : ℕ), cost n ≠ ⊤) (hl : l0 μ sem [a, b] = l0 μ sem [b, a]) (hne : utility μ sem β cost [a, b] r ≠ 0) : seqWeight μ sem β cost (alternation a b) r [a, b] < seqWeight μ sem β cost (alternation a b) r [b, a] ↔ utility μ sem β cost [a] r < utility μ sem β cost [b] r

With an order-blind listener, the sequence speaker's preference between the two orders is its preference between their first words, the discriminatory strength of the first word.

theorem SchlotterbeckWang2023.utility_single_lt_iff {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} {r : R} {a b : U} (hβ : 0 < β) (h0 : cost 1 ≠ 0) (htop : cost 1 ≠ ⊤) : utility μ sem β cost [a] r < utility μ sem β cost [b] r ↔ (l0 μ sem [a]) {r} < (l0 μ sem [b]) {r}

At a positive rationality the first-word utility comparison is the listener comparison.

Order-blind listeners

theorem SchlotterbeckWang2023.l0_contextFree {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {μ : MeasureTheory.Measure R} [MeasureTheory.IsProbabilityMeasure μ] (m : U → R → ENNReal) (hm : ∀ (u : U) (r : R), m u r ≤ 1) (us : List U) : l0 μ (fun (u : U) (x : Finset R) => m u) us = (μ.withDensity (RSA.prodMeaning m us))[|Set.univ]

At a context-independent semantics the incremental listener is the one-shot literal listener at the product meaning, since Bayesian updates compose.

theorem SchlotterbeckWang2023.l0_perm {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {μ : MeasureTheory.Measure R} [MeasureTheory.IsProbabilityMeasure μ] (m : U → R → ENNReal) (hm : ∀ (u : U) (r : R), m u r ≤ 1) {us us' : List U} (h : us.Perm us') : l0 μ (fun (u : U) (x : Finset R) => m u) us = l0 μ (fun (u : U) (x : Finset R) => m u) us'

A context-independent semantics cannot distinguish word orders, the paper's sanity check.

theorem SchlotterbeckWang2023.supp_uniformOn {R : Type u_2} [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] (S : Finset R) : supp (ProbabilityTheory.uniformOn ↑S) = S

theorem SchlotterbeckWang2023.l0_indicator {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] [DecidableEq R] (ext : U → Finset R → Finset R) (us : List U) : l0 (ProbabilityTheory.uniformOn Set.univ) (sharp ext) us = ProbabilityTheory.uniformOn ↑(extSeq ext us)

At a uniform prior and a Boolean semantics the incremental listener is uniform on the sequentially intersected extension.

theorem SchlotterbeckWang2023.l0_single_lt_iff {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {r : R} {a b : U} [DecidableEq R] (ext : U → Finset R → Finset R) (ha : r ∈ ext a Finset.univ) (hb : r ∈ ext b Finset.univ) : (l0 (ProbabilityTheory.uniformOn Set.univ) (sharp ext) [a]) {r} < (l0 (ProbabilityTheory.uniformOn Set.univ) (sharp ext) [b]) {r} ↔ (ext b Finset.univ).card < (ext a Finset.univ).card

At a uniform prior and Boolean meanings, of two words true of the referent the one true of fewer referents is the more informative first word.

The speaker kernels (rows 3–6)

noncomputable def SchlotterbeckWang2023.seqSpeaker {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] (μ : MeasureTheory.Measure R) (sem : U → Finset R → R → ENNReal) (β : ℝ) (cost : ℕ → ENNReal) (pLang : List U → U → ENNReal) (n : ℕ) : ProbabilityTheory.Kernel R (Fin n → U)

The incremental sequence speaker of rows (4)–(5) chooses among sequences of length n.

Equations

• SchlotterbeckWang2023.seqSpeaker μ sem β cost pLang n = ProbabilityTheory.Kernel.ofWeights fun (r : R) (v : Fin n → U) => SchlotterbeckWang2023.seqWeight μ sem β cost pLang r (List.ofFn v)

noncomputable def SchlotterbeckWang2023.globalSpeaker {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] (μ : MeasureTheory.Measure R) (sem : U → Finset R → R → ENNReal) (β : ℝ) (cost : ℕ → ENNReal) {n : ℕ} (P : (Fin n → U) → ENNReal) : ProbabilityTheory.Kernel R (Fin n → U)

The global speaker of row (3) chooses among sequences of length n with utterance prior P.

Equations

• SchlotterbeckWang2023.globalSpeaker μ sem β cost P = ProbabilityTheory.Kernel.ofWeights fun (r : R) (v : Fin n → U) => SchlotterbeckWang2023.utility μ sem β cost (List.ofFn v) r * P v

noncomputable def SchlotterbeckWang2023.uttSpeaker {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] (μ : MeasureTheory.Measure R) (sem : U → Finset R → R → ENNReal) (β : ℝ) (cost : ℕ → ENNReal) (pLang : List U → U → ENNReal) (α : ℝ) {n : ℕ} (P : (Fin n → U) → ENNReal) : ProbabilityTheory.Kernel R (Fin n → U)

The incremental utterance speaker of row (6) is a softmax at rationality α over the sequence speaker with utterance prior P.

Equations

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

theorem SchlotterbeckWang2023.seqSpeaker_real_lt_iff {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} {pLang : List U → U → ENNReal} {r : R} [MeasureTheory.IsProbabilityMeasure μ] (hβ : 0 ≤ β) (hcost : ∀ (n : ℕ), cost n ≠ ⊤) (hp : ∀ (us : List U) (u : U), pLang us u ≠ ⊤) {n : ℕ} (h0 : ∃ (v : Fin n → U), seqWeight μ sem β cost pLang r (List.ofFn v) ≠ 0) {v v' : Fin n → U} : ((seqSpeaker μ sem β cost pLang n) r).real {v} < ((seqSpeaker μ sem β cost pLang n) r).real {v'} ↔ seqWeight μ sem β cost pLang r (List.ofFn v) < seqWeight μ sem β cost pLang r (List.ofFn v')

An order preference of the sequence speaker is a weight comparison; normalization cancels.

theorem SchlotterbeckWang2023.globalSpeaker_apply_singleton_eq {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} {r : R} {n : ℕ} {P : (Fin n → U) → ENNReal} {v v' : Fin n → U} (hl : l0 μ sem (List.ofFn v) = l0 μ sem (List.ofFn v')) (hP : P v = P v') : ((globalSpeaker μ sem β cost P) r) {v} = ((globalSpeaker μ sem β cost P) r) {v'}

A global speaker (row (3)) cannot prefer an order the listener cannot distinguish.

theorem SchlotterbeckWang2023.uttSpeaker_real_lt_iff {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {μ : MeasureTheory.Measure R} {sem : U → Finset R → R → ENNReal} {β : ℝ} {cost : ℕ → ENNReal} {pLang : List U → U → ENNReal} {r : R} [MeasureTheory.IsProbabilityMeasure μ] (hβ : 0 ≤ β) (hcost : ∀ (n : ℕ), cost n ≠ ⊤) (hp : ∀ (us : List U) (u : U), pLang us u ≠ ⊤) {α : ℝ} (hα : 0 ≤ α) {n : ℕ} {P : (Fin n → U) → ENNReal} (hP : ∀ (v : Fin n → U), P v ≠ ⊤) (h0 : ∃ (v : Fin n → U), seqWeight μ sem β cost pLang r (List.ofFn v) ^ α * P v ≠ 0) {v v' : Fin n → U} : ((uttSpeaker μ sem β cost pLang α P) r).real {v} < ((uttSpeaker μ sem β cost pLang α P) r).real {v'} ↔ seqWeight μ sem β cost pLang r (List.ofFn v) ^ α * P v < seqWeight μ sem β cost pLang r (List.ofFn v') ^ α * P v'

The order preference of the utterance speaker (row (6)) is the sequence speaker's, weighed against the utterance prior.

theorem SchlotterbeckWang2023.seqSpeaker_real_lt_of_card_lt {U : Type u_1} {R : Type u_2} [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] {β : ℝ} {cost : ℕ → ENNReal} {r : R} {a b : U} [DecidableEq U] [DecidableEq R] (hβ : 0 < β) (hcost0 : ∀ (n : ℕ), cost n ≠ 0) (hcost : ∀ (n : ℕ), cost n ≠ ⊤) (ext : U → Finset R) (ha : r ∈ ext a) (hb : r ∈ ext b) (hcard : (ext a).card < (ext b).card) : ((seqSpeaker (ProbabilityTheory.uniformOn Set.univ) (sharp fun (u : U) (x : Finset R) => ext u) β cost (alternation a b) 2) r).real {![b, a]} < ((seqSpeaker (ProbabilityTheory.uniformOn Set.univ) (sharp fun (u : U) (x : Finset R) => ext u) β cost (alternation a b) 2) r).real {![a, b]}

At a uniform prior, sharp context-independent meanings and the paper's language model, the sequence speaker prefers first the adjective true of fewer referents, the relevance effect.

The k%-semantics (3a) distinguishes the orders

def SchlotterbeckWang2023.kPercent {R : Type u_2} [Fintype R] (k : ℕ) (size : R → ℕ) (C : Finset R) : Finset R

Under the k%-semantics (3a) of a dimension adjective against the comparison class C, an object is big when its size exceeds the maximum of C less k% of the range of C.

Equations

• SchlotterbeckWang2023.kPercent k size C = {x : R | ∃ (hC : C.Nonempty), 100 * C.sup' hC size < 100 * size x + k * (C.sup' hC size - C.inf' hC size)}

inductive SchlotterbeckWang2023.Sticker : Type

The display has three blue stickers of sizes 6, 5 and 1, and a green one of size 10.

• blue6 : Sticker
• blue5 : Sticker
• blue1 : Sticker
• green10 : Sticker

@[instance_reducible]

instance SchlotterbeckWang2023.instDecidableEqSticker : DecidableEq Sticker

Equations

• SchlotterbeckWang2023.instDecidableEqSticker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SchlotterbeckWang2023.instFintypeSticker : Fintype Sticker

Equations

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

@[instance_reducible]

instance SchlotterbeckWang2023.instMeasurableSpaceSticker : MeasurableSpace Sticker

Equations

• SchlotterbeckWang2023.instMeasurableSpaceSticker = ⊤

instance SchlotterbeckWang2023.instDiscreteMeasurableSpaceSticker : DiscreteMeasurableSpace Sticker

def SchlotterbeckWang2023.Sticker.size : Sticker → ℕ

A sticker's size.

Equations

• SchlotterbeckWang2023.Sticker.blue6.size = 6
• SchlotterbeckWang2023.Sticker.blue5.size = 5
• SchlotterbeckWang2023.Sticker.blue1.size = 1
• SchlotterbeckWang2023.Sticker.green10.size = 10

inductive SchlotterbeckWang2023.Adj : Type

The two adjectives of the paper's stimuli.

• big : Adj
• blue : Adj

@[instance_reducible]

instance SchlotterbeckWang2023.instDecidableEqAdj : DecidableEq Adj

Equations

• SchlotterbeckWang2023.instDecidableEqAdj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SchlotterbeckWang2023.instFintypeAdj : Fintype Adj

Equations

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

@[instance_reducible]

instance SchlotterbeckWang2023.instMeasurableSpaceAdj : MeasurableSpace Adj

Equations

• SchlotterbeckWang2023.instMeasurableSpaceAdj = ⊤

instance SchlotterbeckWang2023.instDiscreteMeasurableSpaceAdj : DiscreteMeasurableSpace Adj

def SchlotterbeckWang2023.Adj.ext : Adj → Finset Sticker → Finset Sticker

big by the 50%-semantics of the paper's simulations, and blue sharply.

Equations

• SchlotterbeckWang2023.Adj.big.ext x✝ = SchlotterbeckWang2023.kPercent 50 SchlotterbeckWang2023.Sticker.size x✝
• SchlotterbeckWang2023.Adj.blue.ext x✝ = {SchlotterbeckWang2023.Sticker.blue6, SchlotterbeckWang2023.Sticker.blue5, SchlotterbeckWang2023.Sticker.blue1}

theorem SchlotterbeckWang2023.l0_big_blue_ne : l0 (ProbabilityTheory.uniformOn Set.univ) (sharp Adj.ext) [Adj.big, Adj.blue] ≠ l0 (ProbabilityTheory.uniformOn Set.univ) (sharp Adj.ext) [Adj.blue, Adj.big]

Big blue and blue big resolve differently, since big interpreted against the blue stickers admits the second-largest one, which it excludes against the whole display.