inductive DeoThomas2025.JustFlavor : Type

The interpretive flavors of just ([DT25]: §2). Nine constructors covering the paper's 7 major categories, with precisifying split into equality/proximity (§2.3.1-2) and complement exclusion separated from rank order (§2.1).

• complementExclusion : JustFlavor
• rankOrder : JustFlavor
• emphatic : JustFlavor
• precisifyingEquality : JustFlavor
• precisifyingProximity : JustFlavor
• minimalSufficiency : JustFlavor
• unexplanatory : JustFlavor
• unelaboratory : JustFlavor
• counterexpectational : JustFlavor

def DeoThomas2025.instReprJustFlavor.repr : JustFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DeoThomas2025.instReprJustFlavor : Repr JustFlavor

Equations

• DeoThomas2025.instReprJustFlavor = { reprPrec := DeoThomas2025.instReprJustFlavor.repr }

@[implicit_reducible]

instance DeoThomas2025.instDecidableEqJustFlavor : DecidableEq JustFlavor

Equations

• DeoThomas2025.instDecidableEqJustFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive DeoThomas2025.ContextType : Type

Why the widest answerable construal is optimal at context ([DT25] (37)).

• answerable : ContextType
• qualityFail : ContextType
• relevanceFail : ContextType

@[implicit_reducible]

instance DeoThomas2025.instReprContextType : Repr ContextType

Equations

• DeoThomas2025.instReprContextType = { reprPrec := DeoThomas2025.instReprContextType.repr }

def DeoThomas2025.instReprContextType.repr : ContextType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DeoThomas2025.instDecidableEqContextType : DecidableEq ContextType

Equations

• DeoThomas2025.instDecidableEqContextType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive DeoThomas2025.AlternativeSource : Type

Where the alternatives for just come from. Roothian alternatives are the standard focus-semantic alternatives; the other sources are what distinguish just from only.

• roothian : AlternativeSource
• granularity : AlternativeSource
• causal : AlternativeSource
• elaboration : AlternativeSource
• normative : AlternativeSource

def DeoThomas2025.instReprAlternativeSource.repr : AlternativeSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DeoThomas2025.instReprAlternativeSource : Repr AlternativeSource

Equations

• DeoThomas2025.instReprAlternativeSource = { reprPrec := DeoThomas2025.instReprAlternativeSource.repr }

@[implicit_reducible]

instance DeoThomas2025.instDecidableEqAlternativeSource : DecidableEq AlternativeSource

Equations

• DeoThomas2025.instDecidableEqAlternativeSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeoThomas2025.associatedSource : JustFlavor → AlternativeSource

Map each flavor of just to its alternative source.

Equations

• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.complementExclusion = DeoThomas2025.AlternativeSource.roothian
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.rankOrder = DeoThomas2025.AlternativeSource.roothian
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.emphatic = DeoThomas2025.AlternativeSource.granularity
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.precisifyingEquality = DeoThomas2025.AlternativeSource.granularity
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.precisifyingProximity = DeoThomas2025.AlternativeSource.granularity
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.minimalSufficiency = DeoThomas2025.AlternativeSource.causal
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.unexplanatory = DeoThomas2025.AlternativeSource.causal
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.unelaboratory = DeoThomas2025.AlternativeSource.elaboration
• DeoThomas2025.associatedSource DeoThomas2025.JustFlavor.counterexpectational = DeoThomas2025.AlternativeSource.normative

def DeoThomas2025.flavorOf (row : Data.Examples.LinguisticExample) : Option JustFlavor

A row's flavor feature as a JustFlavor.

Equations

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

def DeoThomas2025.contextTypeOf (row : Data.Examples.LinguisticExample) : Option ContextType

A row's context_type feature as a ContextType.

Equations

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

def DeoThomas2025.onlyOkOf (row : Data.Examples.LinguisticExample) : Bool

Whether the row's #only substitution test succeeds.

Equations

• DeoThomas2025.onlyOkOf row = (row.feature? "only_ok" == some "true")

structure DeoThomas2025.DiscourseContext (W : Type u_1) : Type u_1

A discourse context provides construals of an underspecified question (UQ) together with Quality and Relevance filters.

Construals are Questions (sets of alternative propositions), matching the paper's definition (30)-(31): questions are sets of propositions that cover the common ground. This is more faithful than using partitions (QUD), since the paper explicitly notes that granularity-based construals generally cannot be ordered by question entailment (fn. 20).

W is the world type.

• construals : List (Question W)

  The available construals of UQ_c

• quality : Question W → Bool

  Does the speaker have sufficient evidence to answer this question?

• relevance : Question W → Bool

  Is this question relevant to the current discourse?

• nonempty : self.construals ≠ []

  There must be at least one construal

def DeoThomas2025.answerable {W : Type u_1} (ctx : DiscourseContext W) (q : Question W) : Bool

A question is answerable iff it passes both Quality and Relevance (34).

Equations

• DeoThomas2025.answerable ctx q = (ctx.quality q && ctx.relevance q)

def DeoThomas2025.isWidestAnswerable {W : Type u_1} (ctx : DiscourseContext W) (q : Question W) : Prop

OPT_c(Q) ([DT25] (35)): the optimal question in a set of construals.

q is the widest answerable construal: it is answerable, it is in the construal set, and no strictly wider answerable construal exists.

Width is measured by Question.widerThan ((32)), the paper's comparison of question inquisitivity — explicitly weaker than G&S question entailment (fn. 20), because granularity-based construals generally cannot be ordered by entailment strength.

Equations

• DeoThomas2025.isWidestAnswerable ctx q = (q ∈ ctx.construals ∧ DeoThomas2025.answerable ctx q = true ∧ ∀ q' ∈ ctx.construals, DeoThomas2025.answerable ctx q' = true → ¬q'.widerThan q)

def DeoThomas2025.classifyContext {W : Type u_1} (ctx : DiscourseContext W) : ContextType

Classify a discourse context by WHY the widest answerable construal is optimal ([DT25] (37)).

• (37a) answerable: all construals are answerable → CQ = widest overall
• (37b) qualityFail: some construal fails Quality (speaker lacks evidence)
• (37c) relevanceFail: some construal fails Relevance (not discourse-relevant)

Equations

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

theorem DeoThomas2025.only_substitutes_iff_exclusive (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (onlyOkOf row = true ↔ flavorOf row = some JustFlavor.complementExclusion ∨ flavorOf row = some JustFlavor.rankOrder)

Only can substitute for just exactly in the complement-exclusion and rank-order uses.

theorem DeoThomas2025.only_substitutes_iff_roothian (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (onlyOkOf row = true ↔ Option.map associatedSource (flavorOf row) = some AlternativeSource.roothian)

Only can replace just exactly when the alternatives are Roothian.

theorem DeoThomas2025.unexplanatory_is_quality_fail (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → flavorOf row = some JustFlavor.unexplanatory → contextTypeOf row = some ContextType.qualityFail

Unexplanatory uses arise when wider construals fail Quality (37b).

theorem DeoThomas2025.unelaboratory_is_relevance_fail (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → flavorOf row = some JustFlavor.unelaboratory → contextTypeOf row = some ContextType.relevanceFail

Unelaboratory uses arise when wider construals fail Relevance (37c).

theorem DeoThomas2025.standard_uses_are_answerable (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (contextTypeOf row = some ContextType.answerable ↔ flavorOf row ≠ some JustFlavor.unexplanatory ∧ flavorOf row ≠ some JustFlavor.unelaboratory)

All other uses — complement exclusion, rank order, emphatic, precisifying, minimal sufficiency, counterexpectational — arise when the widest construal IS answerable (37a).

theorem DeoThomas2025.quality_fail_implies_causal (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → contextTypeOf row = some ContextType.qualityFail → Option.map associatedSource (flavorOf row) = some AlternativeSource.causal

Quality-failure contexts yield only causal-alternative flavors.

theorem DeoThomas2025.relevance_fail_implies_elaboration (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → contextTypeOf row = some ContextType.relevanceFail → Option.map associatedSource (flavorOf row) = some AlternativeSource.elaboration

Relevance-failure contexts yield only elaboration-alternative flavors.

theorem DeoThomas2025.only_requires_shared_cq (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → onlyOkOf row = true → Option.map associatedSource (flavorOf row) = some AlternativeSource.roothian

only is felicitous only with Roothian alternatives (shared CQ). just is felicitous regardless of alternative source. This is WHY they diverge: only exhaustifies over shared alternatives, just widens the question.

theorem DeoThomas2025.all_flavors_attested (f : JustFlavor) : (Examples.all.any fun (x : Data.Examples.LinguisticExample) => flavorOf x == some f) = true

All 9 JustFlavor constructors are attested in the example rows.

def DeoThomas2025.justFlavorFromConstruction : Degree.AdjectivalConstruction → JustFlavor

Derive just flavor from adjectival construction type. [TD20] predict:

• comparative + just → precisifying proximity (barely)
• equative + just → precisifying equality (exactly)

Equations

• DeoThomas2025.justFlavorFromConstruction Degree.AdjectivalConstruction.comparative = DeoThomas2025.JustFlavor.precisifyingProximity
• DeoThomas2025.justFlavorFromConstruction Degree.AdjectivalConstruction.equative = DeoThomas2025.JustFlavor.precisifyingEquality
• DeoThomas2025.justFlavorFromConstruction x✝ = DeoThomas2025.JustFlavor.complementExclusion

theorem DeoThomas2025.comparative_yields_proximity : flavorOf Examples.precisifying_prox_older = some (justFlavorFromConstruction Degree.AdjectivalConstruction.comparative)

"Fafen is just older than Siri" — comparative + just = proximity.

theorem DeoThomas2025.equative_yields_equality : flavorOf Examples.precisifying_eq_full = some (justFlavorFromConstruction Degree.AdjectivalConstruction.equative)

Equative + just = equality ("just as tall as" ≈ "exactly as tall as"). Note: precisifying_eq_full ("just full") achieves equality via a closed-scale endpoint standard, not via equative morphology. The shared flavor (.precisifyingEquality) reflects parallel pragmatic effects through different compositional routes.

theorem DeoThomas2025.equative_data_match_corpus (d : ThomasDeo2020.GranularityDatum) : d ∈ ThomasDeo2020.allGranularityData → d.construction = Degree.AdjectivalConstruction.equative → some (justFlavorFromConstruction d.construction) = flavorOf Examples.precisifying_eq_full

Every equative datum of [TD20] §3 receives the flavor of the 2025 corpus's equality row.

theorem DeoThomas2025.comparative_data_match_corpus (d : ThomasDeo2020.GranularityDatum) : d ∈ ThomasDeo2020.allGranularityData → d.construction = Degree.AdjectivalConstruction.comparative → some (justFlavorFromConstruction d.construction) = flavorOf Examples.precisifying_prox_older

Every comparative datum of [TD20] §3 receives the flavor of the 2025 corpus's proximity row.

def DeoThomas2025.wxdyAlternativeSource : AlternativeSource

WXDY's incredulity arises from a normative expectation violation: the situation violates what the speaker considers normal/appropriate. This is the same alternative source as counterexpectational just ("He's just texting during the lecture!").

• WXDY: "What's this fly doing in my soup?" — violates dining norms
• just: "He's just texting during the lecture!" — violates classroom norms

Equations

• DeoThomas2025.wxdyAlternativeSource = DeoThomas2025.AlternativeSource.normative

theorem DeoThomas2025.wxdy_incongruity_is_counterexpectational : wxdyAlternativeSource = associatedSource JustFlavor.counterexpectational

WXDY's incongruity and counterexpectational just share the same alternative source: both involve normative expectations being violated.

Partition refinement implies question width

The paper's central formal insight: finer granularity produces wider questions. At the partition level, "finer" is QUD.refines (every fine cell ⊆ some coarse cell), equivalently q.toSetoid ≤ q'.toSetoid in mathlib's Setoid lattice. At the issue level, "wider" is Question.widerThan ([DT25] (32): same info, no coarse answer ⊊ fine answer, some fine answer ⊊ coarse answer). The bridge: toIssue := Question.fromSetoid ∘ QUD.toSetoid preserves this relationship.

The proof is an order-theoretic one-liner over Setoid: every alternative of Question.fromSetoid r is either ∅ or an equivalence class of r (alt_fromSetoid_subset_classes), and the q-class of w₀ is contained in the q'-class of w₀ by refinement, with v₀ witnessing strict containment. This replaces a 100-line Bool/List proof that managed indices into worlds : List W and case-split on properlyContains.

def DeoThomas2025.toIssue {W : Type u_2} (q : QUD W) : Question W

A QUD partitions a meaning space via an equivalence relation; via QUD.toSetoid and Question.fromSetoid, every QUD induces an inquisitive content whose alternatives are exactly the QUD's equivalence classes. The bridge is one-way: not every Question arises from a QUD (mention-some, intermediate-exhaustive, and conditional-question alternatives are non-disjoint or non-exhaustive and so are not representable as the cells of any equivalence relation — [TRA18]).

Equations

• DeoThomas2025.toIssue q = Question.fromSetoid q.toSetoid

theorem DeoThomas2025.refinement_implies_wider {W : Type u_2} (q q' : QUD W) (hRefines : q.refines q') (w₀ v₀ : W) (hCoarse : q'.r w₀ v₀) (hFine : ¬q.r w₀ v₀) : (toIssue q).widerThan (toIssue q')

Strict partition refinement implies issue width.

If q (strictly) refines q' (q is the finer partition), then toIssue q is wider than toIssue q' as Questions.

The strictness witnesses w₀, v₀ : W share a coarse cell (q'.r w₀ v₀) but not a fine cell (¬ q.r w₀ v₀); they witness condition (c).

The proof establishes the three conditions of Question.widerThan:

• (a) Same info: both fromSetoid-derived issues have info = univ.
• (b) No q'-alternative is properly contained in any q-alternative: alternatives are classes (or ∅); under refinement, classes only widen as we go from the finer to the coarser setoid, so the reverse containment is impossible.
• (c) Some q-alternative properly contained in some q'-alternative: witnessed by the q-class and q'-class of w₀, with v₀ showing the inclusion is strict.

The full chain: finer granularity → wider question

Composes the two independently proved steps:

1. finer_granularity_refines (from Degree.Granularity): if ε₁ ∣ ε₂, the ε₁-partition refines the ε₂-partition
2. refinement_implies_wider (proved above): strict partition refinement → issue width

This is the formal content of the lexical entry (36): just selects the widest answerable construal, which — when alternatives vary by granularity — is the finest one the speaker can answer.

theorem DeoThomas2025.finer_granularity_implies_wider (n ε₁ ε₂ : ℕ) (hdvd : ε₁ ∣ ε₂) (w₀ v₀ : Fin n) (hCoarse : (Degree.Granularity.granQUD n ε₂).r w₀ v₀) (hFine : ¬(Degree.Granularity.granQUD n ε₁).r w₀ v₀) : (toIssue (Degree.Granularity.granQUD n ε₁)).widerThan (toIssue (Degree.Granularity.granQUD n ε₂))

The complete granularity–width chain ([DT25] §3.1.2–3.2).

If ε₁ divides ε₂ (finer grain) and there exist worlds that share a coarse cell but not a fine cell, then the fine-grained question is strictly wider than the coarse-grained question.

This is the general version of Figure 1: any uniform-grain-width scale satisfies the width relation when grain widths are divisible.

def DeoThomas2025.fig1Worlds : List (Fin 8)

The 8-point age scale from Figure 1 ([DT25]).

Equations

• DeoThomas2025.fig1Worlds = [0, 1, 2, 3, 4, 5, 6, 7]

def DeoThomas2025.coarseQ : QUD (Fin 8)

Coarse granularity: 2 cells of 4 (e.g., "younger half" vs "older half"). Worlds 0–3 share one answer, worlds 4–7 share another.

Equations

• DeoThomas2025.coarseQ = QUD.ofProject fun (w : Fin 8) => ↑w / 4

def DeoThomas2025.fineQ : QUD (Fin 8)

Fine granularity: 4 cells of 2 (e.g., {0,1}, {2,3}, {4,5}, {6,7}). Each pair of adjacent worlds shares an answer.

Equations

• DeoThomas2025.fineQ = QUD.ofProject fun (w : Fin 8) => ↑w / 2

theorem DeoThomas2025.coarseQ_is_granQUD : coarseQ = Degree.Granularity.granQUD 8 4

Figure 1's partitions are instances of the general granQUD.

theorem DeoThomas2025.fineQ_is_granQUD : fineQ = Degree.Granularity.granQUD 8 2

theorem DeoThomas2025.fig1_strict_refinement : fineQ.refines coarseQ ∧ ¬coarseQ.refines fineQ

Fine strictly refines coarse: knowing the fine answer determines the coarse answer, but not vice versa (0 and 2 share a coarse cell but not a fine cell).

theorem DeoThomas2025.fig1_finer_is_wider : (toIssue fineQ).widerThan (toIssue coarseQ)

Figure 1 via the general granularity–width theorem. The fine 4-cell partition produces a wider issue than the coarse 2-cell partition over the 8-point domain.

Witnessed by worlds 0 and 2: they share a coarse cell (0/4 = 2/4 = 0) but not a fine cell (0/2 = 0 ≠ 2/2 = 1).